mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.CategoryTheory.Adjunction.Mates
CategoryTheory.mateEquiv.eq_1 : ∀ {C : Type u₁} {D : Type u₂} {E : Type u₃} {F : Type u₄} [inst : CategoryTheory.Category.{v₁, u₁} C]
  [inst_1 : CategoryTheory.Category.{v₂, u₂} D] [inst_2 : CategoryTheory.Category.{v₃, u₃} E]
  [inst_3 : CategoryTheory.Category.{v₄, u₄} F] {G : CategoryTheory.Functor C E} {H : CategoryTheory.Functor D F}
  {L₁ : CategoryTheory.Functor C D} {R₁ : CategoryTheory.Functor D C} {L₂ : CategoryTheory.Functor E F}
  {R₂ : CategoryTheory.Functor F E} (adj₁ : L₁ ⊣ R₁) (adj₂ : L₂ ⊣ R₂),
  CategoryTheory.mateEquiv adj₁ adj₂ =
    {
      toFun := fun α =>
        CategoryTheory.TwoSquare.mk R₁ H G R₂
          (CategoryTheory.CategoryStruct.comp (R₁.comp G).rightUnitor.inv
            (CategoryTheory.CategoryStruct.comp ((R₁.comp G).whiskerLeft adj₂.unit)
              (CategoryTheory.CategoryStruct.comp (R₁.associator G (L₂.comp R₂)).hom
                (CategoryTheory.CategoryStruct.comp (R₁.whiskerLeft (G.associator L₂ R₂).inv)
                  (CategoryTheory.CategoryStruct.comp
                    (R₁.whiskerLeft (CategoryTheory.Functor.whiskerRight α.natTrans R₂))
                    (CategoryTheory.CategoryStruct.comp (R₁.whiskerLeft (L₁.associator H R₂).hom)
                      (CategoryTheory.CategoryStruct.comp (R₁.associator L₁ (H.comp R₂)).inv
                        (CategoryTheory.CategoryStruct.comp
                          (CategoryTheory.Functor.whiskerRight adj₁.counit (H.comp R₂))
                          (H.comp R₂).leftUnitor.hom)))))))),
      invFun := fun β =>
        CategoryTheory.TwoSquare.mk G L₁ L₂ H
          (CategoryTheory.CategoryStruct.comp (G.comp L₂).leftUnitor.inv
            (CategoryTheory.CategoryStruct.comp (CategoryTheory.Functor.whiskerRight adj₁.unit (G.comp L₂))
              (CategoryTheory.CategoryStruct.comp ((L₁.comp R₁).associator G L₂).inv
                (CategoryTheory.CategoryStruct.comp (CategoryTheory.Functor.whiskerRight (L₁.associator R₁ G).hom L₂)
                  (CategoryTheory.CategoryStruct.comp
                    (CategoryTheory.Functor.whiskerRight (L₁.whiskerLeft β.natTrans) L₂)
                    (CategoryTheory.CategoryStruct.comp
                      (CategoryTheory.Functor.whiskerRight (L₁.associator H R₂).inv L₂)
                      (CategoryTheory.CategoryStruct.comp ((L₁.comp H).associator R₂ L₂).hom
                        (CategoryTheory.CategoryStruct.comp ((L₁.comp H).whiskerLeft adj₂.counit)
                          (L₁.comp H).rightUnitor.hom)))))))),
      left_inv := ⋯, right_inv := ⋯ }
-- Mathlib.LinearAlgebra.Matrix.Cartan
CartanMatrix.E₈_transpose : CartanMatrix.E₈.transpose = CartanMatrix.E₈
-- Lean.Structure
/-- Gets the name of the auxiliary definition that would have the autoParam definition for a field.
 -/
Lean.mkAutoParamFnOfProjFn : Lean.Name → Lean.Name
-- Lean.Expr
_private.Lean.Expr.0.Lean.Expr.etaExpandedAux : Lean.Expr → ℕ → Option Lean.Expr
-- Lean.Elab.PreDefinition.MkInhabitant
Lean.Elab.mkInhabitantFor : Lean.MessageData → Array Lean.Expr → Lean.Expr → Lean.MetaM Lean.Expr
-- Init.Data.List.MinMaxOn
List.apply_minOn_le_of_mem : ∀ {β : Type u_1} {α : Type u_2} [inst : LE β] [inst_1 : DecidableLE β] [Std.IsLinearPreorder β] {xs : List α}
  {f : α → β} {y : α} (hx : y ∈ xs), f (List.minOn f xs ⋯) ≤ f y
