mathlib-initiative/mathlib-types huggingface dataset:
-- Init.Data.Iterators.Lemmas.Combinators.FilterMap
_private.Init.Data.Iterators.Lemmas.Combinators.FilterMap.0.Std.IterM.step_filterMap.match_1.eq_2 : ∀ {β' : Type u_1} (motive : Option β' → Sort u_2) (out' : β') (h_1 : some out' = none → motive none)
  (h_2 : (out'_1 : β') → some out' = some out'_1 → motive (some out'_1)),
  (match h' : some out' with
    | none => h_1 h'
    | some out'_1 => h_2 out'_1 h') =
    h_2 out' ⋯
-- Mathlib.Algebra.Algebra.Subalgebra.Basic
SubalgebraClass.coe_val : ∀ {S : Type u_1} {R : Type u_2} {A : Type u_3} [inst : CommSemiring R] [inst_1 : Semiring A] [inst_2 : Algebra R A]
  [inst_3 : SetLike S A] [inst_4 : SubsemiringClass S A] [hSR : SMulMemClass S R A] (s : S),
  ⇑(SubalgebraClass.val s) = Subtype.val
-- Mathlib.CategoryTheory.Category.Pairwise
CategoryTheory.Pairwise.single.inj : ∀ {ι : Type v} {a a_1 : ι}, CategoryTheory.Pairwise.single a = CategoryTheory.Pairwise.single a_1 → a = a_1
-- Mathlib.RingTheory.GradedAlgebra.HomogeneousLocalization
/-- This is strictly weaker than `Away.adjoin_mk_prod_pow_eq_top`.  -/
_private.Mathlib.RingTheory.GradedAlgebra.HomogeneousLocalization.0.HomogeneousLocalization.Away.adjoin_mk_prod_pow_eq_top_of_pos : ∀ {A : Type u_2} {σ : Type u_3} [inst : CommRing A] [inst_1 : SetLike σ A] [inst_2 : AddSubgroupClass σ A] {𝒜 : ℕ → σ}
  [inst_3 : GradedRing 𝒜] {f : A} {d : ℕ} (hf : f ∈ 𝒜 d) {ι' : Type u_4} [inst_4 : Fintype ι'] (v : ι' → A),
  Algebra.adjoin (↥(𝒜 0)) (Set.range v) = ⊤ →
    ∀ (dv : ι' → ℕ) (hxd : ∀ (i : ι'), v i ∈ 𝒜 (dv i)),
      (∀ (i : ι'), 0 < dv i) →
        Algebra.adjoin ↥(𝒜 0)
            {x |
              ∃ a ai,
                ∃ (hai : ∑ i, ai i • dv i = a • d) (_ : ∀ (i : ι'), ai i ≤ d),
                  HomogeneousLocalization.Away.mk 𝒜 hf a (∏ i, v i ^ ai i) ⋯ = x} =
          ⊤
-- Mathlib.Algebra.Group.Units.Equiv
Equiv.symm_divLeft : ∀ {G : Type u_5} [inst : CommGroup G] (a : G), (Equiv.divLeft a).symm = Equiv.divLeft a
-- Mathlib.RingTheory.Jacobson.Ring
/-- If `R` is a Jacobson ring, then maximal ideals in the localization at `y`
correspond to maximal ideals in the original ring `R` that don't contain `y`.
This lemma gives the correspondence in the particular case of an ideal and its comap.
See `le_relIso_of_maximal` for the more general relation isomorphism  -/
IsLocalization.isMaximal_iff_isMaximal_disjoint : ∀ {R : Type u_1} (S : Type u_2) [inst : CommRing R] [inst_1 : CommRing S] (y : R) [inst_2 : Algebra R S]
  [IsLocalization.Away y S] [H : IsJacobsonRing R] (J : Ideal S),
  J.IsMaximal ↔ (Ideal.under R J).IsMaximal ∧ y ∉ Ideal.under R J
-- Batteries.Data.Fin.Coding
_private.Batteries.Data.Fin.Coding.0.Fin.decodeOption.match_1.eq_1 : ∀ {n : ℕ} (motive : Fin (n + 1) → Sort u_1) (h_1 : Unit → motive ⟨0, ⋯⟩)
  (h_2 : (i : ℕ) → (h : i + 1 < n + 1) → motive ⟨i.succ, h⟩),
  (match ⟨0, ⋯⟩ with
    | ⟨0, ⋯⟩ => h_1 ()
    | ⟨i.succ, h⟩ => h_2 i h) =
    h_1 ()
-- Mathlib.Algebra.Polynomial.Coeff
Polynomial.coeff_C_mul : ∀ {R : Type u} {a : R} {n : ℕ} [inst : Semiring R] (p : Polynomial R), (Polynomial.C a * p).coeff n = a * p.coeff n
-- Mathlib.RingTheory.KrullDimension.Basic
Nontrivial.of_finiteRingKrullDim : ∀ {R : Type u_1} [inst : CommSemiring R] [FiniteRingKrullDim R], Nontrivial R
-- Mathlib.CategoryTheory.Preadditive.Mat
CategoryTheory.Mat_.id_def : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.Preadditive C]
  (M : CategoryTheory.Mat_ C),
  CategoryTheory.CategoryStruct.id M = fun i j => if h : i = j then CategoryTheory.eqToHom ⋯ else 0
-- Lean.Data.Lsp.Capabilities
Lean.Lsp.ClientCapabilities.mk : Option Lean.Lsp.TextDocumentClientCapabilities →
  Option Lean.Lsp.WindowClientCapabilities →
    Option Lean.Lsp.WorkspaceClientCapabilities → Option Lean.Lsp.LeanClientCapabilities → Lean.Lsp.ClientCapabilities
-- Init.Data.OfScientific
/-- Converts a natural number into the closest-possible 32-bit floating-point number, or an infinite
floating-point value if the range of `Float32` is exceeded.
 -/
Nat.toFloat32 : ℕ → Float32
-- Mathlib.Algebra.Lie.Ideal
/-- Regarding an ideal `I` as a subalgebra, the inclusion map into its ambient space is a morphism
of Lie algebras.  -/
LieIdeal.incl : {R : Type u} →
  {L : Type v} →
    [inst : CommRing R] → [inst_1 : LieRing L] → [inst_2 : LieAlgebra R L] → (I : LieIdeal R L) → ↥I →ₗ⁅R⁆ L
-- Mathlib.Geometry.Manifold.LocalSourceTargetProperty
Manifold.IsLocalSourceTargetProperty.mk : ∀ {H : Type u_6} {G : Type u_8} [inst : TopologicalSpace H] [inst_1 : TopologicalSpace G] {M : Type u_10}
  {N : Type u_12} [inst_2 : TopologicalSpace M] [inst_3 : TopologicalSpace N]
  {P : (M → N) → OpenPartialHomeomorph M H → OpenPartialHomeomorph N G → Prop},
  (∀ {f : M → N} {φ : OpenPartialHomeomorph M H} {ψ : OpenPartialHomeomorph N G} {s : Set M},
      IsOpen s → P f φ ψ → P f (φ.restr s) ψ) →
    (∀ {f g : M → N} {φ : OpenPartialHomeomorph M H} {ψ : OpenPartialHomeomorph N G},
        Set.EqOn f g φ.source → P f φ ψ → P g φ ψ) →
      Manifold.IsLocalSourceTargetProperty P
-- Mathlib.Combinatorics.HalesJewett
/-- We require combinatorial subspaces to be nontrivial in the sense that `fun x ↦ l x i` is
`fun x ↦ x e` for at least one coordinate `i`.  -/
Combinatorics.Subspace.proper : ∀ {η : Type u_5} {α : Type u_6} {ι : Type u_7} (self : Combinatorics.Subspace η α ι) (e : η),
  ∃ i, self.idxFun i = Sum.inr e
-- Mathlib.Combinatorics.SimpleGraph.Bipartite
_private.Mathlib.Combinatorics.SimpleGraph.Bipartite.0.SimpleGraph.bipartiteDoubleCover.match_1.eq_2 : ∀ {V : Type u_1} (motive : V ⊕ V → V ⊕ V → Sort u_2) (v' w' : V) (h_1 : (v' w' : V) → motive (Sum.inl v') (Sum.inr w'))
  (h_2 : (v' w' : V) → motive (Sum.inr v') (Sum.inl w')) (h_3 : (x x_1 : V ⊕ V) → motive x x_1),
  (match Sum.inr v', Sum.inl w' with
    | Sum.inl v', Sum.inr w' => h_1 v' w'
    | Sum.inr v', Sum.inl w' => h_2 v' w'
    | x, x_1 => h_3 x x_1) =
    h_2 v' w'
-- Mathlib.Data.Fintype.Defs
Finset.coe_univ : ∀ {α : Type u_1} [inst : Fintype α], ↑Finset.univ = Set.univ
-- Batteries.Control.Lemmas
ReaderT.run_throw : ∀ {ε : Type u_1} {m : Type u_2 → Type u_3} {ρ α : Type u_2} [inst : MonadExceptOf ε m] (e : ε) (ctx : ρ),
  (throw e).run ctx = throw e
-- Mathlib.Analysis.BoxIntegral.Partition.Filter
BoxIntegral.IntegrationParams.MemBaseSet.mono' : ∀ {ι : Type u_1} [inst : Fintype ι] (I : BoxIntegral.Box ι) {c₁ c₂ : NNReal} {l₁ l₂ : BoxIntegral.IntegrationParams}
  {r₁ r₂ : (ι → ℝ) → ↑(Set.Ioi 0)} {π : BoxIntegral.TaggedPrepartition I},
  l₁ ≤ l₂ → c₁ ≤ c₂ → (∀ J ∈ π, r₁ (π.tag J) ≤ r₂ (π.tag J)) → l₁.MemBaseSet I c₁ r₁ π → l₂.MemBaseSet I c₂ r₂ π
-- Mathlib.Algebra.Group.Pointwise.Finset.Scalar
Finset.vadd_finset_empty : ∀ {α : Type u_2} {β : Type u_3} [inst : DecidableEq β] [inst_1 : VAdd α β] (a : α), a +ᵥ ∅ = ∅
-- Lean.Data.Lsp.Extra
Lean.Lsp.instToJsonRpcCallParams : Lean.ToJson Lean.Lsp.RpcCallParams
-- Mathlib.RingTheory.Polynomial.Content
Polynomial.IsPrimitive.primPart_eq : ∀ {R : Type u_1} [inst : CommRing R] [inst_1 : NormalizedGCDMonoid R] {p : Polynomial R}, p.IsPrimitive → p.primPart = p
-- Mathlib.Algebra.Squarefree.Basic
Squarefree.dvd_of_squarefree_of_mul_dvd_mul_right : ∀ {R : Type u_1} [inst : CommMonoidWithZero R] [IsCancelMulZero R] {x y d : R} [DecompositionMonoid R],
  Squarefree x → d * d ∣ x * y → d ∣ y
-- Mathlib.Tactic.CategoryTheory.Coherence.Datatypes
/-- The expression for the identity `𝟙 f`.  -/
Mathlib.Tactic.BicategoryLike.Mor₂.id : Lean.Expr →
  Mathlib.Tactic.BicategoryLike.IsoLift → Mathlib.Tactic.BicategoryLike.Mor₁ → Mathlib.Tactic.BicategoryLike.Mor₂
-- Init.Data.Nat.ToString
Nat.digitChar_eq_zero : ∀ {n : ℕ}, n.digitChar = '0' ↔ n = 0
-- Batteries.Data.AssocList
Batteries.AssocList.mapKey.eq_def : ∀ {α : Type u_1} {δ : Type u_2} {β : Type u_3} (f : α → δ) (x : Batteries.AssocList α β),
  Batteries.AssocList.mapKey f x =
    match x with
    | Batteries.AssocList.nil => Batteries.AssocList.nil
    | Batteries.AssocList.cons k v t => Batteries.AssocList.cons (f k) v (Batteries.AssocList.mapKey f t)
-- Mathlib.MeasureTheory.Group.Action
/-- See also `measure_preimage_smul_of_nullMeasurableSet` and `measure_preimage_smul`.  -/
MeasureTheory.measure_preimage_vadd_le : ∀ {G : Type u} {α : Type w} {m : MeasurableSpace α} [inst : VAdd G α] (μ : MeasureTheory.Measure α)
  [MeasureTheory.VAddInvariantMeasure G α μ] (c : G) (s : Set α), μ ((fun x => c +ᵥ x) ⁻¹' s) ≤ μ s
-- Lean.Parser.Command
Lean.Parser.Command.sectionHeader.formatter : Lean.PrettyPrinter.Formatter
-- Init.Grind.Ordered.Linarith
Lean.Grind.Linarith.Expr.sub.inj : ∀ {a b a_1 b_1 : Lean.Grind.Linarith.Expr}, a.sub b = a_1.sub b_1 → a = a_1 ∧ b = b_1
-- Mathlib.MeasureTheory.Group.FundamentalDomain
MeasureTheory.IsFundamentalDomain.fundamentalInterior : ∀ {G : Type u_1} {α : Type u_3} [Countable G] [inst : Group G] [inst_1 : MulAction G α] [inst_2 : MeasurableSpace α]
  {μ : MeasureTheory.Measure α} {s : Set α},
  MeasureTheory.IsFundamentalDomain G s μ →
    ∀ [MeasurableConstSMul G α] [MeasureTheory.SMulInvariantMeasure G α μ],
      MeasureTheory.IsFundamentalDomain G (MeasureTheory.fundamentalInterior G s) μ
-- Mathlib.Algebra.Group.Shrink
Shrink.instAddGroup.eq_1 : ∀ {α : Type u_2} [inst : Small.{v, u_2} α] [inst_1 : AddGroup α], Shrink.instAddGroup = (equivShrink α).symm.addGroup
-- Mathlib.Algebra.Field.Opposite
AddOpposite.instDivisionRing : {α : Type u_1} → [DivisionRing α] → DivisionRing αᵃᵒᵖ
-- Mathlib.Data.Int.Fib.Lemmas
/-- **Cassini's identity**: `fib (n + 1) * fib (n - 1) - fib n ^ 2 = (-1) ^ |n|`.  -/
Int.fib_succ_mul_fib_pred_sub_fib_sq : ∀ (n : ℤ), Int.fib (n + 1) * Int.fib (n - 1) - Int.fib n ^ 2 = (-1) ^ n.natAbs
-- Init.Data.List.Find
List.findSome?_eq_none_iff : ∀ {α : Type u_1} {α_1 : Type u_2} {p : α → Option α_1} {l : List α}, List.findSome? p l = none ↔ ∀ x ∈ l, p x = none
-- Mathlib.Data.Real.Basic
Real.partialOrder : PartialOrder ℝ
-- Mathlib.Algebra.Homology.Embedding.Extend
HomologicalComplex.extend.X.eq_1 : ∀ {ι : Type u_1} {c : ComplexShape ι} {C : Type u_3} [inst : CategoryTheory.Category.{v_1, u_3} C]
  [inst_1 : CategoryTheory.Limits.HasZeroObject C] [inst_2 : CategoryTheory.Limits.HasZeroMorphisms C]
  (K : HomologicalComplex C c) (x_1 : ι), HomologicalComplex.extend.X K (some x_1) = K.X x_1
-- Mathlib.RingTheory.FormalGroup.Basic
/-- Multiplicative formal group law `𝔾ₘ(X,Y) = X + Y + XY`.  -/
FormalGroup.𝔾ₘ : {R : Type u_1} → [inst : CommRing R] → FormalGroup R
-- Mathlib.RingTheory.Spectrum.Prime.ChevalleyComplexity
ChevalleyThm.MvPolynomialC.numBound.eq_2 : ∀ (k : ℕ) (D : ℕ → ℕ) (n : ℕ),
  ChevalleyThm.MvPolynomialC.numBound k D n.succ =
    ChevalleyThm.MvPolynomialC.numBound k D n * ChevalleyThm.MvPolynomialC.degBound k D n * D n
-- Mathlib.NumberTheory.HeckeRing.Defs
/-- Conjugating the right subgroup of a Hecke triple `(H₁, Δ, H₂)` by an element of `Δ` gives a
subgroup commensurable with the left one.  -/
IsHeckeTriple.commensurable_conjAct_right : ∀ {G : Type u_1} [inst : Group G] {Δ : Submonoid G} {H₁ H₂ : Subgroup G} [IsHeckeTriple Δ H₁ H₂] (g : ↥Δ),
  (ConjAct.toConjAct ↑g • H₂).Commensurable H₁
-- Lean.Compiler.IR.Basic
Lean.IR.IRType.float32 : Lean.IR.IRType
-- Aesop.Forward.State
Aesop.instInhabitedVariableMap : Inhabited Aesop.VariableMap
-- Init.Data.SInt.Lemmas
Int64.toInt16_sub : ∀ (a b : Int64), (a - b).toInt16 = a.toInt16 - b.toInt16
-- Mathlib.CategoryTheory.Adjunction.CompositionIso
CategoryTheory.Adjunction.leftAdjointCompIso_assoc : ∀ {C₀ : Type u_1} {C₁ : Type u_2} {C₂ : Type u_3} {C₃ : Type u_4} [inst : CategoryTheory.Category.{v_1, u_1} C₀]
  [inst_1 : CategoryTheory.Category.{v_2, u_2} C₁] [inst_2 : CategoryTheory.Category.{v_3, u_3} C₂]
  [inst_3 : CategoryTheory.Category.{v_4, u_4} C₃] {F₀₁ : CategoryTheory.Functor C₀ C₁}
  {F₁₂ : CategoryTheory.Functor C₁ C₂} {F₂₃ : CategoryTheory.Functor C₂ C₃} {F₀₂ : CategoryTheory.Functor C₀ C₂}
  {F₁₃ : CategoryTheory.Functor C₁ C₃} {F₀₃ : CategoryTheory.Functor C₀ C₃} {G₁₀ : CategoryTheory.Functor C₁ C₀}
  {G₂₁ : CategoryTheory.Functor C₂ C₁} {G₃₂ : CategoryTheory.Functor C₃ C₂} {G₂₀ : CategoryTheory.Functor C₂ C₀}
  {G₃₁ : CategoryTheory.Functor C₃ C₁} {G₃₀ : CategoryTheory.Functor C₃ C₀} (adj₀₁ : F₀₁ ⊣ G₁₀) (adj₁₂ : F₁₂ ⊣ G₂₁)
  (adj₂₃ : F₂₃ ⊣ G₃₂) (adj₀₂ : F₀₂ ⊣ G₂₀) (adj₁₃ : F₁₃ ⊣ G₃₁) (adj₀₃ : F₀₃ ⊣ G₃₀) (e₀₁₂ : G₂₁.comp G₁₀ ≅ G₂₀)
  (e₁₂₃ : G₃₂.comp G₂₁ ≅ G₃₁) (e₀₁₃ : G₃₁.comp G₁₀ ≅ G₃₀) (e₀₂₃ : G₃₂.comp G₂₀ ≅ G₃₀),
  G₃₂.isoWhiskerLeft e₀₁₂ ≪≫ e₀₂₃ =
      (G₃₂.associator G₂₁ G₁₀).symm ≪≫ CategoryTheory.Functor.isoWhiskerRight e₁₂₃ G₁₀ ≪≫ e₀₁₃ →
    F₀₁.isoWhiskerLeft (adj₁₂.leftAdjointCompIso adj₂₃ adj₁₃ e₁₂₃) ≪≫ adj₀₁.leftAdjointCompIso adj₁₃ adj₀₃ e₀₁₃ =
      (F₀₁.associator F₁₂ F₂₃).symm ≪≫
        CategoryTheory.Functor.isoWhiskerRight (adj₀₁.leftAdjointCompIso adj₁₂ adj₀₂ e₀₁₂) F₂₃ ≪≫
          adj₀₂.leftAdjointCompIso adj₂₃ adj₀₃ e₀₂₃
-- Mathlib.Analysis.Normed.Unbundled.SpectralNorm
/-- For `x : L` with minimal polynomial `f(X) := X^n + a_{n-1}X^{n-1} + ... + a_0` over `K`,
the spectral norm of `x` is equal to `‖a_0‖^(1/(degree(f(X))))`.  -/
spectralNorm.spectralNorm_eq_norm_coeff_zero_rpow : ∀ (K : Type u) [inst : NontriviallyNormedField K] (L : Type v) [inst_1 : Field L] [inst_2 : Algebra K L]
  [Algebra.IsAlgebraic K L] [hu : IsUltrametricDist K] [CompleteSpace K] (x : L),
  spectralNorm K L x = ‖(minpoly K x).coeff 0‖ ^ (1 / ↑(minpoly K x).natDegree)
-- Init.Data.Int.DivMod.Lemmas
Int.natAbs_emod : ∀ (a : ℤ) {b : ℤ},
  b ≠ 0 → (a % b).natAbs = if 0 ≤ a ∨ b ∣ a then a.natAbs % b.natAbs else b.natAbs - a.natAbs % b.natAbs
-- Mathlib.Analysis.SpecialFunctions.Gamma.Deligne
Complex.Gammaℂ_add_one : ∀ {s : ℂ}, s ≠ 0 → (s + 1).Gammaℂ = s.Gammaℂ * s / 2 / ↑Real.pi
-- Mathlib.Order.Hom.BoundedLattice
/-- Copy of a `BoundedLatticeHom` with a new `toFun` equal to the old one. Useful to fix
definitional equalities.  -/
BoundedLatticeHom.copy : {α : Type u_2} →
  {β : Type u_3} →
    [inst : Lattice α] →
      [inst_1 : Lattice β] →
        [inst_2 : BoundedOrder α] →
          [inst_3 : BoundedOrder β] → (f : BoundedLatticeHom α β) → (f' : α → β) → f' = ⇑f → BoundedLatticeHom α β
-- Mathlib.Algebra.Lie.SemiDirect
LieAlgebra.SemiDirectSum.lie_eq_mk : ∀ {R : Type u_1} [inst : CommRing R] {K : Type u_2} [inst_1 : LieRing K] [inst_2 : LieAlgebra R K] {L : Type u_3}
  [inst_3 : LieRing L] [inst_4 : LieAlgebra R L] (ψ : L →ₗ⁅R⁆ LieDerivation R K K) (x y : K ⋊⁅ψ⁆ L),
  ⁅x, y⁆ = { left := ⁅x.left, y.left⁆ + (ψ x.right) y.left - (ψ y.right) x.left, right := ⁅x.right, y.right⁆ }
-- Mathlib.CategoryTheory.Monoidal.Opposite
CategoryTheory.monoidalUnopUnop_μ : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.MonoidalCategory C] (X Y : Cᵒᵖᵒᵖ),
  CategoryTheory.Functor.LaxMonoidal.μ (CategoryTheory.unopUnop C) X Y =
    CategoryTheory.CategoryStruct.id
      (CategoryTheory.MonoidalCategoryStruct.tensorObj ((CategoryTheory.unopUnop C).obj X)
        ((CategoryTheory.unopUnop C).obj Y))
-- Mathlib.CategoryTheory.Comma.StructuredArrow.Basic
/-- The natural equivalence
`CostructuredArrow (S.prod S') (T, T') ≌ CostructuredArrow S T × CostructuredArrow S' T'`.  -/
CategoryTheory.CostructuredArrow.prodEquivalence : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    {D : Type u₂} →
      [inst_1 : CategoryTheory.Category.{v₂, u₂} D] →
        {C' : Type u₃} →
          [inst_2 : CategoryTheory.Category.{v₃, u₃} C'] →
            {D' : Type u₄} →
              [inst_3 : CategoryTheory.Category.{v₄, u₄} D'] →
                (S : CategoryTheory.Functor C D) →
                  (S' : CategoryTheory.Functor C' D') →
                    (T : D) →
                      (T' : D') →
                        CategoryTheory.CostructuredArrow (S.prod S') (T, T') ≌
                          CategoryTheory.CostructuredArrow S T × CategoryTheory.CostructuredArrow S' T'
-- Mathlib.CategoryTheory.Bicategory.Adjunction.Basic
CategoryTheory.Bicategory.Adjunction.mk.sizeOf_spec : ∀ {B : Type u₁} [inst : CategoryTheory.Bicategory B] {a b : B} {f : a ⟶ b} {g : b ⟶ a} [inst_1 : SizeOf B]
  (unit : CategoryTheory.CategoryStruct.id a ⟶ CategoryTheory.CategoryStruct.comp f g)
  (counit : CategoryTheory.CategoryStruct.comp g f ⟶ CategoryTheory.CategoryStruct.id b)
  (left_triangle :
    autoParam
      (CategoryTheory.Bicategory.leftZigzag unit counit =
        CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.leftUnitor f).hom
          (CategoryTheory.Bicategory.rightUnitor f).inv)
      CategoryTheory.Bicategory.Adjunction.left_triangle._autoParam)
  (right_triangle :
    autoParam
      (CategoryTheory.Bicategory.rightZigzag unit counit =
        CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.rightUnitor g).hom
          (CategoryTheory.Bicategory.leftUnitor g).inv)
      CategoryTheory.Bicategory.Adjunction.right_triangle._autoParam),
  sizeOf { unit := unit, counit := counit, left_triangle := left_triangle, right_triangle := right_triangle } =
    1 + sizeOf unit + sizeOf counit + sizeOf left_triangle + sizeOf right_triangle
-- Mathlib.CategoryTheory.Action.Basic
Action.FunctorCategoryEquivalence.functor_obj_map : ∀ {V : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} V] {G : Type u_2} [inst_1 : Monoid G] (M : Action V G)
  {X Y : CategoryTheory.SingleObj G} (g : X ⟶ Y), (Action.FunctorCategoryEquivalence.functor.obj M).map g = M.ρ g
-- Mathlib.Data.List.Cycle
List.next_prev : ∀ {α : Type u_1} [inst : DecidableEq α] (l : List α), l.Nodup → ∀ (x : α) (hx : x ∈ l), l.next (l.prev x hx) ⋯ = x
-- Mathlib.CategoryTheory.Monoidal.Mod
/-- The action map is compatible with addition.  -/
CategoryTheory.AddModObj.add_vadd_assoc : ∀ {C : Type u₁} {inst : CategoryTheory.Category.{v₁, u₁} C} {inst_1 : CategoryTheory.MonoidalCategory C} {D : Type u₂}
  {inst_2 : CategoryTheory.Category.{v₂, u₂} D} {inst_3 : CategoryTheory.MonoidalCategory.MonoidalLeftAction C D}
  {M : C} {inst_4 : CategoryTheory.AddMonObj M} (X : D) [self : CategoryTheory.AddModObj M X] {Z : D} (h : X ⟶ Z),
  CategoryTheory.CategoryStruct.comp
      (CategoryTheory.MonoidalCategory.MonoidalLeftActionStruct.actionHomLeft CategoryTheory.AddMonObj.add X)
      (CategoryTheory.CategoryStruct.comp CategoryTheory.AddModObj.vadd h) =
    CategoryTheory.CategoryStruct.comp
      (CategoryTheory.MonoidalCategory.MonoidalLeftActionStruct.actionAssocIso M M X).hom
      (CategoryTheory.CategoryStruct.comp
        (CategoryTheory.MonoidalCategory.MonoidalLeftActionStruct.actionHomRight M CategoryTheory.AddModObj.vadd)
        (CategoryTheory.CategoryStruct.comp CategoryTheory.AddModObj.vadd h))
-- Mathlib.Probability.Moments.SubGaussian
ProbabilityTheory.Kernel.HasSubgaussianMGF.zero_measure : ∀ {Ω : Type u_1} {Ω' : Type u_2} {mΩ : MeasurableSpace Ω} {mΩ' : MeasurableSpace Ω'} {κ : ProbabilityTheory.Kernel Ω' Ω}
  {X : Ω → ℝ} {c : NNReal}, ProbabilityTheory.Kernel.HasSubgaussianMGF X c κ 0
-- Mathlib.CategoryTheory.Limits.Shapes.SingleObj
CategoryTheory.Limits.SingleObj.Types.sections.equivFixedPoints_apply_coe : ∀ {M : Type v} [inst : Monoid M] (J : CategoryTheory.Functor (CategoryTheory.SingleObj M) (Type u)) (s : ↑J.sections),
  ↑((CategoryTheory.Limits.SingleObj.Types.sections.equivFixedPoints J) s) = ↑s (CategoryTheory.SingleObj.star M)
-- Init.Data.Array.Subarray.Split
/-- Splits a subarray into two parts, the first of which contains the first `i` elements and the second
of which contains the remainder.
 -/
Subarray.split : {α : Type u_1} → (s : Subarray α) → Fin (Std.Slice.size s).succ → Subarray α × Subarray α
-- Mathlib.CategoryTheory.Equivalence
CategoryTheory.Functor.instIsEquivalenceObjWhiskeringLeft : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  {E : Type u₃} [inst_2 : CategoryTheory.Category.{v₃, u₃} E] (F : CategoryTheory.Functor C D) [F.IsEquivalence],
  ((CategoryTheory.Functor.whiskeringLeft C D E).obj F).IsEquivalence
-- Mathlib.Algebra.Group.Equiv.Opposite
AddMonoidHom.mulUnop.eq_1 : ∀ {α : Type u_3} {β : Type u_4} [inst : AddZeroClass α] [inst_1 : AddZeroClass β],
  AddMonoidHom.mulUnop = AddMonoidHom.mulOp.symm
-- Mathlib.Logic.Relation
IsTrans.map : ∀ {α : Type u_1} {β : Type u_2} {r : α → α → Prop} [IsTrans α r] {f : α → β},
  (∀ (x y : α), f x = f y → r x y) → IsTrans β (Relation.Map r f f)
-- Mathlib.Tactic.Module
Mathlib.Tactic.Module.NF.add_eq_eval : ∀ {R : Type u_2} {M : Type u_3} {R₁ : Type u_4} {R₂ : Type u_5} [inst : AddCommMonoid M] [inst_1 : Semiring R]
  [inst_2 : Module R M] [inst_3 : Semiring R₁] [inst_4 : Module R₁ M] [inst_5 : Semiring R₂] [inst_6 : Module R₂ M]
  {l₁ l₂ l : Mathlib.Tactic.Module.NF R M} {l₁' : Mathlib.Tactic.Module.NF R₁ M} {l₂' : Mathlib.Tactic.Module.NF R₂ M}
  {x₁ x₂ : M},
  x₁ = l₁'.eval →
    x₂ = l₂'.eval → l₁.eval = l₁'.eval → l₂.eval = l₂'.eval → l₁.eval + l₂.eval = l.eval → x₁ + x₂ = l.eval
-- Mathlib.Tactic.FunProp.Theorems
Mathlib.Meta.FunProp.LambdaTheoremType.noConfusionType : Sort v✝ → Mathlib.Meta.FunProp.LambdaTheoremType → Mathlib.Meta.FunProp.LambdaTheoremType → Sort v✝
-- Std.Data.DHashMap.Lemmas
Std.DHashMap.get?_inter_of_not_mem_left : ∀ {α : Type u} {β : α → Type v} {x : BEq α} {x_1 : Hashable α} {m₁ m₂ : Std.DHashMap α β} [inst : LawfulBEq α] {k : α},
  k ∉ m₁ → (m₁ ∩ m₂).get? k = none
-- Mathlib.Order.Interval.Finset.Basic
Finset.Ioc_disjoint_Ioc : ∀ {α : Type u_2} {a₁ a₂ b₁ b₂ : α} [inst : LinearOrder α] [inst_1 : LocallyFiniteOrder α],
  Disjoint (Finset.Ioc a₁ a₂) (Finset.Ioc b₁ b₂) ↔ min a₂ b₂ ≤ max a₁ b₁
-- Mathlib.Algebra.Star.SelfAdjoint
/-- All elements are self-adjoint when `star` is trivial.  -/
IsSelfAdjoint.all : ∀ {R : Type u_1} [inst : Star R] [TrivialStar R] (r : R), IsSelfAdjoint r
-- Init.Data.String.Basic
String.endPos_push : ∀ {s : String} {c : Char}, (s.push c).rawEndPos = s.rawEndPos + c
-- Mathlib.Data.Set.Image
Set.rightInverse_rangeSplitting : ∀ {α : Type u_1} {β : Type u_2} {f : α → β},
  Function.Injective f → Function.RightInverse (Set.rangeFactorization f) (Set.rangeSplitting f)
-- Mathlib.Algebra.Group.UniqueProds.Basic
/-- `Unique_Mul` is preserved under multiplicative maps that are injective.

See `UniqueMul.mulHom_map_iff` for a version with swapped bundling.  -/
UniqueMul.mulHom_image_iff : ∀ {G : Type u_1} {H : Type u_2} [inst : Mul G] [inst_1 : Mul H] {A B : Finset G} {a0 b0 : G} [inst_2 : DecidableEq H]
  (f : G →ₙ* H),
  Function.Injective ⇑f → (UniqueMul (Finset.image (⇑f) A) (Finset.image (⇑f) B) (f a0) (f b0) ↔ UniqueMul A B a0 b0)
-- Mathlib.Algebra.Lie.Abelian
LieModule.toLinearMap_maxTrivLinearMapEquivLieModuleHom_symm : ∀ {R : Type u} {L : Type v} {M : Type w} {N : Type w₁} [inst : CommRing R] [inst_1 : LieRing L]
  [inst_2 : LieAlgebra R L] [inst_3 : AddCommGroup M] [inst_4 : Module R M] [inst_5 : LieRingModule L M]
  [inst_6 : LieModule R L M] [inst_7 : AddCommGroup N] [inst_8 : Module R N] [inst_9 : LieRingModule L N]
  [inst_10 : LieModule R L N] (f : M →ₗ⁅R,L⁆ N), ↑(LieModule.maxTrivLinearMapEquivLieModuleHom.symm f) = ↑f
-- Mathlib.Order.Preorder.Chain
IsChain.le_of_not_gt : ∀ {α : Type u_1} {s : Set α} [inst : Preorder α],
  IsChain (fun x1 x2 => x1 ≤ x2) s → ∀ {x y : α}, x ∈ s → y ∈ s → ¬x < y → y ≤ x
-- Init.Control.State
/-- Applies a function to the current state that both computes a new state and a value. The new state
replaces the current state, and the value is returned.

It is equivalent to `do let (a, s) := f (← StateT.get); StateT.set s; pure a`. However, using
`StateT.modifyGet` may lead to better performance because it doesn't add a new reference to the
state value, and additional references can inhibit in-place updates of data.
 -/
StateT.modifyGet : {σ : Type u} → {m : Type u → Type v} → [Monad m] → {α : Type u} → (σ → α × σ) → StateT σ m α
-- Mathlib.GroupTheory.GroupAction.DomAct.Basic
DomMulAct.instInvOfMulOpposite : {M : Type u_1} → [Inv Mᵐᵒᵖ] → Inv Mᵈᵐᵃ
-- Mathlib.Analysis.Convex.BetweenList
AffineEquiv.list_wbtw_map_iff : ∀ {R : Type u_1} {V : Type u_2} {V' : Type u_3} {P : Type u_4} {P' : Type u_5} [inst : Ring R] [inst_1 : PartialOrder R]
  [inst_2 : AddCommGroup V] [inst_3 : Module R V] [inst_4 : AddTorsor V P] [inst_5 : AddCommGroup V']
  [inst_6 : Module R V'] [inst_7 : AddTorsor V' P'] {l : List P} (f : P ≃ᵃ[R] P'),
  List.Wbtw R (List.map (⇑f) l) ↔ List.Wbtw R l