mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.CategoryTheory.Monoidal.Bimod
Bimod.TensorBimod.one_act_left' : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.MonoidalCategory C]
  [inst_2 : CategoryTheory.Limits.HasCoequalizers C] {R S T : CategoryTheory.Mon C} (P : Bimod R S) (Q : Bimod S T)
  [inst_3 :
    ∀ (X : C),
      CategoryTheory.Limits.PreservesColimitsOfSize.{0, 0, v₁, v₁, u₁, u₁}
        (CategoryTheory.MonoidalCategory.tensorLeft X)],
  CategoryTheory.CategoryStruct.comp
      (CategoryTheory.MonoidalCategoryStruct.whiskerRight CategoryTheory.MonObj.one (Bimod.TensorBimod.X P Q))
      (Bimod.TensorBimod.actLeft P Q) =
    (CategoryTheory.MonoidalCategoryStruct.leftUnitor (Bimod.TensorBimod.X P Q)).hom
-- Std.Data.HashMap.RawLemmas
Std.HashMap.Raw.getD_insert : ∀ {α : Type u} {β : Type v} {m : Std.HashMap.Raw α β} [inst : BEq α] [inst_1 : Hashable α] [EquivBEq α]
  [LawfulHashable α],
  m.WF → ∀ {k a : α} {fallback v : β}, (m.insert k v).getD a fallback = if (k == a) = true then v else m.getD a fallback
-- Init.Data.String.TakeDrop
String.Slice.dropRight : String.Slice → ℕ → String.Slice
-- Mathlib.AlgebraicGeometry.ColimitsOver
AlgebraicGeometry.Scheme.Cover.ColimitGluingData.gluedCocone.eq_1 : ∀ {P : CategoryTheory.MorphismProperty AlgebraicGeometry.Scheme} [inst : P.IsStableUnderBaseChange]
  [inst_1 : P.IsMultiplicative] {S : AlgebraicGeometry.Scheme} {J : Type u_1}
  [inst_2 : CategoryTheory.Category.{v_1, u_1} J] {D : CategoryTheory.Functor J (P.Over ⊤ S)} {𝒰 : S.OpenCover}
  [inst_3 : CategoryTheory.Category.{v_2, u_2} 𝒰.I₀] [inst_4 : AlgebraicGeometry.Scheme.Cover.LocallyDirected 𝒰]
  (d : AlgebraicGeometry.Scheme.Cover.ColimitGluingData D 𝒰)
  [inst_5 :
    ∀ {i j : 𝒰.I₀} (hij : i ⟶ j),
      CategoryTheory.Limits.PreservesColimitsOfShape J
        (CategoryTheory.MorphismProperty.Over.pullback P ⊤ (AlgebraicGeometry.Scheme.Cover.trans 𝒰 hij))]
  [inst_6 : Quiver.IsThin 𝒰.I₀] [inst_7 : Small.{u, u_2} 𝒰.I₀] [inst_8 : AlgebraicGeometry.IsZariskiLocalAtTarget P],
  d.gluedCocone =
    { pt := d.glued,
      ι :=
        {
          app := fun a =>
            {
              toCommaMorphism :=
                AlgebraicGeometry.Scheme.OpenCover.glueMorphismsOverOfLocallyDirected
                  ((fun a => CategoryTheory.Precoverage.ZeroHypercover.pullback₁ (D.obj a).hom 𝒰) a)
                  (fun i =>
                    CategoryTheory.CategoryStruct.comp ((d.cocone i).ι.app a).left
                      (CategoryTheory.Limits.colimit.ι d.relativeGluingData.functor i))
                  ⋯ ⋯,
              prop_hom_left := trivial, prop_hom_right := trivial },
          naturality := ⋯ } }
-- Mathlib.Data.Rel
SetRel.preimage_univ_left : ∀ {α : Type u_1} {β : Type u_2} {t : Set β}, t.Nonempty → SetRel.preimage Set.univ t = Set.univ
-- Mathlib.Logic.Equiv.Set
Equiv.ofLeftInverse_eq_ofInjective : ∀ {α : Type u_3} {β : Type u_4} (f : α → β) (f_inv : Nonempty α → β → α)
  (hf : ∀ (h : Nonempty α), Function.LeftInverse (f_inv h) f), Equiv.ofLeftInverse f f_inv hf = Equiv.ofInjective f ⋯
