mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.RingTheory.DedekindDomain.Different
differentialIdeal_le_fractionalIdeal_iff : ∀ {A : Type u_1} {K : Type u_2} {L : Type u} {B : Type u_3} [inst : CommRing A] [inst_1 : Field K] [inst_2 : CommRing B]
  [inst_3 : Field L] [inst_4 : Algebra A K] [inst_5 : Algebra B L] [inst_6 : Algebra A B] [inst_7 : Algebra K L]
  [inst_8 : Algebra A L] [inst_9 : IsScalarTower A K L] [inst_10 : IsScalarTower A B L] [inst_11 : IsDomain A]
  [IsFractionRing A K] [FiniteDimensional K L] [Algebra.IsSeparable K L] [IsIntegralClosure B A L]
  [IsIntegrallyClosed A] [inst_17 : IsDedekindDomain B] [inst_18 : Module.IsTorsionFree A B]
  [inst_19 : IsFractionRing B L] {I : FractionalIdeal (nonZeroDivisors B) L},
  I ≠ 0 → (↑(differentIdeal A B) ≤ I ↔ Submodule.map (↑A (Algebra.trace K L)) (Submodule.restrictScalars A ↑I⁻¹) ≤ 1)
-- Batteries.Data.Fin.Coding
_private.Batteries.Data.Fin.Coding.0.Fin.encodePi.match_1.splitter : (n : ℕ) → (motive : Fin n → Sort u_1) → (x : Fin n) → ((i : ℕ) → (hi : i < n) → motive ⟨i, hi⟩) → motive x
-- Mathlib.Order.Filter.Tendsto
Filter.map_mapsTo_Iic_iff_mapsTo : ∀ {α : Type u_1} {β : Type u_2} {s : Set α} {t : Set β} {m : α → β},
  Set.MapsTo (Filter.map m) (Set.Iic (Filter.principal s)) (Set.Iic (Filter.principal t)) ↔ Set.MapsTo m s t
-- Mathlib.Algebra.Order.Interval.Basic
NonemptyInterval.toProd_nsmul : ∀ {α : Type u_2} [inst : AddMonoid α] [inst_1 : Preorder α] [inst_2 : AddLeftMono α] [inst_3 : AddRightMono α]
  (s : NonemptyInterval α) (n : ℕ), (n • s).toProd = n • s.toProd
-- Mathlib.Combinatorics.Additive.VerySmallDoubling
_private.Mathlib.Combinatorics.Additive.VerySmallDoubling.0.Finset.subgroup_strong_bound_right : ∀ {G : Type u_1} [inst : Group G] [inst_1 : DecidableEq G] {A : Finset G},
  ↑(A * A).card < 3 / 2 * ↑A.card → ∀ a ∈ A, a • MulOpposite.op a • (A⁻¹ * A) ⊆ A * A
-- Mathlib.CategoryTheory.WithTerminal.Basic
CategoryTheory.WithTerminal.opEquiv_counitIso_hom_app : ∀ (C : Type u) [inst : CategoryTheory.Category.{v, u} C] (X : CategoryTheory.WithInitial Cᵒᵖ),
  (CategoryTheory.WithTerminal.opEquiv C).counitIso.hom.app X =
    (match X with
      | CategoryTheory.WithInitial.of x => CategoryTheory.Iso.refl (CategoryTheory.WithInitial.of x)
      | CategoryTheory.WithInitial.star => CategoryTheory.Iso.refl CategoryTheory.WithInitial.star).hom
-- Init.Data.Int.DivMod.Lemmas
Int.ediv_mul : ∀ {x y z : ℤ}, x / (y * z) = x / y / z + if y < 0 ∧ ¬z ∣ x / y then z.sign else 0
-- Mathlib.GroupTheory.GroupExtension.Basic
/-- `N`-conjugacy is symmetric.  -/
GroupExtension.IsConj.symm : ∀ {N : Type u_1} {G : Type u_2} [inst : Group N] [inst_1 : Group G] {E : Type u_3} [inst_2 : Group E]
  (S : GroupExtension N E G) {s₁ s₂ : S.Splitting}, S.IsConj s₁ s₂ → S.IsConj s₂ s₁