-- Mathlib.RingTheory.Artinian.Module
/-- A temporary field instance on the quotients by maximal ideals.  -/
IsArtinianRing.fieldOfSubtypeIsMaximal : (R : Type u_1) → [inst : CommRing R] → (I : MaximalSpectrum R) → Field (R ⧸ I.asIdeal)
-- Init.Grind.Ring.CommSolver
Lean.Grind.CommRing.Poly.mulMon_nc.go.eq_def : ∀ (k : ℤ) (m : Lean.Grind.CommRing.Mon) (p acc : Lean.Grind.CommRing.Poly),
  Lean.Grind.CommRing.Poly.mulMon_nc.go k m p acc =
    match p with
    | Lean.Grind.CommRing.Poly.num k' => Lean.Grind.CommRing.Poly.insert (k * k') m acc
    | Lean.Grind.CommRing.Poly.add k' m' p =>
      Lean.Grind.CommRing.Poly.mulMon_nc.go k m p (Lean.Grind.CommRing.Poly.insert (k * k') (m.mul_nc m') acc)
-- Mathlib.Algebra.Star.StarAlgHom
NonUnitalStarAlgHom.instMonoidWithZero : {R : Type u_1} →
  {A : Type u_2} →
    [inst : Monoid R] →
      [inst_1 : NonUnitalNonAssocSemiring A] →
        [inst_2 : DistribMulAction R A] → [inst_3 : StarAddMonoid A] → MonoidWithZero (A →⋆ₙₐ[R] A)
-- Init.Data.Dyadic.Basic
Int.trailingZeros_eq_zero_of_mod_eq : ∀ {i : ℤ}, i % 2 = 1 → i.trailingZeros = 0
-- Mathlib.Algebra.Module.Equiv.Basic
AddEquiv.coe_toLinearEquiv_symm : ∀ {R : Type u_1} {M : Type u_5} {M₂ : Type u_7} [inst : Semiring R] [inst_1 : AddCommMonoid M]
  [inst_2 : AddCommMonoid M₂] [inst_3 : Module R M] [inst_4 : Module R M₂] (e : M ≃+ M₂)
  (h : ∀ (c : R) (x : M), e (c • x) = c • e x), ⇑(e.toLinearEquiv h).symm = ⇑e.symm
-- Mathlib.Geometry.Euclidean.Angle.Oriented.RightAngle
/-- An angle in a right-angled triangle expressed using `arcsin`.  -/
EuclideanGeometry.oangle_right_eq_arcsin_of_oangle_eq_pi_div_two : ∀ {V : Type u_1} {P : Type u_2} [inst : NormedAddCommGroup V] [inst_1 : InnerProductSpace ℝ V] [inst_2 : MetricSpace P]
  [inst_3 : NormedAddTorsor V P] [hd2 : Fact (Module.finrank ℝ V = 2)] [inst_4 : Module.Oriented ℝ V (Fin 2)]
  {p₁ p₂ p₃ : P},
  EuclideanGeometry.oangle p₁ p₂ p₃ = ↑(Real.pi / 2) →
    EuclideanGeometry.oangle p₂ p₃ p₁ = ↑(Real.arcsin (dist p₁ p₂ / dist p₁ p₃))
-- Std.Data.DHashMap.Internal.RawLemmas
Std.DHashMap.Internal.Raw₀.Const.equiv_of_forall_get?_eq : ∀ {β : Type v} {α : Type u} [inst : BEq α] [inst_1 : Hashable α] [LawfulBEq α]
  {m₁ m₂ : Std.DHashMap.Internal.Raw₀ α fun x => β},
  (↑m₁).WF →
    (↑m₂).WF →
      (∀ (k : α), Std.DHashMap.Internal.Raw₀.Const.get? m₁ k = Std.DHashMap.Internal.Raw₀.Const.get? m₂ k) →
        (↑m₁).Equiv ↑m₂