-- Mathlib.LinearAlgebra.AnnihilatingPolynomial
Polynomial.annIdealGenerator.eq_1 : ∀ (𝕜 : Type u_1) {A : Type u_2} [inst : Field 𝕜] [inst_1 : Ring A] [inst_2 : Algebra 𝕜 A] (a : A),
  Polynomial.annIdealGenerator 𝕜 a =
    Submodule.IsPrincipal.generator (Polynomial.annIdeal 𝕜 a) *
      Polynomial.C (Submodule.IsPrincipal.generator (Polynomial.annIdeal 𝕜 a)).leadingCoeff⁻¹
-- Mathlib.Analysis.Asymptotics.Defs
Asymptotics.isBigO_pure : ∀ {α : Type u_1} {E'' : Type u_9} {F'' : Type u_10} [inst : NormedAddCommGroup E''] [inst_1 : NormedAddCommGroup F'']
  {f'' : α → E''} {g'' : α → F''} {x : α}, f'' =O[pure x] g'' ↔ g'' x = 0 → f'' x = 0
-- Std.Data.DHashMap.RawLemmas
Std.DHashMap.Raw.Const.find?_toList_eq_none_iff_not_mem : ∀ {α : Type u} [inst : BEq α] [inst_1 : Hashable α] {β : Type v} {m : Std.DHashMap.Raw α fun x => β} [EquivBEq α]
  [LawfulHashable α], m.WF → ∀ {k : α}, List.find? (fun x => x.1 == k) (Std.DHashMap.Raw.Const.toList m) = none ↔ k ∉ m
-- Mathlib.CategoryTheory.Groupoid.VertexGroup
CategoryTheory.Groupoid.vertexGroupIsomOfMap_symm_apply : ∀ {C : Type u} [inst : CategoryTheory.Groupoid C] {c d : C} (f : c ⟶ d) (δ : d ⟶ d),
  (CategoryTheory.Groupoid.vertexGroupIsomOfMap f).symm δ =
    CategoryTheory.CategoryStruct.comp f (CategoryTheory.CategoryStruct.comp δ (CategoryTheory.Groupoid.inv f))
-- Init.Data.Option.Basic
/-- Equality with `none` is decidable even if the wrapped type does not have decidable equality.
 -/