-- Mathlib.Order.ConditionallyCompleteLattice.Basic
csSup_empty : ∀ {α : Type u_1} [inst : ConditionallyCompleteLinearOrderBot α], sSup ∅ = ⊥
-- Mathlib.CategoryTheory.Enriched.Basic
CategoryTheory.EnrichedCategory.comp_id : ∀ {V : Type v} {inst : CategoryTheory.Category.{w, v} V} {inst_1 : CategoryTheory.MonoidalCategory V} {C : Type u₁}
  [self : CategoryTheory.EnrichedCategory V C] (X Y : C),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.rightUnitor (X ⟶[V] Y)).inv
      (CategoryTheory.CategoryStruct.comp
        (CategoryTheory.MonoidalCategoryStruct.whiskerLeft (X ⟶[V] Y) (CategoryTheory.EnrichedCategory.id Y))
        (CategoryTheory.EnrichedCategory.comp X Y Y)) =
    CategoryTheory.CategoryStruct.id (X ⟶[V] Y)
-- Mathlib.Algebra.Polynomial.Basic
Polynomial.coeff_monomial : ∀ {R : Type u} {a : R} {m n : ℕ} [inst : Semiring R], ((Polynomial.monomial n) a).coeff m = if n = m then a else 0
-- Mathlib.Algebra.Lie.Free
FreeLieAlgebra.instZero : (R : Type u) → (X : Type v) → [inst : CommRing R] → Zero (FreeLieAlgebra R X)
-- Mathlib.Topology.UniformSpace.Cauchy
totallyBounded_interUnionBalls : ∀ {α : Type u} [uniformSpace : UniformSpace α] {p : ℕ → Prop} {U : ℕ → SetRel α α},
  (uniformity α).HasBasis p U → ∀ (xs : ℕ → α) (u : ℕ → ℕ), TotallyBounded (interUnionBalls xs u U)
-- Mathlib.Data.Set.Prod
Equiv.piCongrLeft_preimage_univ_pi : ∀ {ι : Type u_1} {ι' : Type u_2} {α : ι → Type u_3} (f : ι' ≃ ι) (t : (i : ι) → Set (α i)),
  ⇑(Equiv.piCongrLeft α f) ⁻¹' Set.univ.pi t = Set.univ.pi fun i => t (f i)
-- Init.Data.Bool
Bool.bne_self_right : ∀ (a b : Bool), ((a != b) != b) = a
-- Mathlib.AlgebraicTopology.SimplicialSet.AnodyneExtensions.UnionProd
SSet.prodStdSimplex.pairingCore.IsType₂.type₁_x : ∀ {m : ℕ} {k : Fin (m + 1)} {n : ℕ} {x : ((SSet.horn (m + 1) k.castSucc).unionProd (SSet.boundary n)).N}
  (hx : SSet.prodStdSimplex.pairingCore.IsType₂ x) {d : ℕ} (hd : x.dim = d),
  (hx.type₁ hd).x = SSet.Subcomplex.N.mk (hx.simplex hd) ⋯ ⋯
-- Mathlib.CategoryTheory.Functor.KanExtension.Adjunction
CategoryTheory.Functor.ranCompLimIso_hom_app : ∀ {C : Type u_1} {D : Type u_2} [inst : CategoryTheory.Category.{v_1, u_1} C]
  [inst_1 : CategoryTheory.Category.{v_2, u_2} D] {H : Type u_3} [inst_2 : CategoryTheory.Category.{v_3, u_3} H]
  (L : CategoryTheory.Functor C D) [inst_3 : ∀ (G : CategoryTheory.Functor C H), L.HasRightKanExtension G]
  [inst_4 : CategoryTheory.Limits.HasLimitsOfShape C H] [inst_5 : CategoryTheory.Limits.HasLimitsOfShape D H]
  (X : CategoryTheory.Functor C H),
  L.ranCompLimIso.hom.app X = ((L.ran.obj X).limitIsoOfIsRightKanExtension (L.ranCounit.app X)).hom
