mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Tactic.DepRewrite
Mathlib.Tactic.DepRewrite.Config.mk : Lean.Meta.TransparencyMode →
  Lean.Meta.Occurrences →
    Mathlib.Tactic.DepRewrite.CastMode → Lean.Meta.TransparencyMode → Mathlib.Tactic.DepRewrite.Config
-- Mathlib.Algebra.Order.Module.Defs
Prod.instSMulPosStrictMono : ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} [inst : Zero α] [inst_1 : PartialOrder α] [inst_2 : PartialOrder β]
  [inst_3 : PartialOrder γ] [inst_4 : Zero β] [inst_5 : Zero γ] [inst_6 : SMulWithZero α β] [inst_7 : SMulWithZero α γ]
  [SMulPosStrictMono α β] [SMulPosStrictMono α γ], SMulPosStrictMono α (β × γ)
-- Mathlib.Data.QPF.Univariate.Basic
QPF.Wequiv.below.abs : ∀ {F : Type u → Type v} [q : QPF F] {motive : (a a_1 : (QPF.P F).W) → QPF.Wequiv a a_1 → Prop} (a : (QPF.P F).A)
  (f : (QPF.P F).B a → (QPF.P F).W) (a' : (QPF.P F).A) (f' : (QPF.P F).B a' → (QPF.P F).W)
  (a_1 : QPF.abs ⟨a, f⟩ = QPF.abs ⟨a', f'⟩), QPF.Wequiv.below ⋯
-- Mathlib.Data.Finsupp.SMul
Finsupp.sum_smul_index' : ∀ {α : Type u_1} {M : Type u_3} {N : Type u_4} {R : Type u_6} [inst : Zero M] [inst_1 : SMulZeroClass R M]
  [inst_2 : AddCommMonoid N] {g : α →₀ M} {b : R} {h : α → M → N},
  (∀ (i : α), h i 0 = 0) → (b • g).sum h = g.sum fun i c => h i (b • c)
-- Mathlib.Analysis.InnerProductSpace.Basic
inner_re_symm : ∀ {𝕜 : Type u_1} {E : Type u_2} [inst : RCLike 𝕜] [inst_1 : SeminormedAddCommGroup E] [inst_2 : InnerProductSpace 𝕜 E]
  (x y : E), RCLike.re (inner 𝕜 x y) = RCLike.re (inner 𝕜 y x)
-- Std.Data.DHashMap.Raw
/-- Support for the `for` loop construct in `do` blocks.  -/
Std.DHashMap.Raw.Const.forInUncurried : {α : Type u} →
  {δ : Type w} →
    {m : Type w → Type w'} →
      [Monad m] → {β : Type v} → (α × β → δ → m (ForInStep δ)) → δ → (Std.DHashMap.Raw α fun x => β) → m δ
-- Mathlib.Algebra.Algebra.Subalgebra.Centralizer
Subalgebra.centralizer_coe_sup : ∀ {R : Type u_1} [inst : CommSemiring R] {A : Type u_2} [inst_1 : Semiring A] [inst_2 : Algebra R A]
  (S T : Subalgebra R A), Subalgebra.centralizer R ↑(S ⊔ T) = Subalgebra.centralizer R ↑S ⊓ Subalgebra.centralizer R ↑T
-- Lean.Elab.DocString
_private.Lean.Elab.DocString.0.Lean.Doc.getModState : {m : Type → Type} →
  [Monad m] →
    [Lean.MonadEnv m] →
      [MonadLiftT IO m] →
        [MonadLiftT Lean.MetaM m] →
          [Lean.MonadLCtx m] → [Lean.MonadResolveName m] → [Lean.MonadOptions m] → m Lean.Doc.ModuleDocstringState✝
-- Std.Data.Internal.List.Associative
_private.Std.Data.Internal.List.Associative.0.Std.Internal.List.minEntry?_cons.match_1.eq_1 : ∀ {α : Type u_2} {β : α → Type u_1} (motive : Option ((a : α) × β a) → Sort u_3) (h_1 : Unit → motive none)
  (h_2 : (w : (a : α) × β a) → motive (some w)),
  (match none with
    | none => h_1 ()
    | some w => h_2 w) =
    h_1 ()
-- Mathlib.Analysis.Normed.Group.Defs
NormedCommGroup.ofMulDist.eq_1 : ∀ {E : Type u_5} [inst : Norm E] [inst_1 : CommGroup E] [inst_2 : MetricSpace E] (h₁ : ∀ (x : E), ‖x‖ = dist 1 x)
  (h₂ : ∀ (x y z : E), dist x y ≤ dist (z * x) (z * y)),
  NormedCommGroup.ofMulDist h₁ h₂ =
    { toNorm := (NormedGroup.ofMulDist h₁ h₂).toNorm, toGroup := (NormedGroup.ofMulDist h₁ h₂).toGroup, mul_comm := ⋯,
      toMetricSpace := (NormedGroup.ofMulDist h₁ h₂).toMetricSpace, dist_eq := ⋯ }
-- Init.Data.Int.DivMod.Lemmas
Int.neg_add_fmod_self : ∀ (a b : ℤ), (-a + b).fmod a = b.fmod a
-- Mathlib.CategoryTheory.LocallyDirected
CategoryTheory.instIsLocallyDirectedWidePushoutShapeOfMonoObjNoneSomeMapInit : ∀ {J : Type u_1} (F : CategoryTheory.Functor (CategoryTheory.Limits.WidePushoutShape J) (Type u_2))
  [∀ (i : J), CategoryTheory.Mono (F.map (CategoryTheory.Limits.WidePushoutShape.Hom.init i))], F.IsLocallyDirected
-- Lean.Meta.Tactic.Subst
Lean.Meta.substCore? : Lean.MVarId →
  Lean.FVarId →
    optParam Bool false →
      optParam Lean.Meta.FVarSubst { } →
        optParam Bool true → optParam Bool false → Lean.MetaM (Option (Lean.Meta.FVarSubst × Lean.MVarId))
-- Mathlib.Data.NNRat.Defs
NNRat.coe_inj : ∀ {p q : ℚ≥0}, ↑p = ↑q ↔ p = q
-- Mathlib.NumberTheory.NumberField.Completion.FinitePlace
/-- **Alias** of `NumberField.HeightOneSpectrum.adicAbv_add_le_max`.

---

The `v`-adic absolute value satisfies the ultrametric inequality.  -/
NumberField.HeightOneSpectrum.NumberField.RingOfIntegers.HeightOneSpectrum.adicAbv_add_le_max : ∀ (K : Type u_1) [inst : Field K] {R : Type u_2} [inst_1 : CommRing R] [inst_2 : Algebra R K]
  [inst_3 : IsDedekindDomain R] [inst_4 : IsFractionRing R K] (v : IsDedekindDomain.HeightOneSpectrum R)
  [inst_5 : Module.Finite ℤ R] [inst_6 : Module.Free ℤ R] (x y : K),
  (NumberField.HeightOneSpectrum.adicAbv K v) (x + y) ≤
    max ((NumberField.HeightOneSpectrum.adicAbv K v) x) ((NumberField.HeightOneSpectrum.adicAbv K v) y)
-- Lean.Data.Lsp.LanguageFeatures
Lean.Lsp.instBEqSemanticTokenType : BEq Lean.Lsp.SemanticTokenType
-- Mathlib.Algebra.Homology.HomotopyCategory.HomComplexSingle
CochainComplex.HomComplex.Cocycle.fromSingleMk_zero : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Preadditive C]
  [inst_2 : CategoryTheory.Limits.HasZeroObject C] (X : C) (K : CochainComplex C ℤ) {p q n : ℤ} (h : p + n = q) (q' : ℤ)
  (hq' : q + 1 = q'), CochainComplex.HomComplex.Cocycle.fromSingleMk 0 h q' hq' ⋯ = 0
-- Mathlib.Algebra.Category.ModuleCat.Presheaf.Submodule
ModuleCat.semilinearMapAddEquiv.eq_1 : ∀ {R : Type u₁} {S : Type u₂} [inst : Ring R] [inst_1 : Ring S] (f : R →+* S) (M : ModuleCat R) (N : ModuleCat S),
  ModuleCat.semilinearMapAddEquiv f M N =
    { toFun := fun g => ModuleCat.ofHom { toFun := ⇑g, map_add' := ⋯, map_smul' := ⋯ },
      invFun := fun g => { toFun := ⇑(CategoryTheory.ConcreteCategory.hom g), map_add' := ⋯, map_smul' := ⋯ },
      left_inv := ⋯, right_inv := ⋯, map_add' := ⋯ }
-- Mathlib.LinearAlgebra.Matrix.NonsingularInverse
Matrix.nonsing_inv_cancel_or_zero : ∀ {n : Type u'} {α : Type v} [inst : Fintype n] [inst_1 : DecidableEq n] [inst_2 : CommRing α] (A : Matrix n n α),
  A⁻¹ * A = 1 ∧ A * A⁻¹ = 1 ∨ A⁻¹ = 0
-- Mathlib.Algebra.Module.LocalizedModule.Submodule
Submodule.toLocalizedQuotient'_mk : ∀ {R : Type u_5} (S : Type u_6) {M : Type u_7} {N : Type u_8} [inst : CommRing R] [inst_1 : CommRing S]
  [inst_2 : AddCommGroup M] [inst_3 : AddCommGroup N] [inst_4 : Module R M] [inst_5 : Module R N] [inst_6 : Algebra R S]
  [inst_7 : Module S N] [inst_8 : IsScalarTower R S N] (p : Submonoid R) [inst_9 : IsLocalization p S] (f : M →ₗ[R] N)
  [inst_10 : IsLocalizedModule p f] (M' : Submodule R M) (x : M),
  (Submodule.toLocalizedQuotient' S p f M') (Submodule.Quotient.mk x) = Submodule.Quotient.mk (f x)
-- Mathlib.Control.Traversable.Basic
/-- A traversable functor is a functor along with a way to commute
with all applicative functors (see `sequence`).  For example, if `t`
is the traversable functor `List` and `m` is the applicative functor
`IO`, then given a function `f : α → IO β`, the function `Functor.map f` is
`List α → List (IO β)`, but `traverse f` is `List α → IO (List β)`.  -/
Traversable : (Type u → Type u) → Type (u + 1)
-- Init.Data.Rat.Lemmas
Rat.lt_irrefl : ∀ {a : ℚ}, ¬a < a
-- Lean.Meta.TryThis
/-- Text to be used as a suggested replacement in the infoview. This can be either a `TSyntax kind`
for a single `kind : SyntaxNodeKind` or a raw `String`.

Instead of using constructors directly, there are coercions available from these types to
`SuggestionText`.  -/
Lean.Meta.Tactic.TryThis.SuggestionText : Type
-- Mathlib.Order.Cover
Pi.wcovBy_iff_exists_left_eq : ∀ {ι : Type u_3} {α : ι → Type u_4} [inst : (i : ι) → PartialOrder (α i)] {a b : (i : ι) → α i} [Nonempty ι]
  [inst_2 : DecidableEq ι], a ⩿ b ↔ ∃ i x, x ⩿ b i ∧ a = Function.update b i x
-- Mathlib.RingTheory.LocalRing.ResidueField.Ideal
Ideal.injective_algebraMap_quotient_residueField : ∀ {R : Type u_1} [inst : CommRing R] (I : Ideal R) [inst_1 : I.IsPrime],
  Function.Injective ⇑(algebraMap (R ⧸ I) I.ResidueField)
-- Std.Data.ExtDTreeMap.Lemmas
Std.ExtDTreeMap.Const.get!_insertIfNew : ∀ {α : Type u} {cmp : α → α → Ordering} {β : Type v} {t : Std.ExtDTreeMap α (fun x => β) cmp} [inst : Std.TransCmp cmp]
  [inst_1 : Inhabited β] {k a : α} {v : β},
  Std.ExtDTreeMap.Const.get! (t.insertIfNew k v) a =
    if cmp k a = Ordering.eq ∧ k ∉ t then v else Std.ExtDTreeMap.Const.get! t a
-- Init.Grind.Lemmas
Lean.Grind.eq_of_beq_eq_true : ∀ {α : Type u} {x : BEq α} {x_1 : LawfulBEq α} {a b : α}, (a == b) = true → a = b
-- Batteries.Data.Float.Lemmas
Float.Model.UnpackedFloat.pack_unpack : ∀ {spec : Float.Model.Format} (b : BitVec spec.numBits),
  autoParam (2 ≤ spec.exponentBits) Float.Model.UnpackedFloat.pack_unpack._auto_1 →
    Float.Model.UnpackedFloat.pack spec (Float.Model.UnpackedFloat.unpack spec b) =
      if Float.Model.UnpackedFloat.isNaNBits b = true then Float.Model.UnpackedFloat.packedNaN spec else b
-- Mathlib.Order.Disjoint
Complementeds.mk_bot : ∀ {α : Type u_1} [inst : Lattice α] [inst_1 : BoundedOrder α], ⟨⊥, ⋯⟩ = ⊥
-- Mathlib.Topology.Constructions
map_nhds_subtype_val : ∀ {X : Type u} [inst : TopologicalSpace X] {s : Set X} (x : ↑s), Filter.map Subtype.val (nhds x) = nhdsWithin (↑x) s
-- Mathlib.Data.Fin.Basic
Fin.eq_zero : ∀ (n : Fin 1), n = 0
-- Mathlib.Order.JordanHolder
/-- **Alias** of `JordanHolderLattice.iso_refl`. -/
JordanHolderLattice.IsMaximal.iso_refl : ∀ {X : Type u} [inst : Lattice X] [inst_1 : JordanHolderLattice X] {x : X × X}, JordanHolderLattice.Iso x x
-- Mathlib.Algebra.Ring.Periodic
Function.Antiperiodic.nat_even_mul_periodic : ∀ {α : Type u_1} {β : Type u_2} {f : α → β} {c : α} [inst : NonAssocSemiring α] [inst_1 : InvolutiveNeg β],
  Function.Antiperiodic f c → ∀ (n : ℕ), Function.Periodic f (↑n * (2 * c))
-- Mathlib.Algebra.Homology.Double
HomologicalComplex.evalCompCoyonedaCorepresentableBySingle_homEquiv_symm_apply : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  [inst_2 : CategoryTheory.Limits.HasZeroObject C] {ι : Type u_2} (c : ComplexShape ι) (i : ι) [inst_3 : DecidableEq ι]
  (hi : ∀ (j : ι), ¬c.Rel i j) (X : C) {K : HomologicalComplex C c}
  (f : ((HomologicalComplex.eval C c i).comp (CategoryTheory.coyoneda.obj (Opposite.op X))).obj K),
  (HomologicalComplex.evalCompCoyonedaCorepresentableBySingle c i hi X).homEquiv.symm f =
    HomologicalComplex.mkHomFromSingle f ⋯
-- Mathlib.RingTheory.IntegralClosure.IsIntegral.Basic
/-- If `R → A → B` is an algebra tower,
then if the entire tower is an integral extension so is `A → B`.  -/
IsIntegral.tower_top : ∀ {R : Type u_1} {A : Type u_2} {B : Type u_3} [inst : CommRing R] [inst_1 : CommRing A] [inst_2 : Ring B]
  [inst_3 : Algebra R A] [inst_4 : Algebra R B] [inst_5 : Algebra A B] [IsScalarTower R A B] {x : B},
  IsIntegral R x → IsIntegral A x
-- Mathlib.Algebra.Homology.ShortComplex.Basic
CategoryTheory.ShortComplex.opMap_id : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  (S : CategoryTheory.ShortComplex C),
  CategoryTheory.ShortComplex.opMap (CategoryTheory.CategoryStruct.id S) = CategoryTheory.CategoryStruct.id S.op
-- Mathlib.CategoryTheory.Limits.Shapes.Pullback.Categorical.Basic
CategoryTheory.Limits.CategoricalPullback.CatCommSqOver.precompose_map_whiskerRight : ∀ {A : Type u₁} {B : Type u₂} {C : Type u₃} [inst : CategoryTheory.Category.{v₁, u₁} A]
  [inst_1 : CategoryTheory.Category.{v₂, u₂} B] [inst_2 : CategoryTheory.Category.{v₃, u₃} C]
  (F : CategoryTheory.Functor A B) (G : CategoryTheory.Functor C B) {X : Type u₄} {Y : Type u₅} {Z : Type u₆}
  [inst_3 : CategoryTheory.Category.{v₄, u₄} X] [inst_4 : CategoryTheory.Category.{v₅, u₅} Y]
  [inst_5 : CategoryTheory.Category.{v₆, u₆} Z] {U V : CategoryTheory.Functor X Y} (α : U ⟶ V)
  (W : CategoryTheory.Functor Y Z),
  (CategoryTheory.Limits.CategoricalPullback.CatCommSqOver.precompose F G).map
      (CategoryTheory.Functor.whiskerRight α W) =
    CategoryTheory.CategoryStruct.comp
      (CategoryTheory.Limits.CategoricalPullback.CatCommSqOver.precomposeObjComp F G U W).hom
      (CategoryTheory.CategoryStruct.comp
        (((CategoryTheory.Limits.CategoricalPullback.CatCommSqOver.precompose F G).obj W).whiskerLeft
          ((CategoryTheory.Limits.CategoricalPullback.CatCommSqOver.precompose F G).map α))
        (CategoryTheory.Limits.CategoricalPullback.CatCommSqOver.precomposeObjComp F G V W).inv)
-- Init.SimpLemmas
cond_true : ∀ {α : Sort u_1} (a b : α), (bif true then a else b) = a
-- Mathlib.Algebra.Lie.Prod
LieHom.prod_comp : ∀ {R : Type u_1} {L₁ : Type u_2} {L₂ : Type u_3} {L : Type u_4} [inst : CommRing R] [inst_1 : LieRing L₁]
  [inst_2 : LieAlgebra R L₁] [inst_3 : LieRing L₂] [inst_4 : LieAlgebra R L₂] [inst_5 : LieRing L]
  [inst_6 : LieAlgebra R L] (f : L₁ →ₗ⁅R⁆ L₂) (g : L₁ →ₗ⁅R⁆ L) (h : L →ₗ⁅R⁆ L₁),
  (f.prod g).comp h = (f.comp h).prod (g.comp h)
-- Mathlib.Algebra.Algebra.Subalgebra.Unitization
/-- The natural star `R`-algebra homomorphism from the unitization of a non-unital star subalgebra
to its `StarAlgebra.adjoin`.  -/
NonUnitalStarSubalgebra.unitization : {R : Type u_1} →
  {S : Type u_2} →
    {A : Type u_3} →
      [inst : CommSemiring R] →
        [inst_1 : StarRing R] →
          [inst_2 : Semiring A] →
            [inst_3 : StarRing A] →
              [inst_4 : Algebra R A] →
                [StarModule R A] →
                  [inst_6 : SetLike S A] →
                    [hSA : NonUnitalSubsemiringClass S A] →
                      [hSRA : SMulMemClass S R A] → [inst_7 : StarMemClass S A] → (s : S) → Unitization R ↥s →⋆ₐ[R] A
-- Mathlib.CategoryTheory.Comma.Over.Basic
/-- Characterization of the costructured arrow category on the projection functor of any
costructured arrow category.  -/
CategoryTheory.CostructuredArrow.ofCostructuredArrowProjEquivalence : {T : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} T] →
    {D : Type u₂} →
      [inst_1 : CategoryTheory.Category.{v₂, u₂} D] →
        (F : CategoryTheory.Functor T D) →
          (Y : D) →
            (X : T) →
              CategoryTheory.CostructuredArrow (CategoryTheory.CostructuredArrow.proj F Y) X ≌
                CategoryTheory.CostructuredArrow ((CategoryTheory.Over.forget X).comp F) Y
-- Mathlib.Order.Filter.Extr
/-- `IsMinFilter f l a` means that `f a ≤ f x` for all `x` in some `l`-neighborhood of `a`  -/
IsMinFilter : {α : Type u} → {β : Type v} → [Preorder β] → (α → β) → Filter α → α → Prop
-- Mathlib.CategoryTheory.Limits.Preserves.Creates.Opposites
/-- If `F.leftOp : Cᵒᵖ ⥤ D` creates limits, then `F : C ⥤ Dᵒᵖ` creates colimits.  -/
CategoryTheory.Limits.createsColimitsOfLeftOp : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    {D : Type u₂} →
      [inst_1 : CategoryTheory.Category.{v₂, u₂} D] →
        (F : CategoryTheory.Functor C Dᵒᵖ) → [CategoryTheory.CreatesLimits F.leftOp] → CategoryTheory.CreatesColimits F
-- Mathlib.CategoryTheory.Retract
/-- If a morphism `f` is a retract of `g`,
then `F.map f` is a retract of `F.map g` for any functor `F`.  -/
CategoryTheory.RetractArrow.map : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    {D : Type u'} →
      [inst_1 : CategoryTheory.Category.{v', u'} D] →
        {X Y Z W : C} →
          {f : X ⟶ Y} →
            {g : Z ⟶ W} →
              CategoryTheory.RetractArrow f g →
                (F : CategoryTheory.Functor C D) → CategoryTheory.RetractArrow (F.map f) (F.map g)
-- Mathlib.Order.Category.PartOrd
PartOrd.uliftFunctor_obj_coe : ∀ (X : PartOrd), ↑(PartOrd.uliftFunctor.obj X) = ULift.{v, u} ↑X
-- Mathlib.MeasureTheory.Measure.Haar.NormedSpace
MeasureTheory.Measure.integral_comp_mul_left : ∀ {F : Type u_2} [inst : NormedAddCommGroup F] [inst_1 : NormedSpace ℝ F] (g : ℝ → F) (a : ℝ),
  ∫ (x : ℝ), g (a * x) = |a⁻¹| • ∫ (y : ℝ), g y
-- Mathlib.ModelTheory.Basic
FirstOrder.Language.Embedding.refl_apply : ∀ {L : FirstOrder.Language} {M : Type w} [inst : L.Structure M] (x : M), (FirstOrder.Language.Embedding.refl L M) x = x
-- Mathlib.CategoryTheory.Retract
CategoryTheory.RetractArrow.instIsSplitEpiLeftRArrow : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {X Y Z W : C} {f : X ⟶ Y} {g : Z ⟶ W}
  (h : CategoryTheory.RetractArrow f g), CategoryTheory.IsSplitEpi (CategoryTheory.Arrow.Hom.left h.r)
-- Mathlib.RingTheory.Flat.Equalizer
/-- If `M` is `R`-flat, the canonical map `M ⊗[R] ker f →ₗ[R] ker (𝟙 ⊗ f)` is an isomorphism.  -/
LinearMap.tensorKerEquiv : {R : Type u_1} →
  (S : Type u_2) →
    [inst : CommRing R] →
      [inst_1 : CommRing S] →
        [inst_2 : Algebra R S] →
          (M : Type u_3) →
            [inst_3 : AddCommGroup M] →
              [inst_4 : Module R M] →
                [inst_5 : Module S M] →
                  [inst_6 : IsScalarTower R S M] →
                    {N : Type u_4} →
                      {P : Type u_5} →
                        [inst_7 : AddCommGroup N] →
                          [inst_8 : AddCommGroup P] →
                            [inst_9 : Module R N] →
                              [inst_10 : Module R P] →
                                (f : N →ₗ[R] P) →
                                  [Module.Flat R M] →
                                    TensorProduct R M ↥f.ker ≃ₗ[S]
                                      ↥((TensorProduct.AlgebraTensorModule.lTensor S M) f).ker
-- Lean.Data.Lsp.LanguageFeatures
Lean.Lsp.instHashableSemanticTokenType.hash : Lean.Lsp.SemanticTokenType → UInt64
-- Mathlib.GroupTheory.Exponent
AddMonoid.exponent_eq_max'_addOrderOf : ∀ {G : Type u} [inst : AddCancelCommMonoid G] [inst_1 : Fintype G],
  AddMonoid.exponent G = (Finset.image addOrderOf Finset.univ).max' ⋯
-- Mathlib.Probability.Kernel.Composition.Comp
ProbabilityTheory.Kernel.comp_sum_right : ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} {mα : MeasurableSpace α} {mβ : MeasurableSpace β}
  {mγ : MeasurableSpace γ} {ι : Type u_4} [inst : Countable ι] (κ : ι → ProbabilityTheory.Kernel α β)
  (η : ProbabilityTheory.Kernel β γ),
  η.comp (ProbabilityTheory.Kernel.sum κ) = ProbabilityTheory.Kernel.sum fun i => η.comp (κ i)
-- Mathlib.Tactic.Widget.StringDiagram
/-- Nodes for 2-morphisms in a string diagram.  -/
Mathlib.Tactic.Widget.StringDiagram.AtomNode : Type
-- Std.Data.HashMap.Lemmas
Std.HashMap.contains_of_contains_erase : ∀ {α : Type u} {β : Type v} {x : BEq α} {x_1 : Hashable α} {m : Std.HashMap α β} [EquivBEq α] [LawfulHashable α]
  {k a : α}, (m.erase k).contains a = true → m.contains a = true
-- Mathlib.Combinatorics.Matroid.Minor.Order
/-- `N` is a minor of `M` if `N = M ／ C ＼ D` for some `C` and `D`.
The definition itself does not require `C` and `D` to be disjoint,
or even to be subsets of the ground set. See `Matroid.IsMinor.exists_eq_contract_delete_disjoint`
for the fact that we can choose `C` and `D` with these properties.  -/
Matroid.IsMinor : {α : Type u_1} → Matroid α → Matroid α → Prop
-- Mathlib.Algebra.Star.StarAlgHom
/-- Any type satisfying `AlgEquivClass` and `StarHomClass` can be cast into `StarAlgEquiv` via
`StarAlgEquivClass.toStarAlgEquiv`.  -/
StarAlgEquivClass.instCoeHead : {F : Type u_1} →
  {R : Type u_2} →
    {A : Type u_3} →
      {B : Type u_4} →
        [inst : Add A] →
          [inst_1 : Mul A] →
            [inst_2 : SMul R A] →
              [inst_3 : Star A] →
                [inst_4 : Add B] →
                  [inst_5 : Mul B] →
                    [inst_6 : SMul R B] →
                      [inst_7 : Star B] →
                        [inst_8 : EquivLike F A B] →
                          [NonUnitalAlgEquivClass F R A B] → [StarHomClass F A B] → CoeHead F (A ≃⋆ₐ[R] B)
-- Mathlib.CategoryTheory.Limits.IsLimit
CategoryTheory.Limits.IsColimit.extendIso.eq_1 : ∀ {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.Cocone F} {X : C} (i : s.pt ⟶ X)
  [inst_2 : CategoryTheory.IsIso i] (hs : CategoryTheory.Limits.IsColimit s),
  CategoryTheory.Limits.IsColimit.extendIso i hs = hs.ofIsoColimit (s.extendIso (CategoryTheory.asIso i))
-- Mathlib.CategoryTheory.Functor.ReflectsIso.Basic
CategoryTheory.isIso_iff_of_reflects_iso : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] {D : Type u_2}
  [inst_1 : CategoryTheory.Category.{v_2, u_2} D] {A B : C} (f : A ⟶ B) (F : CategoryTheory.Functor C D)
  [F.ReflectsIsomorphisms], CategoryTheory.IsIso (F.map f) ↔ CategoryTheory.IsIso f
-- Mathlib.Analysis.Fourier.AddCircle
fourier_one : ∀ {T : ℝ} {x : AddCircle T}, (fourier 1) x = ↑x.toCircle
-- Std.Do.SPred.DerivedLaws
Std.Do.SPred.and_elim_r' : ∀ {σs : List (Type u)} {P Q R : Std.Do.SPred σs}, (Q ⊢ₛ R) → P ∧ Q ⊢ₛ R
-- Lean.Parser.Term
/-- `binrel_no_prop% r a b` is similar to `binrel% r a b`, but it coerces `Prop` arguments into `Bool`.  -/
Lean.Parser.Term.binrel_no_prop : Lean.Parser.Parser
-- Mathlib.Algebra.Module.Torsion.PrimaryComponent
Ideal.primaryComponent_sup : ∀ {A : Type u_1} {M : Type u_2} [inst : CommRing A] (I : Ideal A) [inst_1 : AddCommGroup M] [inst_2 : Module A M]
  (N₁ N₂ : Submodule A M),
  Disjoint N₁ N₂ →
    Submodule.map (N₁ ⊔ N₂).subtype (Ideal.primaryComponent (↥(N₁ ⊔ N₂)) I) =
      Submodule.map N₁.subtype (Ideal.primaryComponent (↥N₁) I) ⊔
        Submodule.map N₂.subtype (Ideal.primaryComponent (↥N₂) I)
-- Mathlib.Analysis.Complex.UpperHalfPlane.MoebiusAction
/-- The matrix `[-1, 0; 0, 1]`, which defines an anti-holomorphic involution of `ℍ` via
`τ ↦ -conj τ`.  -/
UpperHalfPlane.J : GL (Fin 2) ℝ
-- Mathlib.Topology.Neighborhoods
IsOpen.mem_nhds : ∀ {X : Type u} [inst : TopologicalSpace X] {x : X} {s : Set X}, IsOpen s → x ∈ s → s ∈ nhds x
-- Lean.Util.SafeExponentiation
/-- Returns `true` if `n` is `≤ exponentiation.threshold`. Otherwise,
reports a warning and returns `false`.
This method ensures there is at most one warning message of this kind in the message log.
 -/
Lean.checkExponent : ℕ → optParam Bool true → Lean.CoreM Bool
-- Mathlib.Algebra.Group.Subgroup.Basic
Subgroup.comap_normalClosure_image_ge : ∀ {G : Type u_1} [inst : Group G] {N : Type u_5} [inst_1 : Group N] (s : Set G) (f : G →* N),
  Subgroup.normalClosure s ≤ Subgroup.comap f (Subgroup.normalClosure (⇑f '' s))
-- Mathlib.Geometry.Euclidean.Angle.Oriented.Basic
/-- The sign of the angle between a linear combination of two vectors and the second vector is
the sign of the factor by which the first vector is multiplied in that combination multiplied by
the sign of the angle between the two vectors.  -/
Orientation.oangle_sign_smul_add_smul_left : ∀ {V : Type u_1} [inst : NormedAddCommGroup V] [inst_1 : InnerProductSpace ℝ V] [inst_2 : Fact (Module.finrank ℝ V = 2)]
  (o : Orientation ℝ V (Fin 2)) (x y : V) (r₁ r₂ : ℝ),
  (o.oangle (r₁ • x + r₂ • y) y).sign = SignType.sign r₁ * (o.oangle x y).sign
-- Mathlib.Analysis.Normed.Group.Defs
NormedAddGroup.toSeminormedAddGroup : {E : Type u_5} → [NormedAddGroup E] → SeminormedAddGroup E
-- Mathlib.Order.SymmDiff
symmDiff_left_inj : ∀ {α : Type u_2} [inst : GeneralizedBooleanAlgebra α] {a b c : α}, symmDiff a b = symmDiff c b ↔ a = c
-- Mathlib.RingTheory.Ideal.Quotient.Operations
/-- The **first isomorphism theorem** for algebras.  -/
Ideal.quotientKerAlgEquivOfSurjective : {R₁ : Type u_1} →
  {A : Type u_3} →
    {B : Type u_4} →
      [inst : CommSemiring R₁] →
        [inst_1 : Ring A] →
          [inst_2 : Algebra R₁ A] →
            [inst_3 : Semiring B] →
              [inst_4 : Algebra R₁ B] → {f : A →ₐ[R₁] B} → Function.Surjective ⇑f → (A ⧸ RingHom.ker f) ≃ₐ[R₁] B
-- Init.Data.UInt.Lemmas
UInt64.ofNat_div : ∀ {a b : ℕ}, a < 2 ^ 64 → b < 2 ^ 64 → UInt64.ofNat (a / b) = UInt64.ofNat a / UInt64.ofNat b
-- Mathlib.Algebra.CubicDiscriminant
Cubic.card_roots_of_discr_ne_zero : ∀ {F : Type u_3} {K : Type u_4} {P : Cubic F} [inst : Field F] [inst_1 : Field K] {φ : F →+* K}
  [inst_2 : DecidableEq K],
  P.a ≠ 0 → (Polynomial.map φ P.toPoly).Splits → P.discr ≠ 0 → (Cubic.map φ P).roots.toFinset.card = 3
-- Mathlib.CategoryTheory.FiberedCategory.Fibered
CategoryTheory.Functor.IsFibered.comp : ∀ {𝒮 : Type u₁} {𝒳 : Type u₂} {inst : CategoryTheory.Category.{v₁, u₁} 𝒮} {inst_1 : CategoryTheory.Category.{v₂, u₂} 𝒳}
  {p : CategoryTheory.Functor 𝒳 𝒮} [self : p.IsFibered] {R S T : 𝒮} (f : R ⟶ S) (g : S ⟶ T) {a b c : 𝒳} (φ : a ⟶ b)
  (ψ : b ⟶ c) [p.IsCartesian f φ] [p.IsCartesian g ψ],
  p.IsCartesian (CategoryTheory.CategoryStruct.comp f g) (CategoryTheory.CategoryStruct.comp φ ψ)