-- Mathlib.NumberTheory.Padics.RingHoms
/-- `lift f_compat` is the limit of a sequence `f` of compatible ring homs `R →+* ZMod (p^k)`,
with the equality `lift f_compat r = PadicInt.limNthHom f_compat r`.
 -/
PadicInt.lift : {R : Type u_1} →
  [inst : NonAssocSemiring R] →
    {p : ℕ} →
      {f : (k : ℕ) → R →+* ZMod (p ^ k)} →
        [hp_prime : Fact (Nat.Prime p)] →
          (∀ (k1 k2 : ℕ) (hk : k1 ≤ k2), (ZMod.castHom ⋯ (ZMod (p ^ k1))).comp (f k2) = f k1) → R →+* ℤ_[p]
-- Std.Do.SPred.DerivedLaws
Std.Do.SPred.Tactic.instIsPureAndPureAnd : ∀ {φ ψ : Prop} (σs : List (Type u_1)), Std.Do.SPred.Tactic.IsPure spred(⌜φ⌝ ∧ ⌜ψ⌝) (φ ∧ ψ)
-- Mathlib.MeasureTheory.MeasurableSpace.Embedding
/-- Products of measurable spaces are associative.  -/
MeasurableEquiv.prodAssoc : {α : Type u_1} →
  {β : Type u_2} →
    {γ : Type u_3} →
      [inst : MeasurableSpace α] →
        [inst_1 : MeasurableSpace β] → [inst_2 : MeasurableSpace γ] → (α × β) × γ ≃ᵐ α × β × γ