-- Mathlib.Tactic.ComputeAsymptotics.Multiseries.Monomial.Basic
Tactic.ComputeAsymptotics.Monomial.inv_length : ∀ (t : Tactic.ComputeAsymptotics.Monomial), List.length t.inv.unit = List.length t.unit
-- Init.Data.String.Lemmas.Basic
String.Slice.Pos.sliceTo_eq_endPos : ∀ {s : String.Slice} {p : s.Pos}, p.sliceTo p ⋯ = (s.sliceTo p).endPos
-- Mathlib.Algebra.Homology.ShortComplex.Homology
/-- Given a short complex `S` such that `S.HasHomology`, this is the canonical
right homology data for `S` whose `Q` and `H` fields are
respectively `S.opcycles` and `S.homology`.  -/
CategoryTheory.ShortComplex.RightHomologyData.canonical : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C] →
      (S : CategoryTheory.ShortComplex C) → [S.HasHomology] → S.RightHomologyData
-- Std.Do.SPred.SPred
Std.Do.SPred.entails_nil_pure_intro : ∀ {φ : Prop} {Q : Std.Do.SPred []}, (φ → Q.down) → ⌜φ⌝ ⊢ₛ Q
-- Init.Prelude
/-- The bytes of the UTF-8 encoding of the string. Since strings have a special representation in
the runtime, this function actually takes linear time and space at runtime. For efficient access
to the string's bytes, use `String.utf8ByteSize` and `String.getUTF8Byte`.  -/
String.toByteArray : String → ByteArray
-- Mathlib.Topology.VectorBundle.FiniteDimensional
VectorBundle.finrank_eq : ∀ (R : Type u_1) {B : Type u_2} (F : Type u_3) (E : B → Type u_4) [inst : NontriviallyNormedField R]
  [inst_1 : TopologicalSpace B] [inst_2 : TopologicalSpace (Bundle.TotalSpace F E)] [inst_3 : NormedAddCommGroup F]
  [inst_4 : NormedSpace R F] [inst_5 : (x : B) → TopologicalSpace (E x)] [inst_6 : FiberBundle F E]
  [inst_7 : (x : B) → AddCommGroup (E x)] [inst_8 : (x : B) → Module R (E x)] [VectorBundle R F E] (b : B),
  Module.finrank R (E b) = Module.finrank R F
-- Lean.Meta.Tactic.Simp.BuiltinSimprocs.Fin
_private.Lean.Meta.Tactic.Simp.BuiltinSimprocs.Fin.0.Fin.Value.mk.inj : ∀ {n : ℕ} {value : Fin n} {n_1 : ℕ} {value_1 : Fin n_1},
  { n := n, value := value } = { n := n_1, value := value_1 } → n = n_1 ∧ value ≍ value_1
-- Lean.Widget.InteractiveGoal
Lean.Widget.InteractiveGoal.mk.injEq : ∀ (toInteractiveGoalCore : Lean.Widget.InteractiveGoalCore) (userName? : Option String) (goalPrefix : String)
  (mvarId : Lean.MVarId) (isInserted? isRemoved? : Option Bool)
  (toInteractiveGoalCore_1 : Lean.Widget.InteractiveGoalCore) (userName?_1 : Option String) (goalPrefix_1 : String)
  (mvarId_1 : Lean.MVarId) (isInserted?_1 isRemoved?_1 : Option Bool),
  ({ toInteractiveGoalCore := toInteractiveGoalCore, userName? := userName?, goalPrefix := goalPrefix, mvarId := mvarId,
        isInserted? := isInserted?, isRemoved? := isRemoved? } =
      { toInteractiveGoalCore := toInteractiveGoalCore_1, userName? := userName?_1, goalPrefix := goalPrefix_1,
        mvarId := mvarId_1, isInserted? := isInserted?_1, isRemoved? := isRemoved?_1 }) =
    (toInteractiveGoalCore = toInteractiveGoalCore_1 ∧
      userName? = userName?_1 ∧
        goalPrefix = goalPrefix_1 ∧ mvarId = mvarId_1 ∧ isInserted? = isInserted?_1 ∧ isRemoved? = isRemoved?_1)
-- Mathlib.Topology.Inseparable
stableUnderSpecialization_iUnion : ∀ {X : Type u_1} [inst : TopologicalSpace X] {ι : Sort u_7} (S : ι → Set X),
  (∀ (i : ι), StableUnderSpecialization (S i)) → StableUnderSpecialization (⋃ i, S i)