Option.decidableNoneEq : {α : Type u_1} → (o : Option α) → Decidable (none = o)
-- Init.Data.Iterators.Lemmas.Combinators.Monadic.FilterMap
Std.IterM.toListRev_map_eq_toListRev_filterMapM : ∀ {α β γ : Type w} {m : Type w → Type w'} [inst : Monad m] [inst_1 : MonadAttach m] [LawfulMonad m]
  [WeaklyLawfulMonadAttach m] [inst_4 : Std.Iterator α m β] [Std.Iterators.Finite α m] {f : β → γ} {it : Std.IterM m β},
  (Std.IterM.map f it).toListRev = (Std.IterM.filterMapM (fun b => pure (some (f b))) it).toListRev
-- Mathlib.Control.Monad.Cont
ContT.run_tryCatch : ∀ {r : Type u} {m : Type u → Type v} {α : Type w} {ε : Type u_1} [inst : MonadExceptOf ε m] (act : ContT r m α)
  (h : ε → ContT r m α) (f : α → m r), (tryCatch act h).run f = tryCatch (act.run f) fun e => (h e).run f
-- Mathlib.Algebra.Group.Irreducible.Defs
/-- An irreducible element is not an additive unit.  -/
AddIrreducible.not_isAddUnit : ∀ {M : Type u_1} [inst : AddMonoid M] {p : M}, AddIrreducible p → ¬IsAddUnit p
-- Mathlib.Analysis.Normed.Operator.Bilinear
ContinuousLinearMap.coe_flipₗᵢ' : ∀ {𝕜 : Type u_1} {𝕜₂ : Type u_2} {𝕜₃ : Type u_3} {E : Type u_4} {F : Type u_6} {G : Type u_8}
  [inst : SeminormedAddCommGroup E] [inst_1 : SeminormedAddCommGroup F] [inst_2 : SeminormedAddCommGroup G]
  [inst_3 : NontriviallyNormedField 𝕜] [inst_4 : NontriviallyNormedField 𝕜₂] [inst_5 : NontriviallyNormedField 𝕜₃]
  [inst_6 : NormedSpace 𝕜 E] [inst_7 : NormedSpace 𝕜₂ F] [inst_8 : NormedSpace 𝕜₃ G] {σ₂₃ : 𝕜₂ →+* 𝕜₃} {σ₁₃ : 𝕜 →+* 𝕜₃}
  [inst_9 : RingHomIsometric σ₂₃] [inst_10 : RingHomIsometric σ₁₃],
  ⇑(ContinuousLinearMap.flipₗᵢ' E F G σ₂₃ σ₁₃) = ContinuousLinearMap.flip
-- Mathlib.Geometry.Convex.ConvexSpace.Defs
Convexity.StdSimplex.weights_convexCombPair : ∀ {R : Type u_1} {I : Type u_6} [inst : PartialOrder R] [inst_1 : Semiring R] [inst_2 : IsStrictOrderedRing R]
  (w w' : Convexity.StdSimplex R I) (s t : R) (hs : 0 ≤ s) (ht : 0 ≤ t) (hst : s + t = 1),
  (Convexity.convexCombPair s t hs ht hst w w').weights = s • w.weights + t • w'.weights
-- Mathlib.Algebra.Order.Group.Synonym
Lex.instRightCancelSemigroup.eq_1 : ∀ {α : Type u_1} [inst : RightCancelSemigroup α],
  Lex.instRightCancelSemigroup = { toSemigroup := Lex.instSemigroup, toIsRightCancelMul := ⋯ }
-- Mathlib.CategoryTheory.Monoidal.Cartesian.Grp
CategoryTheory.AddGrp.hom_add : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.CartesianMonoidalCategory C]
  [inst_2 : CategoryTheory.BraidedCategory C] (H : CategoryTheory.AddGrp C)
  [inst_3 : CategoryTheory.IsCommAddMonObj H.X], CategoryTheory.AddMonObj.add.hom.hom = CategoryTheory.AddMonObj.add
-- Mathlib.Order.Interval.Finset.Defs
Finset.Ici_one_eq_univ : ∀ {α : Type u_1} [inst : Preorder α] [inst_1 : LocallyFiniteOrderTop α] [inst_2 : One α] [IsBotOneClass α]
  [inst_4 : Fintype α], Finset.Ici 1 = Finset.univ
-- Mathlib.GroupTheory.Finiteness
/-- An equivalent expression of `Subgroup.FG` in terms of `Set.Finite` instead of `Finset`.  -/
Subgroup.fg_iff : ∀ {G : Type u_3} [inst : Group G] (P : Subgroup G), P.FG ↔ ∃ S, Subgroup.closure S = P ∧ S.Finite
-- Init.Data.Int.DivMod.Lemmas
Int.bmod_eq_emod_of_lt : ∀ {x : ℤ} {m : ℕ}, x % ↑m < (↑m + 1) / 2 → x.bmod m = x % ↑m
-- Mathlib.Topology.Instances.Real.Lemmas
Real.isTopologicalBasis_Ioo_rat : TopologicalSpace.IsTopologicalBasis (⋃ a, ⋃ b, ⋃ (_ : a < b), {Set.Ioo ↑a ↑b})
-- Lean.Parser.Tactic
Lean.Parser.Tactic.matchAlts : Lean.Parser.Parser
-- Lean.PrettyPrinter.Delaborator.Options
Lean.pp.mvars.anonymous : Lean.Option Bool
-- Mathlib.RingTheory.Congruence.Basic
RingCon.le_ringConGen : ∀ {R : Type u_3} [inst : Add R] [inst_1 : Mul R] {r : R → R → Prop}, r ≤ ⇑(ringConGen r)
-- Mathlib.Order.Interval.Set.Fin
Fin.preimage_val_uIcc_val : ∀ {n : ℕ} (i j : Fin n), Fin.val ⁻¹' Set.uIcc ↑i ↑j = Set.uIcc i j
-- Mathlib.Analysis.Convex.Star
StarConvex.sub' : ∀ {𝕜 : Type u_1} {E : Type u_2} [inst : Semiring 𝕜] [inst_1 : PartialOrder 𝕜] [inst_2 : AddCommGroup E]
  [inst_3 : Module 𝕜 E] {x y : E} {s : Set (E × E)},
  StarConvex 𝕜 (x, y) s → StarConvex 𝕜 (x - y) ((fun x => x.1 - x.2) '' s)
-- Mathlib.Topology.Sheaves.SheafCondition.PairwiseIntersections
/-- The sheaf condition in terms of an equalizer diagram is equivalent
to the reformulation in terms of a limit diagram over `U i` and `U i ⊓ U j`.
 -/
TopCat.Presheaf.isSheaf_iff_isSheafPairwiseIntersections : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] {X : TopCat} (F : TopCat.Presheaf C X),
  F.IsSheaf ↔ F.IsSheafPairwiseIntersections
-- Mathlib.Data.Nat.Cast.Defs
/-- The canonical map `ℕ → R` is a homomorphism.  -/
AddMonoidWithOne.natCast_succ : ∀ {R : Type u_2} [self : AddMonoidWithOne R] (n : ℕ), ↑(n + 1) = ↑n + 1
-- Mathlib.CategoryTheory.Limits.Preserves.Opposites
/-- If `F : Cᵒᵖ ⥤ Dᵒᵖ` preserves colimits, then `F.unop : C ⥤ D` preserves limits.  -/
CategoryTheory.Limits.preservesLimits_unop : ∀ {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.Limits.PreservesColimits F],
  CategoryTheory.Limits.PreservesLimits F.unop
-- Mathlib.Algebra.ContinuedFractions.Translations
GenContFract.exists_s_a_of_partNum : ∀ {α : Type u_1} {g : GenContFract α} {n : ℕ} {a : α},
  g.partNums.get? n = some a → ∃ gp, g.s.get? n = some gp ∧ gp.a = a
-- Mathlib.AlgebraicGeometry.Morphisms.QuasiSeparated
AlgebraicGeometry.QuasiSeparated.of_comp : ∀ {X Y Z : AlgebraicGeometry.Scheme} (f : X ⟶ Y) (g : Y ⟶ Z)
  [AlgebraicGeometry.QuasiSeparated (CategoryTheory.CategoryStruct.comp f g)], AlgebraicGeometry.QuasiSeparated f
-- Mathlib.FieldTheory.Minpoly.MinpolyDiv
minpolyDiv_ne_zero : ∀ {R : Type u_2} {S : Type u_1} [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : Algebra R S] {x : S},
  IsIntegral R x → ∀ [Nontrivial S], minpolyDiv R x ≠ 0
-- Mathlib.CategoryTheory.Triangulated.TStructure.Heart
/-- The inclusion functor.  -/
CategoryTheory.Triangulated.TStructure.Heart.ι : {C : Type u} →
  {inst : CategoryTheory.Category.{v, u} C} →
    {inst_1 : CategoryTheory.Preadditive C} →
      {inst_2 : CategoryTheory.Limits.HasZeroObject C} →
        {inst_3 : CategoryTheory.HasShift C ℤ} →
          {inst_4 : ∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive} →
            {inst_5 : CategoryTheory.Pretriangulated C} →
              (t : CategoryTheory.Triangulated.TStructure C) →
                {H : Type u'} →
                  {inst_6 : CategoryTheory.Category.{v', u'} H} →
                    {inst_7 : CategoryTheory.Preadditive H} → [self : t.Heart H] → CategoryTheory.Functor H C
-- Mathlib.Algebra.Polynomial.Basic
Polynomial.toFinsupp_apply : ∀ {R : Type u} [inst : Semiring R] (f : Polynomial R) (i : ℕ), f.toFinsupp.coeff i = f.coeff i
-- Lean.Elab.BuiltinTerm
Lean.Elab.Term.elabHole : Lean.Elab.Term.TermElab
-- Mathlib.RingTheory.Polynomial.Pochhammer
descPochhammer_zero : ∀ (R : Type u) [inst : Ring R], descPochhammer R 0 = 1
-- Mathlib.CategoryTheory.Whiskering
/-- Right-composition gives a functor `(D ⥤ E) ⥤ ((C ⥤ D) ⥤ (C ⥤ E))`.

`(whiskeringRight.obj H).obj F` is `F ⋙ H`, and
`(whiskeringRight.obj H).map α` is `whiskerRight α H`.
 -/
CategoryTheory.Functor.whiskeringRight : (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] →
            CategoryTheory.Functor (CategoryTheory.Functor D E)
              (CategoryTheory.Functor (CategoryTheory.Functor C D) (CategoryTheory.Functor C E))
-- Std.Data.ExtDHashMap.Lemmas
Std.ExtDHashMap.Const.get!_insertMany_list_of_mem : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} {β : Type v} {m : Std.ExtDHashMap α fun x => β} [inst : EquivBEq α]
  [inst_1 : LawfulHashable α] [inst_2 : Inhabited β] {l : List (α × β)} {k k' : α},
  (k == k') = true →
    ∀ {v : β},
      List.Pairwise (fun a b => (a.1 == b.1) = false) l →
        (k, v) ∈ l → Std.ExtDHashMap.Const.get! (Std.ExtDHashMap.Const.insertMany m l) k' = v
-- Mathlib.Analysis.InnerProductSpace.Projection.Basic
LinearIsometry.map_starProjection : ∀ {𝕜 : Type u_1} [inst : RCLike 𝕜] {E : Type u_4} {E' : Type u_5} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedAddCommGroup E'] [inst_3 : InnerProductSpace 𝕜 E] [inst_4 : InnerProductSpace 𝕜 E'] (f : E →ₗᵢ[𝕜] E')
  (p : Submodule 𝕜 E) [inst_5 : p.HasOrthogonalProjection]
  [inst_6 : (Submodule.map f.toLinearMap p).HasOrthogonalProjection] (x : E),
  f (p.starProjection x) = (Submodule.map f.toLinearMap p).starProjection (f x)
-- Init.Data.String.Slice
_private.Init.Data.String.Slice.0.String.Slice.SplitIterator.instIteratorIdSubslice.match_3.eq_3 : ∀ {σ : String.Slice → Type} [inst : (s : String.Slice) → Std.Iterator (σ s) Id (String.Slice.Pattern.SearchStep s)]
  {s : String.Slice} (searcher : Std.Iter (String.Slice.Pattern.SearchStep s)) (motive : searcher.Step → Sort u_1)
  (searcher' : Std.Iter (String.Slice.Pattern.SearchStep s))
  (hps : searcher.IsPlausibleStep (Std.IterStep.skip searcher'))
  (h_1 :
    (searcher'_1 : Std.Iter (String.Slice.Pattern.SearchStep s)) →
      (startPos endPos : s.Pos) →
        (hps_1 :
            searcher.IsPlausibleStep
              (Std.IterStep.yield searcher'_1 (String.Slice.Pattern.SearchStep.matched startPos endPos))) →
          ⟨Std.IterStep.skip searcher', hps⟩ =
              ⟨Std.IterStep.yield searcher'_1 (String.Slice.Pattern.SearchStep.matched startPos endPos), hps_1⟩ →
            motive ⟨Std.IterStep.yield searcher'_1 (String.Slice.Pattern.SearchStep.matched startPos endPos), hps_1⟩)
  (h_2 :
    (searcher'_1 : Std.Iter (String.Slice.Pattern.SearchStep s)) →
      (startPos endPos : s.Pos) →
        (hps_1 :
            searcher.IsPlausibleStep
              (Std.IterStep.yield searcher'_1 (String.Slice.Pattern.SearchStep.rejected startPos endPos))) →
          ⟨Std.IterStep.skip searcher', hps⟩ =
              ⟨Std.IterStep.yield searcher'_1 (String.Slice.Pattern.SearchStep.rejected startPos endPos), hps_1⟩ →
            motive ⟨Std.IterStep.yield searcher'_1 (String.Slice.Pattern.SearchStep.rejected startPos endPos), hps_1⟩)
  (h_3 :
    (searcher'_1 : Std.Iter (String.Slice.Pattern.SearchStep s)) →
      (hps_1 : searcher.IsPlausibleStep (Std.IterStep.skip searcher'_1)) →
        ⟨Std.IterStep.skip searcher', hps⟩ = ⟨Std.IterStep.skip searcher'_1, hps_1⟩ →
          motive ⟨Std.IterStep.skip searcher'_1, hps_1⟩)
  (h_4 :
    (property : searcher.IsPlausibleStep Std.IterStep.done) →
      ⟨Std.IterStep.skip searcher', hps⟩ = ⟨Std.IterStep.done, property⟩ → motive ⟨Std.IterStep.done, property⟩),
  (match h : ⟨Std.IterStep.skip searcher', hps⟩ with
    | ⟨Std.IterStep.yield searcher'_1 (String.Slice.Pattern.SearchStep.matched startPos endPos), hps_1⟩ =>
      h_1 searcher'_1 startPos endPos hps_1 h
    | ⟨Std.IterStep.yield searcher'_1 (String.Slice.Pattern.SearchStep.rejected startPos endPos), hps_1⟩ =>
      h_2 searcher'_1 startPos endPos hps_1 h
    | ⟨Std.IterStep.skip searcher'_1, hps_1⟩ => h_3 searcher'_1 hps_1 h
    | ⟨Std.IterStep.done, property⟩ => h_4 property h) =
    h_3 searcher' hps ⋯
-- Mathlib.Analysis.Normed.Field.Basic
NormedDivisionRing.toMetricSpace : {α : Type u_5} → [self : NormedDivisionRing α] → MetricSpace α
-- Mathlib.RingTheory.Etale.StandardEtale
StandardEtalePair.hasMap_X : ∀ {R : Type u_1} [inst : CommRing R] {P : StandardEtalePair R}, P.HasMap P.X
-- Mathlib.GroupTheory.Perm.Sign
Equiv.Perm.signAux2.congr_simp : ∀ {α : Type u} {inst : DecidableEq α} [inst_1 : DecidableEq α] (a a_1 : List α),
  a = a_1 → ∀ (a_2 a_3 : Equiv.Perm α), a_2 = a_3 → Equiv.Perm.signAux2 a a_2 = Equiv.Perm.signAux2 a_1 a_3
-- Mathlib.Data.Set.Lattice
Set.sdiff_iInter : ∀ {β : Type u_2} {ι : Sort u_5} (s : Set β) (t : ι → Set β), s \ ⋂ i, t i = ⋃ i, s \ t i
-- Mathlib.AlgebraicGeometry.SpreadingOut
AlgebraicGeometry.Scheme.exists_le_and_germ_injective : ∀ (X : AlgebraicGeometry.Scheme) (x : ↥X) [X.IsGermInjectiveAt x] (V : X.Opens),
  x ∈ V →
    ∃ U,
      ∃ (hx : x ∈ U),
        AlgebraicGeometry.IsAffineOpen U ∧
          U ≤ V ∧ Function.Injective ⇑(CategoryTheory.ConcreteCategory.hom (X.presheaf.germ U x hx))
-- Std.Time.Zoned.RecurringRule
/-- Returns the `Day.Offset` (days since epoch) for this `TransitionSpec` in the given year.
 -/
Std.Time.TimeZone.TransitionSpec.toEpochDay : Std.Time.TimeZone.TransitionSpec → Std.Time.Year.Offset → Std.Time.Day.Offset
-- Mathlib.CategoryTheory.Monoidal.Multifunctor
/-- The bottom right map in the associativity hexagon.
 -/
CategoryTheory.Functor.LaxMonoidal.ofBifunctor.secondMap₃ : {C : Type u_1} →
  [inst : CategoryTheory.Category.{v_1, u_1} C] →
    [inst_1 : CategoryTheory.MonoidalCategory C] →
      {D : Type u_2} →
        [inst_2 : CategoryTheory.Category.{v_2, u_2} D] →
          [inst_3 : CategoryTheory.MonoidalCategory D] →
            {F : CategoryTheory.Functor C D} →
              (CategoryTheory.MonoidalCategory.curriedTensorPre F ⟶
                  CategoryTheory.MonoidalCategory.curriedTensorPost F) →
                (CategoryTheory.MonoidalCategory.curriedTensorPrePost F ⟶
                  CategoryTheory.MonoidalCategory.curriedTensorPostPost' F)
-- Mathlib.GroupTheory.GroupExtension.Defs
AddGroupExtension.Section.instFunLike.eq_1 : ∀ {N : Type u_1} {E : Type u_2} {G : Type u_3} [inst : AddGroup N] [inst_1 : AddGroup E] [inst_2 : AddGroup G]
  (S : AddGroupExtension N E G),
  AddGroupExtension.Section.instFunLike S = { coe := AddGroupExtension.Section.toFun, coe_injective := ⋯ }
-- Init.Sym.Lemmas
Lean.Sym.BitVec.le_eq_false : ∀ {n : ℕ} (a b : BitVec n), decide (a ≤ b) = false → (a ≤ b) = False
-- Mathlib.Topology.Separation.Basic
isClosed_inter_singleton : ∀ {X : Type u_1} [inst : TopologicalSpace X] [T1Space X] {A : Set X} {a : X}, IsClosed (A ∩ {a})
-- Mathlib.GroupTheory.GroupAction.Defs
MulAction.orbit_submonoid_subset : ∀ {M : Type u_1} {α : Type u_3} [inst : Monoid M] [inst_1 : MulAction M α] (S : Submonoid M) (a : α),
  MulAction.orbit (↥S) a ⊆ MulAction.orbit M a
-- Mathlib.Algebra.Polynomial.Monic
Polynomial.Monic.mul_natDegree_lt_iff : ∀ {R : Type u} [inst : Semiring R] {p : Polynomial R},
  p.Monic → ∀ {q : Polynomial R}, (p * q).natDegree < p.natDegree ↔ p ≠ 1 ∧ q = 0
-- Mathlib.Topology.Algebra.OpenSubgroup
OpenSubgroup.comap.eq_1 : ∀ {G : Type u_1} [inst : Group G] [inst_1 : TopologicalSpace G] {N : Type u_2} [inst_2 : Group N]
  [inst_3 : TopologicalSpace N] (f : G →* N) (hf : Continuous ⇑f) (H : OpenSubgroup N),
  OpenSubgroup.comap f hf H = { toSubgroup := Subgroup.comap f ↑H, isOpen' := ⋯ }
-- Mathlib.Analysis.Analytic.Constructions
/-- Scalar multiplication of one analytic function by another.  -/
AnalyticOn.smul : ∀ {𝕜 : Type u_2} [inst : NontriviallyNormedField 𝕜] {E : Type u_3} {F : Type u_4} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F] {A : Type u_7}
  [inst_5 : NormedRing A] [inst_6 : NormedAlgebra 𝕜 A] [inst_7 : Module A F] [IsBoundedSMul A F] [IsScalarTower 𝕜 A F]
  {f : E → A} {g : E → F} {s : Set E}, AnalyticOn 𝕜 f s → AnalyticOn 𝕜 g s → AnalyticOn 𝕜 (fun x => f x • g x) s
-- Mathlib.Topology.Algebra.OpenSubgroup
OpenNormalSubgroup.instSetLike.eq_1 : ∀ {G : Type u} [inst : Group G] [inst_1 : TopologicalSpace G],
  OpenNormalSubgroup.instSetLike = { coe := fun U => ↑U.toOpenSubgroup, coe_injective := ⋯ }
-- Mathlib.Combinatorics.Additive.Energy
Finset.mulEnergy_empty_left : ∀ {α : Type u_1} [inst : DecidableEq α] [inst_1 : Mul α] (t : Finset α), ∅.mulEnergy t = 0
-- Mathlib.Data.NNReal.Defs
Real.toNNReal_eq_ofNat : ∀ {r : ℝ} {n : ℕ} [inst : n.AtLeastTwo], r.toNNReal = OfNat.ofNat n ↔ r = OfNat.ofNat n
-- Mathlib.Algebra.Group.Subgroup.Lattice
AddSubgroup.mem_sInf : ∀ {G : Type u_1} [inst : AddGroup G] {S : Set (AddSubgroup G)} {x : G}, x ∈ sInf S ↔ ∀ p ∈ S, x ∈ p
-- Mathlib.Condensed.AB
Condensed.hasExactLimitsOfShape : ∀ (A : Type u_1) (J : Type u_2) [inst : CategoryTheory.Category.{v_1, u_1} A]
  [inst_1 : CategoryTheory.Category.{v_2, u_2} J] [CategoryTheory.Preadditive A]
  [∀ (X : CompHausᵒᵖ),
      CategoryTheory.Limits.HasLimitsOfShape (CategoryTheory.StructuredArrow X Stonean.toCompHaus.op) A]
  [CategoryTheory.HasWeakSheafify (CategoryTheory.coherentTopology CompHaus) A]
  [CategoryTheory.HasWeakSheafify (CategoryTheory.extensiveTopology Stonean) A]
  [inst_6 : CategoryTheory.Limits.HasLimitsOfShape J A] [CategoryTheory.HasExactLimitsOfShape J A]
  [CategoryTheory.Limits.HasFiniteColimits A], CategoryTheory.HasExactLimitsOfShape J (Condensed A)
-- Mathlib.Topology.Algebra.Module.Multilinear.Basic
ContinuousMultilinearMap.coe_coe : ∀ {R : Type u} {ι : Type v} {M₁ : ι → Type w₁} {M₂ : Type w₂} [inst : Semiring R]
  [inst_1 : (i : ι) → AddCommMonoid (M₁ i)] [inst_2 : AddCommMonoid M₂] [inst_3 : (i : ι) → Module R (M₁ i)]
  [inst_4 : Module R M₂] [inst_5 : (i : ι) → TopologicalSpace (M₁ i)] [inst_6 : TopologicalSpace M₂]
  (f : ContinuousMultilinearMap R M₁ M₂), ⇑f.toMultilinearMap = ⇑f
-- Mathlib.Probability.Kernel.Defs
ProbabilityTheory.Kernel.sum_apply : ∀ {α : Type u_1} {β : Type u_2} {ι : Type u_3} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} [inst : Countable ι]
  (κ : ι → ProbabilityTheory.Kernel α β) (a : α),
  (ProbabilityTheory.Kernel.sum κ) a = MeasureTheory.Measure.sum fun n => (κ n) a
-- Mathlib.RingTheory.DedekindDomain.AdicValuation
IsDedekindDomain.HeightOneSpectrum.adicCompletion.instValuedWithZeroMultiplicativeInt : {R : Type u_1} →
  [inst : CommRing R] →
    [inst_1 : IsDedekindDomain R] →
      (K : Type u_2) →
        [inst_2 : Field K] →
          [inst_3 : Algebra R K] →
            [inst_4 : IsFractionRing R K] →
              (v : IsDedekindDomain.HeightOneSpectrum R) →
                Valued (IsDedekindDomain.HeightOneSpectrum.adicCompletion K v) (WithZero (Multiplicative ℤ))
-- Mathlib.CategoryTheory.Monoidal.Cartesian.Mon
/-- `Functor.map` of a fully faithful monoidal functor as a `AddEquiv`.  -/
CategoryTheory.Functor.FullyFaithful.homAddEquiv : {C : Type u_1} →
  {D : Type u_2} →
    [inst : CategoryTheory.Category.{v, u_1} C] →
      [inst_1 : CategoryTheory.CartesianMonoidalCategory C] →
        [inst_2 : CategoryTheory.Category.{w, u_2} D] →
          [inst_3 : CategoryTheory.CartesianMonoidalCategory D] →
            {M X : C} →
              [inst_4 : CategoryTheory.AddMonObj M] →
                (F : CategoryTheory.Functor C D) →
                  [inst_5 : F.Monoidal] → F.FullyFaithful → (X ⟶ M) ≃+ (F.obj X ⟶ F.obj M)
-- Mathlib.Analysis.Calculus.ContDiff.Comp
/-- `x ↦ fderivWithin 𝕜 (f x) t (g x) (k x)` is smooth at a point within a set.  -/
ContDiffWithinAt.fderivWithin_apply : ∀ {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} {G : Type u_4} [inst : NontriviallyNormedField 𝕜]
  [inst_1 : NormedAddCommGroup E] [inst_2 : NormedSpace 𝕜 E] [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F]
  [inst_5 : NormedAddCommGroup G] [inst_6 : NormedSpace 𝕜 G] {s : Set E} {x₀ : E} {m n : WithTop ℕ∞} {f : E → F → G}
  {g k : E → F} {t : Set F},
  ContDiffWithinAt 𝕜 n (Function.uncurry f) (s ×ˢ t) (x₀, g x₀) →
    ContDiffWithinAt 𝕜 m g s x₀ →
      ContDiffWithinAt 𝕜 m k s x₀ →
        UniqueDiffOn 𝕜 t →
          m + 1 ≤ n → x₀ ∈ s → s ⊆ g ⁻¹' t → ContDiffWithinAt 𝕜 m (fun x => (fderivWithin 𝕜 (f x) t (g x)) (k x)) s x₀
-- Mathlib.Algebra.Order.CauSeq.Basic
CauSeq.const_pow : ∀ {α : Type u_1} {β : Type u_2} [inst : Field α] [inst_1 : LinearOrder α] [inst_2 : IsStrictOrderedRing α]
  [inst_3 : Ring β] {abv : β → α} [inst_4 : IsAbsoluteValue abv] (x : β) (n : ℕ),
  CauSeq.const abv (x ^ n) = CauSeq.const abv x ^ n
-- Lean.Elab.Do.Legacy
Lean.Elab.Term.Do.Code.continue.sizeOf_spec : ∀ (ref : Lean.Syntax), sizeOf (Lean.Elab.Term.Do.Code.continue ref) = 1 + sizeOf ref