-- Mathlib.Algebra.Homology.Embedding.ExtendHomology
HomologicalComplex.extend.homologyData'_left_i : ∀ {ι : Type u_1} {ι' : Type u_2} {c : ComplexShape ι} {c' : ComplexShape ι'} {C : Type u_3}
  [inst : CategoryTheory.Category.{v_1, u_3} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  [inst_2 : CategoryTheory.Limits.HasZeroObject C] (K : HomologicalComplex C c) (e : c.Embedding c') {i j k : ι}
  {j' : ι'} (hj' : e.f j = j') (hi : c.prev j = i) (hk : c.next j = k) (h : (K.sc' i j k).HomologyData),
  (HomologicalComplex.extend.homologyData' K e hj' hi hk h).left.i =
    CategoryTheory.CategoryStruct.comp h.left.i (K.extendXIso e hj').inv
-- Mathlib.Algebra.Polynomial.Coeff
Polynomial.mul_X_pow_eq_zero : ∀ {R : Type u} [inst : Semiring R] {p : Polynomial R} {n : ℕ}, p * Polynomial.X ^ n = 0 → p = 0
-- Mathlib.Algebra.Homology.Embedding.ExtendHomology
/-- The kernel fork of `(K.extend e).d j' k'` that is deduced from a kernel
fork of `K.d j k `.  -/
HomologicalComplex.extend.leftHomologyData.kernelFork : {ι : Type u_1} →
  {ι' : Type u_2} →
    {c : ComplexShape ι} →
      {c' : ComplexShape ι'} →
        {C : Type u_3} →
          [inst : CategoryTheory.Category.{v_1, u_3} C] →
            [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C] →
              [inst_2 : CategoryTheory.Limits.HasZeroObject C] →
                (K : HomologicalComplex C c) →
                  (e : c.Embedding c') →
                    {j k : ι} →
                      {j' k' : ι'} →
                        e.f j = j' →
                          c.next j = k →
                            c'.next j' = k' →
                              CategoryTheory.Limits.KernelFork (K.d j k) →
                                CategoryTheory.Limits.KernelFork ((K.extend e).d j' k')
-- Mathlib.Util.AtomM
/-- A simplification to apply to atomic expressions when they are encountered,
before interning them in the atom list.  -/
Mathlib.Tactic.AtomM.Context.evalAtom : Mathlib.Tactic.AtomM.Context → Lean.Expr → Lean.MetaM Lean.Meta.Simp.Result
-- Mathlib.Util.WhatsNew
_private.Mathlib.Util.WhatsNew.0.Mathlib.WhatsNew.printIdCore : Lean.Name → Lean.ConstantInfo → Lean.CoreM Lean.MessageData
-- Mathlib.Condensed.Light.Monoidal
LightCondensed.instMonoidalCategorySheafLightProfiniteCoherentTopologyModuleCat : (R : Type u) →
  [inst : CommRing R] →
    CategoryTheory.MonoidalCategory
      (CategoryTheory.Sheaf (CategoryTheory.coherentTopology LightProfinite) (ModuleCat R))
-- Mathlib.MeasureTheory.VectorMeasure.Variation.Semivariation
MeasureTheory.VectorMeasure.exists_subset_lt_enorm_apply_of_lt_semivariation : ∀ {X : Type u_1} {E : Type u_2} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] {mX : MeasurableSpace X}
  {μ : MeasureTheory.VectorMeasure X E} {s : Set X},
  MeasurableSet s → ∀ {a : ENNReal}, a < μ.semivariation s → ∃ t ⊆ s, MeasurableSet t ∧ a < 2 * ‖μ t‖ₑ
-- Mathlib.Algebra.Group.Submonoid.Saturation
SaturatedAddSubmonoid.mk : {M : Type u_1} →
  [inst : AddZeroClass M] → (toAddSubmonoid : AddSubmonoid M) → toAddSubmonoid.AddSaturated → SaturatedAddSubmonoid M
-- Mathlib.MeasureTheory.Measure.FiniteMeasurePi
MeasureTheory.ProbabilityMeasure.toMeasure_pi : ∀ {ι : Type u_1} {α : ι → Type u_2} [inst : Fintype ι] [inst_1 : (i : ι) → MeasurableSpace (α i)]
  (μ : (i : ι) → MeasureTheory.ProbabilityMeasure (α i)),
  ↑(MeasureTheory.ProbabilityMeasure.pi μ) = MeasureTheory.Measure.pi fun i => ↑(μ i)
-- Mathlib.Algebra.Order.Monoid.Unbundled.Units
/-- **Alias** of the reverse direction of `Units.mul_inv_le_iff`. -/
Units.mul_inv_le_of_le_mul : ∀ {M : Type u_1} [inst : Monoid M] [inst_1 : LE M] [MulRightMono M] {a b : M} (u : Mˣ), a ≤ b * ↑u → a * ↑u⁻¹ ≤ b
-- Mathlib.Algebra.Order.Monoid.LocallyFiniteOrder
Finset.card_Ico_add_right : ∀ {M : Type u_1} [inst : AddCancelCommMonoid M] [inst_1 : LinearOrder M] [IsOrderedAddMonoid M]
  [inst_3 : LocallyFiniteOrder M] [ExistsAddOfLE M] (a b c : M),
  (Finset.Ico (a + c) (b + c)).card = (Finset.Ico a b).card
-- Mathlib.CategoryTheory.Limits.Shapes.Opposites.Pullbacks
CategoryTheory.Limits.pullbackIsoOpPushout_inv_snd_assoc : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {X Y Z : Cᵒᵖ} (f : X ⟶ Z) (g : Y ⟶ Z)
  [inst_1 : CategoryTheory.Limits.HasPullback f g] {Z_1 : Cᵒᵖ} (h : Y ⟶ Z_1),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pullbackIsoOpPushout f g).inv
      (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pullback.snd f g) h) =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pushout.inr f.unop g.unop).op h
-- Mathlib.Algebra.Quaternion
Quaternion.normSq_ratCast : ∀ {R : Type u_1} [inst : Field R] [inst_1 : LinearOrder R] [inst_2 : IsStrictOrderedRing R] (q : ℚ),
  ↑(Quaternion.normSq ↑q) = ↑q ^ 2
-- Mathlib.Algebra.Group.Defs
/-- An additive monoid in which addition is cancellative on both sides.
Main examples are `ℕ` and groups. This is the right typeclass for many sum lemmas, as having a zero
is useful to define the sum over the empty set, so `AddRightCancelMonoid` is not enough.  -/
AddCancelMonoid : Type u → Type u
-- Mathlib.Analysis.InnerProductSpace.Defs
/-- A structure requiring that a scalar product is positive semidefinite and symmetric.  -/
PreInnerProductSpace.Core : (𝕜 : Type u_4) → (F : Type u_5) → [inst : RCLike 𝕜] → [inst_1 : AddCommGroup F] → [Module 𝕜 F] → Type (max u_4 u_5)
-- Mathlib.Computability.PartrecCode
Nat.Partrec.Code.ofNatCode.eq_5 : ∀ (n : ℕ),
  Nat.Partrec.Code.ofNatCode n.succ.succ.succ.succ =
    match n.bodd, n.div2.bodd with
    | false, false =>
      (Nat.Partrec.Code.ofNatCode (Nat.unpair n.div2.div2).1).pair
        (Nat.Partrec.Code.ofNatCode (Nat.unpair n.div2.div2).2)
    | false, true =>
      (Nat.Partrec.Code.ofNatCode (Nat.unpair n.div2.div2).1).comp
        (Nat.Partrec.Code.ofNatCode (Nat.unpair n.div2.div2).2)
    | true, false =>
      (Nat.Partrec.Code.ofNatCode (Nat.unpair n.div2.div2).1).prec
        (Nat.Partrec.Code.ofNatCode (Nat.unpair n.div2.div2).2)
    | true, true => (Nat.Partrec.Code.ofNatCode n.div2.div2).rfind'
-- Std.Http.Data.Response
/-- The set of response headers, providing metadata such as `Content-Type`,
`Content-Length`, and caching directives.
 -/
Std.Http.Response.Head.headers : Std.Http.Response.Head → Std.Http.Headers
-- Init.Data.Nat.Basic
Nat.le_of_lt : ∀ {n m : ℕ}, n < m → n ≤ m
-- Mathlib.Topology.Algebra.InfiniteSum.SummationFilter
SummationFilter.support_map : ∀ {β : Type u_2} {γ : Type u_3} (L : SummationFilter β) [L.NeBot] (f : β ↪ γ), (L.map f).support = ⇑f '' L.support
-- Mathlib.RingTheory.PowerSeries.WeierstrassPreparation
PowerSeries.IsWeierstrassDivisorAt.seq.eq_def : ∀ {A : Type u_1} [inst : CommRing A] {g : PowerSeries A} {I : Ideal A} (H : g.IsWeierstrassDivisorAt I)
  (f : PowerSeries A) (x : ℕ),
  H.seq f x =
    match x with
    | 0 => 0
    | k.succ =>
      H.seq f k +
        (PowerSeries.mk fun i =>
            (PowerSeries.coeff (i + ((PowerSeries.map (Ideal.Quotient.mk I)) g).order.toNat)) (f - g * H.seq f k)) *
          ↑⋯.unit⁻¹
-- Mathlib.Data.Ordmap.Invariants
Ordnode.balanceL.eq_1 : ∀ {α : Type u_1} (l : Ordnode α) (x : α) (r : Ordnode α),
  l.balanceL x r =
    Ordnode.casesOn (id r)
      (Ordnode.casesOn (id l) (Ordnode.singleton x) fun ls ll lx lr =>
        Ordnode.casesOn (id ll)
          (Ordnode.casesOn lr (Ordnode.node 2 l x Ordnode.nil) fun size l lrx r =>
            Ordnode.node 3 (Ordnode.singleton lx) lrx (Ordnode.singleton x))
          fun lls l x_1 r =>
          Ordnode.casesOn (id lr) (Ordnode.node 3 ll lx (Ordnode.singleton x)) fun lrs lrl lrx lrr =>
            if lrs < Ordnode.ratio * lls then Ordnode.node (ls + 1) ll lx (Ordnode.node (lrs + 1) lr x Ordnode.nil)
            else
              Ordnode.node (ls + 1) (Ordnode.node (lls + lrl.size + 1) ll lx lrl) lrx
                (Ordnode.node (lrr.size + 1) lrr x Ordnode.nil))
      fun rs l_1 x_1 r_1 =>
      Ordnode.casesOn (id l) (Ordnode.node (rs + 1) Ordnode.nil x r) fun ls ll lx lr =>
        if ls > Ordnode.delta * rs then
          Ordnode.casesOn (id ll) Ordnode.nil fun lls l x_2 r_2 =>
            Ordnode.casesOn (id lr) Ordnode.nil fun lrs lrl lrx lrr =>
              if lrs < Ordnode.ratio * lls then Ordnode.node (ls + rs + 1) ll lx (Ordnode.node (rs + lrs + 1) lr x r)
              else
                Ordnode.node (ls + rs + 1) (Ordnode.node (lls + lrl.size + 1) ll lx lrl) lrx
                  (Ordnode.node (lrr.size + rs + 1) lrr x r)
        else Ordnode.node (ls + rs + 1) l x r
-- Mathlib.CategoryTheory.Limits.Cones
/-- To give an isomorphism between cocones, it suffices to give an
isomorphism between their vertices which commutes with the cocone maps.  -/
CategoryTheory.Limits.Cocone.ext : {J : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} J] →
    {C : Type u₃} →
      [inst_1 : CategoryTheory.Category.{v₃, u₃} C] →
        {F : CategoryTheory.Functor J C} →
          {c c' : CategoryTheory.Limits.Cocone F} →
            (φ : c.pt ≅ c'.pt) →
              autoParam (∀ (j : J), CategoryTheory.CategoryStruct.comp (c.ι.app j) φ.hom = c'.ι.app j)
                  CategoryTheory.Limits.Cocone.ext._auto_1 →
                (c ≅ c')
-- Lean.DocString.Types
Lean.Doc.Block.brecOn_2.go : {i : Type u} →
  {b : Type v} →
    {motive_1 : Lean.Doc.Block i b → Sort u_1} →
      {motive_2 : Array (Lean.Doc.ListItem (Lean.Doc.Block i b)) → Sort u_1} →
        {motive_3 : Array (Lean.Doc.DescItem (Lean.Doc.Inline i) (Lean.Doc.Block i b)) → Sort u_1} →
          {motive_4 : Array (Lean.Doc.Block i b) → Sort u_1} →
            {motive_5 : List (Lean.Doc.ListItem (Lean.Doc.Block i b)) → Sort u_1} →
              {motive_6 : List (Lean.Doc.DescItem (Lean.Doc.Inline i) (Lean.Doc.Block i b)) → Sort u_1} →
                {motive_7 : List (Lean.Doc.Block i b) → Sort u_1} →
                  {motive_8 : Lean.Doc.ListItem (Lean.Doc.Block i b) → Sort u_1} →
                    {motive_9 : Lean.Doc.DescItem (Lean.Doc.Inline i) (Lean.Doc.Block i b) → Sort u_1} →
                      (t : Array (Lean.Doc.DescItem (Lean.Doc.Inline i) (Lean.Doc.Block i b))) →
                        ((t : Lean.Doc.Block i b) → t.below → motive_1 t) →
                          ((t : Array (Lean.Doc.ListItem (Lean.Doc.Block i b))) →
                              Lean.Doc.Block.below_1 t → motive_2 t) →
                            ((t : Array (Lean.Doc.DescItem (Lean.Doc.Inline i) (Lean.Doc.Block i b))) →
                                Lean.Doc.Block.below_2 t → motive_3 t) →
                              ((t : Array (Lean.Doc.Block i b)) → Lean.Doc.Block.below_3 t → motive_4 t) →
                                ((t : List (Lean.Doc.ListItem (Lean.Doc.Block i b))) →
                                    Lean.Doc.Block.below_4 t → motive_5 t) →
                                  ((t : List (Lean.Doc.DescItem (Lean.Doc.Inline i) (Lean.Doc.Block i b))) →
                                      Lean.Doc.Block.below_5 t → motive_6 t) →
                                    ((t : List (Lean.Doc.Block i b)) → Lean.Doc.Block.below_6 t → motive_7 t) →
                                      ((t : Lean.Doc.ListItem (Lean.Doc.Block i b)) →
                                          Lean.Doc.Block.below_7 t → motive_8 t) →
                                        ((t : Lean.Doc.DescItem (Lean.Doc.Inline i) (Lean.Doc.Block i b)) →
                                            Lean.Doc.Block.below_8 t → motive_9 t) →
                                          motive_3 t ×' Lean.Doc.Block.below_2 t
-- Mathlib.Algebra.Category.ModuleCat.Semi
_private.Mathlib.Algebra.Category.ModuleCat.Semi.0.SemimoduleCat.mk.injEq : ∀ {R : Type u} [inst : Semiring R] (carrier : Type v) [isAddCommMonoid : AddCommMonoid carrier]
  [isModule : Module R carrier] (carrier_1 : Type v) (isAddCommMonoid_1 : AddCommMonoid carrier_1)
  (isModule_1 : Module R carrier_1),
  ({ carrier := carrier, isAddCommMonoid := isAddCommMonoid, isModule := isModule } =
      { carrier := carrier_1, isAddCommMonoid := isAddCommMonoid_1, isModule := isModule_1 }) =
    (carrier = carrier_1 ∧ isAddCommMonoid ≍ isAddCommMonoid_1 ∧ isModule ≍ isModule_1)
-- Mathlib.CategoryTheory.Galois.Basic
/-- The cardinality of the fiber of a not-initial object is non-zero.  -/
CategoryTheory.PreGaloisCategory.non_zero_card_fiber_of_not_initial : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{u₂, u₁} C] (F : CategoryTheory.Functor C FintypeCat)
  [inst_1 : CategoryTheory.PreGaloisCategory C] [CategoryTheory.PreGaloisCategory.FiberFunctor F] (X : C),
  (∀ (a : CategoryTheory.Limits.IsInitial X), False) → Nat.card (F.obj X).obj ≠ 0
-- Mathlib.RingTheory.SimpleModule.Isotypic
Submodule.map_le_isotypicComponent : ∀ {R : Type u_2} {M : Type u} {N : Type u_3} [inst : Ring R] [inst_1 : AddCommGroup M] [inst_2 : AddCommGroup N]
  [inst_3 : Module R M] [inst_4 : Module R N] (S : Submodule R M) [IsSimpleModule R ↥S] (f : M →ₗ[R] N),
  Submodule.map f S ≤ isotypicComponent R N ↥S
-- Mathlib.Topology.List
List.continuous_insertIdx : ∀ {α : Type u_1} [inst : TopologicalSpace α] {n : ℕ}, Continuous fun p => p.2.insertIdx n p.1
-- Mathlib.Algebra.Category.ModuleCat.Basic
ModuleCat.ofHom_add : ∀ {R : Type u} [inst : Ring R] {M N : Type v} [inst_1 : AddCommGroup M] [inst_2 : Module R M] [inst_3 : AddCommGroup N]
  [inst_4 : Module R N] (f g : M →ₗ[R] N), ModuleCat.ofHom (f + g) = ModuleCat.ofHom f + ModuleCat.ofHom g
-- Init.Data.Iterators.Lemmas.Consumers.Loop
Std.Iter.length_toListRev_eq_count : ∀ {α β : Type u_1} [inst : Std.Iterator α Id β] [Std.Iterators.Finite α Id] [inst_2 : Std.IteratorLoop α Id Id]
  [Std.LawfulIteratorLoop α Id Id] {it : Std.Iter β}, it.toListRev.length = it.length
-- Lean.Data.NameTrie
Lean.NamePart.num : ℕ → Lean.NamePart
-- Mathlib.Algebra.Order.Group.Unbundled.Abs
le_abs_self : ∀ {α : Type u_1} [inst : Lattice α] [inst_1 : AddGroup α] (a : α), a ≤ |a|
-- Lean.Data.Options
Lean.instMonadOptionsOfMonadLift : {m n : Type → Type} → [MonadLift m n] → [Lean.MonadOptions m] → Lean.MonadOptions n
-- Mathlib.AlgebraicGeometry.Restrict
AlgebraicGeometry.Scheme.Hom.map_resLE : ∀ {X Y : AlgebraicGeometry.Scheme} (f : X ⟶ Y) {U : Y.Opens} {V V' : X.Opens}
  (e : V ≤ (TopologicalSpace.Opens.map f.base).obj U) (i : V' ≤ V),
  CategoryTheory.CategoryStruct.comp (X.homOfLE i) (AlgebraicGeometry.Scheme.Hom.resLE f U V e) =
    AlgebraicGeometry.Scheme.Hom.resLE f U V' ⋯
-- Mathlib.RingTheory.MvPowerSeries.Equiv
MvPowerSeries.toAdicCompletionAlgEquiv_apply : ∀ {σ : Type u_1} {R : Type u_2} [inst : CommRing R] [inst_1 : Finite σ] (p : MvPowerSeries σ R),
  (MvPowerSeries.toAdicCompletionAlgEquiv σ R) p = (MvPowerSeries.toAdicCompletion σ R) p
-- Mathlib.Analysis.Convex.Intrinsic
intrinsicInterior_prod_eq : ∀ {𝕜 : Type u_1} {V : Type u_2} {W : Type u_3} {Q : Type u_4} {P : Type u_5} [inst : Ring 𝕜] [inst_1 : AddCommGroup V]
  [inst_2 : Module 𝕜 V] [inst_3 : TopologicalSpace P] [inst_4 : AddTorsor V P] [inst_5 : AddCommGroup W]
  [inst_6 : Module 𝕜 W] [inst_7 : TopologicalSpace Q] [inst_8 : AddTorsor W Q] (s : Set P) (t : Set Q),
  intrinsicInterior 𝕜 (s ×ˢ t) = intrinsicInterior 𝕜 s ×ˢ intrinsicInterior 𝕜 t
-- Mathlib.GroupTheory.Index
Subgroup.relIndex.eq_1 : ∀ {G : Type u_1} [inst : Group G] (H K : Subgroup G), H.relIndex K = (H.subgroupOf K).index
-- Mathlib.CategoryTheory.Monoidal.Braided.Basic
CategoryTheory.braiding_inv_tensorUnit_left_assoc : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.MonoidalCategory C]
  [inst_2 : CategoryTheory.BraidedCategory C] (X : C) {Z : C}
  (h : CategoryTheory.MonoidalCategoryStruct.tensorObj (CategoryTheory.MonoidalCategoryStruct.tensorUnit C) X ⟶ Z),
  CategoryTheory.CategoryStruct.comp (β_ (CategoryTheory.MonoidalCategoryStruct.tensorUnit C) X).inv h =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.rightUnitor X).hom
      (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.leftUnitor X).inv h)
-- Mathlib.RingTheory.Valuation.Basic
AddValuation.instFunLike : {R : Type u_3} →
  {Γ₀ : Type u_4} → [inst : Ring R] → [inst_1 : LinearOrderedAddCommMonoidWithTop Γ₀] → FunLike (AddValuation R Γ₀) R Γ₀
-- Init.Data.Vector.Lemmas
Vector.getElem?_eq_none : ∀ {α : Type u_1} {n i : ℕ} {xs : Vector α n}, n ≤ i → xs[i]? = none
-- Mathlib.Lean.Meta.RefinedDiscrTree.Lookup
Lean.Meta.RefinedDiscrTree.instInhabitedPartialMatch.default : Lean.Meta.RefinedDiscrTree.PartialMatch✝
-- Aesop.EMap
Aesop.EMap.find? : {α : Type} → Lean.Expr → Aesop.EMap α → Lean.MetaM (Option α)
-- Mathlib.NumberTheory.ModularForms.Basic
/-- **Alias** of `smul_apply`. -/
ModularForm.IsGLPos.smul_apply : ∀ {M : Type u_1} {F : Type u_2} {α : outParam (Type u_3)} {β : outParam (Type u_4)} {inst : FunLike F α β}
  {inst_1 : SMul M β} {inst_2 : SMul M F} [self : IsSMulApply M F α β] (f : F) (r : M) (x : α), (r • f) x = r • f x
-- Mathlib.Combinatorics.SimpleGraph.Connectivity.Connected
SimpleGraph.Connected.nonempty : ∀ {V : Type u} {G : SimpleGraph V}, G.Connected → Nonempty V
-- Mathlib.SetTheory.Cardinal.Basic
Cardinal.mk_iUnion_le_sum_mk : ∀ {α ι : Type u} {f : ι → Set α}, Cardinal.mk ↑(⋃ i, f i) ≤ Cardinal.sum fun i => Cardinal.mk ↑(f i)
-- Mathlib.CategoryTheory.Products.Basic
/-- The Cartesian product of two natural transformations where both functors have the
same source.  -/
CategoryTheory.NatTrans.prod' : {A : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} A] →
    {B : Type u₂} →
      [inst_1 : CategoryTheory.Category.{v₂, u₂} B] →
        {C : Type u₃} →
          [inst_2 : CategoryTheory.Category.{v₃, u₃} C] →
            {F G : CategoryTheory.Functor A B} →
              {H K : CategoryTheory.Functor A C} → (F ⟶ G) → (H ⟶ K) → (F.prod' H ⟶ G.prod' K)