-- Mathlib.MeasureTheory.Measure.Lebesgue.Basic
Real.volume_pi_Ioo_toReal : ∀ {ι : Type u_1} [inst : Fintype ι] {a b : ι → ℝ},
  a ≤ b → (MeasureTheory.volume (Set.univ.pi fun i => Set.Ioo (a i) (b i))).toReal = ∏ i, (b i - a i)
-- Mathlib.CategoryTheory.Adjunction.Unique
CategoryTheory.Adjunction.leftAdjointUniq_hom_counit_assoc : ∀ {C : Type u_1} {D : Type u_2} [inst : CategoryTheory.Category.{v_1, u_1} C]
  [inst_1 : CategoryTheory.Category.{v_2, u_2} D] {F F' : CategoryTheory.Functor C D} {G : CategoryTheory.Functor D C}
  (adj1 : F ⊣ G) (adj2 : F' ⊣ G) {Z : CategoryTheory.Functor D D} (h : CategoryTheory.Functor.id D ⟶ Z),
  CategoryTheory.CategoryStruct.comp (G.whiskerLeft (adj1.leftAdjointUniq adj2).hom)
      (CategoryTheory.CategoryStruct.comp adj2.counit h) =
    CategoryTheory.CategoryStruct.comp adj1.counit h
-- Mathlib.LinearAlgebra.Dual.Defs
/-- Given a linear map `f : M₁ →ₗ[R] M₂`, `f.dualMap` is the linear map between the dual of
`M₂` and `M₁` such that it maps the functional `φ` to `φ ∘ f`.  -/
LinearMap.dualMap : {R : Type u_1} →
  {M₁ : Type u_2} →
    {M₂ : Type u_3} →
      [inst : CommSemiring R] →
        [inst_1 : AddCommMonoid M₁] →
          [inst_2 : Module R M₁] →
            [inst_3 : AddCommMonoid M₂] →
              [inst_4 : Module R M₂] → (M₁ →ₗ[R] M₂) → Module.Dual R M₂ →ₗ[R] Module.Dual R M₁
-- Mathlib.Logic.Equiv.Prod
/-- A product of copies of a type can be split as the binary product of one copy and the product
of all the remaining copies.  -/
Equiv.funSplitAt : {α : Type u_9} → [DecidableEq α] → (i : α) → (β : Type u_10) → (α → β) ≃ β × ({ j // j ≠ i } → β)
-- Init.Data.Array.Basic
/-- Folds a monadic function over an array from the right, accumulating a value starting with `init`.
The accumulated value is combined with the each element of the list in reverse order, using `f`.

The optional parameters `start` and `stop` control the region of the array to be folded. Folding
proceeds from `start` (exclusive) to `stop` (inclusive), so no folding occurs unless `start > stop`.
By default, the entire array is folded.

Examples:
```lean example
example [Monad m] (f : α → β → m β) :
  Array.foldrM (m := m) f x₀ #[a, b, c] = (do
    let x₁ ← f c x₀
    let x₂ ← f b x₁
    let x₃ ← f a x₂
    pure x₃)
  := by rfl
```

```lean example
example [Monad m] (f : α → β → m β) :
  Array.foldrM (m := m) f x₀ #[a, b, c] (start := 2) = (do
    let x₁ ← f b x₀
    let x₂ ← f a x₁
    pure x₂)
  := by rfl
```
 -/
Array.foldrM : {α : Type u} →
  {β : Type v} →
    {m : Type v → Type w} → [Monad m] → (α → β → m β) → β → (as : Array α) → optParam ℕ as.size → optParam ℕ 0 → m β
-- Init.Grind.Order
Lean.Grind.Order.le_lt_trans : ∀ {α : Type u_1} [inst : LE α] [inst_1 : LT α] [Std.LawfulOrderLT α] [Std.IsPreorder α] {a b c : α},
  a ≤ b → b < c → a < c
-- Mathlib.Algebra.Homology.ShortComplex.LeftHomology
CategoryTheory.ShortComplex.leftHomologyπ_naturality'_assoc : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  {S₁ S₂ : CategoryTheory.ShortComplex C} (φ : S₁ ⟶ S₂) (h₁ : S₁.LeftHomologyData) (h₂ : S₂.LeftHomologyData) {Z : C}
  (h : h₂.H ⟶ Z),
  CategoryTheory.CategoryStruct.comp h₁.π
      (CategoryTheory.CategoryStruct.comp (CategoryTheory.ShortComplex.leftHomologyMap' φ h₁ h₂) h) =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.ShortComplex.cyclesMap' φ h₁ h₂)
      (CategoryTheory.CategoryStruct.comp h₂.π h)
-- Mathlib.MeasureTheory.Function.AEEqFun
MeasureTheory.AEEqFun.ext : ∀ {α : Type u_1} {β : Type u_2} [inst : MeasurableSpace α] {μ : MeasureTheory.Measure α} [inst_1 : TopologicalSpace β]
  {f g : α →ₘ[μ] β}, ↑f =ᵐ[μ] ↑g → f = g
-- Mathlib.CategoryTheory.Limits.Shapes.WidePullbacks
CategoryTheory.Limits.WidePullbackShape.struct : {J : Type w} → CategoryTheory.CategoryStruct.{w, w} (CategoryTheory.Limits.WidePullbackShape J)
-- Mathlib.Algebra.Ring.Subsemiring.Defs
Subsemiring.copy_toSubmonoid : ∀ {R : Type u} [inst : NonAssocSemiring R] (S : Subsemiring R) (s : Set R) (hs : s = ↑S),
  (S.copy s hs).toSubmonoid = { carrier := s, mul_mem' := ⋯, one_mem' := ⋯ }
-- Mathlib.ModelTheory.ElementarySubstructures
FirstOrder.Language.ElementarySubstructure.mk : {L : FirstOrder.Language} →
  {M : Type u_1} →
    [inst : L.Structure M] →
      (toSubstructure : L.Substructure M) → toSubstructure.IsElementary → L.ElementarySubstructure M
-- Mathlib.RingTheory.Extension.Presentation.Submersive
Algebra.PreSubmersivePresentation.baseChange_ring : ∀ {R : Type u} {S : Type v} {ι : Type w} {σ : Type t} [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : Algebra R S]
  (P : Algebra.PreSubmersivePresentation R S ι σ), (Algebra.PreSubmersivePresentation.baseChange R P).Ring = P.Ring
-- Mathlib.RepresentationTheory.Continuous.Basic
/-- The composition of two continuous intertwining maps is a continuous intertwining map.  -/
ContIntertwiningMap.comp : {R : Type u_1} →
  {G : Type u_2} →
    {V : Type u_3} →
      {W : Type u_4} →
        {U : Type u_5} →
          [inst : Monoid G] →
            [inst_1 : Ring R] →
              [inst_2 : AddCommGroup V] →
                [inst_3 : TopologicalSpace V] →
                  [inst_4 : IsTopologicalAddGroup V] →
                    [inst_5 : Module R V] →
                      [inst_6 : AddCommGroup W] →
                        [inst_7 : TopologicalSpace W] →
                          [inst_8 : IsTopologicalAddGroup W] →
                            [inst_9 : Module R W] →
                              [inst_10 : AddCommGroup U] →
                                [inst_11 : Module R U] →
                                  [inst_12 : TopologicalSpace U] →
                                    [inst_13 : IsTopologicalAddGroup U] →
                                      {π₁ : ContRepresentation R G V} →
                                        {π₂ : ContRepresentation R G W} →
                                          {π₃ : ContRepresentation R G U} →
                                            ContIntertwiningMap π₂ π₃ →
                                              ContIntertwiningMap π₁ π₂ → ContIntertwiningMap π₁ π₃
-- Init.Data.String.Iterate
String.Slice.RevByteIterator.instFiniteUInt8 : ∀ {m : Type → Type u_1} [inst : Pure m], Std.Iterators.Finite String.Slice.RevByteIterator m
-- Mathlib.Combinatorics.SimpleGraph.Walk.Subwalks
SimpleGraph.Walk.IsSubwalk.map : ∀ {V : Type u_1} {G G' : SimpleGraph V} {u v u' v' : V} {p₁ : G.Walk u v} {p₂ : G.Walk u' v'},
  p₂.IsSubwalk p₁ → ∀ (f : G →g G'), (SimpleGraph.Walk.map f p₂).IsSubwalk (SimpleGraph.Walk.map f p₁)
-- Mathlib.CategoryTheory.ObjectProperty.Small
CategoryTheory.ObjectProperty.instSmallOppositeOp_1 : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] (P : CategoryTheory.ObjectProperty C)
  [CategoryTheory.ObjectProperty.Small.{w, v, u} P], CategoryTheory.ObjectProperty.Small.{w, v, u} P.op
-- Mathlib.Algebra.Order.Monoid.Unbundled.Basic
AddLECancellable.le_add_iff_nonneg_right : ∀ {α : Type u_1} [inst : LE α] [inst_1 : AddZeroClass α] [AddLeftMono α] {a b : α},
  AddLECancellable a → (a ≤ a + b ↔ 0 ≤ b)
-- Mathlib.Analysis.SpecialFunctions.Complex.Arg
Complex.arg_neg_eq_arg_add_pi_of_im_neg : ∀ {x : ℂ}, x.im < 0 → (-x).arg = x.arg + Real.pi
-- Mathlib.Combinatorics.Hypergraph.Basic
Hypergraph.mk.inj : ∀ {α : Type u_4} {vertexSet : Set α} {edgeSet : Set (Set α)}
  {subset_vertexSet_of_mem_edgeSet' : ∀ ⦃e : Set α⦄, e ∈ edgeSet → e ⊆ vertexSet} {vertexSet_1 : Set α}
  {edgeSet_1 : Set (Set α)} {subset_vertexSet_of_mem_edgeSet'_1 : ∀ ⦃e : Set α⦄, e ∈ edgeSet_1 → e ⊆ vertexSet_1},
  { vertexSet := vertexSet, edgeSet := edgeSet, subset_vertexSet_of_mem_edgeSet' := subset_vertexSet_of_mem_edgeSet' } =
      { vertexSet := vertexSet_1, edgeSet := edgeSet_1,
        subset_vertexSet_of_mem_edgeSet' := subset_vertexSet_of_mem_edgeSet'_1 } →
    vertexSet = vertexSet_1 ∧ edgeSet = edgeSet_1
-- Mathlib.Order.Interval.Set.LinearOrder
Set.Ioc_union_Ici_eq_Ioi : ∀ {α : Type u_1} [inst : LinearOrder α] {a b : α}, a < b → Set.Ioc a b ∪ Set.Ici b = Set.Ioi a
-- Mathlib.Algebra.Algebra.Subalgebra.Lattice
Algebra.mem_adjoin_iff : ∀ {R : Type uR} {A : Type uA} [inst : CommRing R] [inst_1 : Ring A] [inst_2 : Algebra R A] {s : Set A} {x : A},
  x ∈ Algebra.adjoin R s ↔ x ∈ Subring.closure (Set.range ⇑(algebraMap R A) ∪ s)
-- Mathlib.GroupTheory.Congruence.Defs
/-- The infimum of a set of congruence relations on a given type with a multiplication.  -/
Con.instInfSet : {M : Type u_1} → [inst : Mul M] → InfSet (Con M)
-- Mathlib.CategoryTheory.Bicategory.Span.Basic
/-- Construct an isomorphism of spans from an isomorphism between the
apices that is compatible with the projections.  -/
CategoryTheory.Span.mkIso : {C : Type u_1} →
  [inst : CategoryTheory.Category.{v_1, u_1} C] →
    {Wₗ Wᵣ : CategoryTheory.MorphismProperty C} →
      {c c' : C} →
        {S S' : CategoryTheory.Span Wₗ Wᵣ c c'} →
          (e : S.apex ≅ S'.apex) →
            autoParam (CategoryTheory.CategoryStruct.comp e.hom S'.l = S.l) CategoryTheory.Span.mkIso._auto_1 →
              autoParam (CategoryTheory.CategoryStruct.comp e.hom S'.r = S.r) CategoryTheory.Span.mkIso._auto_3 →
                (S ≅ S')
-- Init.Data.Option.Lemmas
Option.guard_comp : ∀ {α : Type u_1} {β : Type u_2} {p : α → Bool} {f : β → α}, Option.guard p ∘ f = Option.map f ∘ Option.guard (p ∘ f)
-- Mathlib.Topology.Algebra.Group.Defs
ContinuousNeg.continuous_neg : ∀ {G : Type u} {inst : TopologicalSpace G} {inst_1 : Neg G} [self : ContinuousNeg G], Continuous fun a => -a
-- Mathlib.CategoryTheory.ComposableArrows.Basic
/-- Constructor for `ComposableArrows C 0`.  -/
CategoryTheory.ComposableArrows.mk₀ : {C : Type u_1} → [inst : CategoryTheory.Category.{v_1, u_1} C] → C → CategoryTheory.ComposableArrows C 0
-- Mathlib.Probability.Distributions.SetBernoulli
ProbabilityTheory.setBernoulli_real_singleton : ∀ {ι : Type u_1} {s u : Set ι} [Countable ι] (p : ↑unitInterval),
  s ⊆ u → u.Finite → (ProbabilityTheory.setBernoulli u p).real {s} = ↑p ^ s.ncard * (1 - ↑p) ^ (u \ s).ncard
-- Mathlib.LinearAlgebra.Dimension.StrongRankCondition
/-- Over any ring `R` satisfying the strong rank condition,
if `b` is a basis for a module `M`,
and `s` is a linearly independent set,
then the cardinality of `s` is bounded by the cardinality of `b`.
 -/
linearIndependent_le_basis : ∀ {R : Type u} {M : Type v} [inst : Semiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M] [StrongRankCondition R]
  {ι : Type w} (b : Module.Basis ι R M) {κ : Type w} (v : κ → M), LinearIndependent R v → Cardinal.mk κ ≤ Cardinal.mk ι
-- Mathlib.MeasureTheory.Measure.DiracProba
/-- In a completely regular T0 topological space `X`, `diracProbaEquiv` is a homeomorphism to
its image in `ProbabilityMeasure X`.  -/
MeasureTheory.diracProbaHomeomorph : {X : Type u_1} →
  [inst : MeasurableSpace X] →
    [inst_1 : TopologicalSpace X] →
      [inst_2 : OpensMeasurableSpace X] →
        [T0Space X] → [CompletelyRegularSpace X] → X ≃ₜ ↑(Set.range MeasureTheory.diracProba)
-- Mathlib.CategoryTheory.Monoidal.Grp
CategoryTheory.Grp.forget₂Mon_obj_one : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.CartesianMonoidalCategory C]
  (A : CategoryTheory.Grp C), CategoryTheory.MonObj.one = CategoryTheory.MonObj.one
-- Mathlib.Topology.ContinuousMap.CocompactMap
CocompactMap.mk : {α : Type u} →
  {β : Type v} →
    [inst : TopologicalSpace α] →
      [inst_1 : TopologicalSpace β] →
        (toContinuousMap : C(α, β)) →
          Filter.Tendsto toContinuousMap.toFun (Filter.cocompact α) (Filter.cocompact β) → CocompactMap α β
-- Mathlib.Topology.Order.LeftRightNhds
orderTopology_of_nhds_abs : ∀ {α : Type u_4} [inst : TopologicalSpace α] [inst_1 : AddCommGroup α] [inst_2 : LinearOrder α] [IsOrderedAddMonoid α],
  (∀ (a : α), nhds a = ⨅ r, ⨅ (_ : r > 0), Filter.principal {b | |a - b| < r}) → OrderTopology α
-- Mathlib.Algebra.Group.Shrink
Shrink.instNSMul.eq_1 : ∀ {M : Type u_1} {α : Type u_2} [inst : Small.{v, u_2} α] [inst_1 : SMul M α],
  Shrink.instNSMul = Equiv.smul M (equivShrink α).symm
-- Mathlib.Topology.Compactness.CompactlyCoherentSpace
CompactCoherentification.continuous_mk_symm : ∀ {X : Type u_1} [inst : TopologicalSpace X], Continuous ⇑(CompactCoherentification.mk X).symm
-- Mathlib.Algebra.Group.Action.Pointwise.Set.Basic
Set.smul_set_inter : ∀ {α : Type u_2} {β : Type u_3} [inst : Group α] [inst_1 : MulAction α β] {s t : Set β} {a : α},
  a • (s ∩ t) = a • s ∩ a • t
-- Mathlib.Analysis.Asymptotics.Defs
/-- **Alias** of the reverse direction of `Asymptotics.isLittleO_neg_left`. -/
Asymptotics.IsLittleO.neg_left : ∀ {α : Type u_1} {F : Type u_4} {E' : Type u_6} [inst : Norm F] [inst_1 : SeminormedAddCommGroup E'] {g : α → F}
  {f' : α → E'} {l : Filter α}, f' =o[l] g → (fun x => -f' x) =o[l] g
-- Mathlib.Algebra.Algebra.NonUnitalSubalgebra
NonUnitalSubalgebra.ext : ∀ {R : Type u} {A : Type v} [inst : CommSemiring R] [inst_1 : NonUnitalNonAssocSemiring A] [inst_2 : Module R A]
  {S T : NonUnitalSubalgebra R A}, (∀ (x : A), x ∈ S ↔ x ∈ T) → S = T
-- Mathlib.CategoryTheory.Limits.Preserves.Opposites
/-- If `F.unop : C ⥤ D` reflects colimits of `K.leftOp : Jᵒᵖ ⥤ C`, then `F : Cᵒᵖ ⥤ Dᵒᵖ` reflects
limits of `K : J ⥤ Cᵒᵖ`.  -/
CategoryTheory.Limits.reflectsLimit_of_unop : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  {J : Type w} [inst_2 : CategoryTheory.Category.{w', w} J] (K : CategoryTheory.Functor J Cᵒᵖ)
  (F : CategoryTheory.Functor Cᵒᵖ Dᵒᵖ) [CategoryTheory.Limits.ReflectsColimit K.leftOp F.unop],
  CategoryTheory.Limits.ReflectsLimit K F
-- Mathlib.CategoryTheory.Monoidal.Rigid.Basic
CategoryTheory.tensorRightHomEquiv_symm_coevaluation_comp_whiskerLeft : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.MonoidalCategory C] {X Y : C}
  [inst_2 : CategoryTheory.HasLeftDual X] [inst_3 : CategoryTheory.HasLeftDual Y] (f : X ⟶ Y),
  (CategoryTheory.tensorRightHomEquiv (CategoryTheory.MonoidalCategoryStruct.tensorUnit C) (ᘁY) Y ᘁX).symm
      (CategoryTheory.CategoryStruct.comp (η_ (ᘁX) X) (CategoryTheory.MonoidalCategoryStruct.whiskerLeft (ᘁX) f)) =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.leftUnitor ᘁY).hom (ᘁf)
-- Mathlib.Algebra.Lie.Weights.Basic
/-- See also `bourbaki1975b` Chapter VII §1.1, Proposition 2 (ii).  -/
LieModule.weight_vector_multiplication : ∀ {R : Type u_2} {L : Type u_3} [inst : CommRing R] [inst_1 : LieRing L] [inst_2 : LieAlgebra R L] (M₁ : Type u_5)
  (M₂ : Type u_6) (M₃ : Type u_7) [inst_3 : AddCommGroup M₁] [inst_4 : Module R M₁] [inst_5 : LieRingModule L M₁]
  [inst_6 : LieModule R L M₁] [inst_7 : AddCommGroup M₂] [inst_8 : Module R M₂] [inst_9 : LieRingModule L M₂]
  [inst_10 : LieModule R L M₂] [inst_11 : AddCommGroup M₃] [inst_12 : Module R M₃] [inst_13 : LieRingModule L M₃]
  [inst_14 : LieModule R L M₃] (g : TensorProduct R M₁ M₂ →ₗ⁅R,L⁆ M₃) (χ₁ χ₂ : R) (x : L),
  (↑g ∘ₗ
        TensorProduct.mapIncl (((LieModule.toEnd R L M₁) x).maxGenEigenspace χ₁)
          (((LieModule.toEnd R L M₂) x).maxGenEigenspace χ₂)).range ≤
    ((LieModule.toEnd R L M₃) x).maxGenEigenspace (χ₁ + χ₂)
-- Std.Do.Triple.SpecLemmas
Std.Do.Spec.throw_ReaderT : ∀ {m : Type u → Type v} {sh : Std.Do.PostShape} {ε : Type u_1} {ρ α : Type u} {e : ε}
  {Q : Std.Do.PostCond α (Std.Do.PostShape.arg ρ sh)} [inst : Std.Do.WP m sh] [inst_1 : MonadExceptOf ε m],
  ⦃(Std.Do.wp (MonadLift.monadLift (MonadExceptOf.throw e))).apply Q⦄ MonadExceptOf.throw e ⦃Q⦄