mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.CategoryTheory.Bicategory.Adjunction.Cat
CategoryTheory.Adjunction.toCat_comp_toCat : ∀ {C D E : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Category.{v, u} D]
  [inst_2 : CategoryTheory.Category.{v, u} E] {F : CategoryTheory.Functor C D} {G : CategoryTheory.Functor D C}
  (adj : F ⊣ G) {F' : CategoryTheory.Functor D E} {G' : CategoryTheory.Functor E D} (adj' : F' ⊣ G'),
  adj.toCat.comp adj'.toCat = (adj.comp adj').toCat
-- Mathlib.CategoryTheory.Distributive.Monoidal
CategoryTheory.IsMonoidalRightDistrib.of_isIso_coprodComparisonTensorRight : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v, u_1} C] [inst_1 : CategoryTheory.MonoidalCategory C]
  [inst_2 : CategoryTheory.Limits.HasBinaryCoproducts C]
  [i :
    ∀ {X Y Z : C},
      CategoryTheory.IsIso
        (CategoryTheory.Limits.coprodComparison (CategoryTheory.MonoidalCategory.tensorRight X) Y Z)],
  CategoryTheory.IsMonoidalRightDistrib C
-- Mathlib.RingTheory.MvPowerSeries.Inverse
MvPowerSeries.coeff_invOfUnit : ∀ {σ : Type u_1} {R : Type u_2} [inst : Ring R] [inst_1 : DecidableEq σ] (n : σ →₀ ℕ) (φ : MvPowerSeries σ R) (u : Rˣ),
  (MvPowerSeries.coeff n) (φ.invOfUnit u) =
    if n = 0 then ↑u⁻¹
    else
      -↑u⁻¹ *
        ∑ x ∈ Finset.HasAntidiagonal.antidiagonal n,
          if x.2 < n then (MvPowerSeries.coeff x.1) φ * (MvPowerSeries.coeff x.2) (φ.invOfUnit u) else 0
-- Mathlib.GroupTheory.Nilpotent
AddSubgroup.mem_upperCentralSeriesStep : ∀ {G : Type u_1} [inst : AddGroup G] (N : AddSubgroup G) [inst_1 : N.Normal] (x : G),
  x ∈ N.upperCentralSeriesStep ↔ ∀ (y : G), ⁅x, y⁆ ∈ N
-- Mathlib.Topology.UniformSpace.UniformConvergenceTopology
/-- The natural bijection between `α → Π i, δ i` and `Π i, α → δ i`, upgraded to a uniform
isomorphism between `α →ᵤ (Π i, δ i)` and `Π i, α →ᵤ δ i`.  -/
UniformFun.uniformEquivPiComm : (α : Type u_1) →
  {ι : Type u_4} →
    (δ : ι → Type u_5) →
      [inst : (i : ι) → UniformSpace (δ i)] → UniformFun α ((i : ι) → δ i) ≃ᵤ ((i : ι) → UniformFun α (δ i))
-- Lean.Meta.Basic
/-- `withMCtx mctx k` replaces the metavariable context and then executes `k`.
The metavariable context is restored after executing `k`.

This method is used to implement the type class resolution procedure.  -/
Lean.Meta.withMCtx : {n : Type → Type u_1} → [MonadControlT Lean.MetaM n] → [Monad n] → {α : Type} → Lean.MetavarContext → n α → n α
-- Mathlib.GroupTheory.GroupAction.Pointwise
AddGroup.preimage_vadd_set : ∀ {G : Type u_1} [inst : AddGroup G] {α : Type u_2} {β : Type u_3} [inst_1 : AddAction G α] [inst_2 : AddAction G β]
  {F : Type u_4} [inst_3 : FunLike F α β] [AddActionHomClass F G α β] (f : F) (c : G) (t : Set β),
  ⇑f ⁻¹' (c +ᵥ t) = c +ᵥ ⇑f ⁻¹' t
-- Lean.Meta.Basic
_private.Lean.Meta.Basic.0.Lean.Meta.withNewFVar : {α : Type} → Lean.Expr → Lean.Expr → (Lean.Expr → Lean.MetaM α) → Lean.MetaM α
-- Mathlib.Algebra.Algebra.NonUnitalSubalgebra
NonUnitalSubalgebra.centralizer_le : ∀ (R : Type u_1) {A : Type u_2} [inst : CommSemiring R] [inst_1 : NonUnitalSemiring A] [inst_2 : Module R A]
  [inst_3 : IsScalarTower R A A] [inst_4 : SMulCommClass R A A] (s t : Set A),
  s ⊆ t → NonUnitalSubalgebra.centralizer R t ≤ NonUnitalSubalgebra.centralizer R s
-- Mathlib.AlgebraicTopology.SimplicialSet.Subcomplex
SSet.Subcomplex.image_le_iff : ∀ {X Y : SSet} (A : X.Subcomplex) (f : X ⟶ Y) (Z : Y.Subcomplex), A.image f ≤ Z ↔ A ≤ Z.preimage f
-- Mathlib.Analysis.Asymptotics.LinearGrowth
LinearGrowth.linearGrowthSup_comp_nonneg : ∀ {u : ℕ → EReal} {v : ℕ → ℕ},
  Monotone u → u ≠ ⊥ → Filter.Tendsto v Filter.atTop Filter.atTop → 0 ≤ LinearGrowth.linearGrowthSup (u ∘ v)
-- Lean.Elab.Tactic.Omega.Frontend
/-- Pending facts which have not been processed yet.  -/
Lean.Elab.Tactic.Omega.MetaProblem.facts : Lean.Elab.Tactic.Omega.MetaProblem → List Lean.Expr
-- Mathlib.CategoryTheory.Limits.Shapes.Opposites.Pullbacks
/-- A pullback cone is a limit cone in `Cᵒᵖ` if and only if the corresponding pushout cocone
in `C` is a colimit cocone.  -/
CategoryTheory.Limits.PullbackCone.isLimitEquivIsColimitUnop : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    {X Y Z : Cᵒᵖ} →
      {f : X ⟶ Z} →
        {g : Y ⟶ Z} →
          (c : CategoryTheory.Limits.PullbackCone f g) →
            CategoryTheory.Limits.IsLimit c ≃ CategoryTheory.Limits.IsColimit c.unop
-- Mathlib.Algebra.Order.ToIntervalMod
toIcoDiv_neg : ∀ {α : Type u_1} [inst : AddCommGroup α] [inst_1 : LinearOrder α] [inst_2 : IsOrderedAddMonoid α] [hα : Archimedean α]
  {p : α} (hp : 0 < p) (a b : α), toIcoDiv hp a (-b) = -(toIocDiv hp (-a) b + 1)
-- Init.Data.BitVec.Lemmas
BitVec.ushiftRight_xor_distrib : ∀ {w : ℕ} (x y : BitVec w) (n : ℕ), (x ^^^ y) >>> n = x >>> n ^^^ y >>> n
-- Mathlib.CategoryTheory.Abelian.Injective.Ext
CategoryTheory.InjectiveResolution.extEquivCohomologyClass_zero : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Abelian C]
  [inst_2 : CategoryTheory.HasExt C] (X : C) {Y : C} (R : CategoryTheory.InjectiveResolution Y) (n : ℕ),
  R.extEquivCohomologyClass 0 = 0
-- Init.System.IOError
IO.Error.interrupted.inj : ∀ {filename : String} {osCode : UInt32} {details filename_1 : String} {osCode_1 : UInt32} {details_1 : String},
  IO.Error.interrupted filename osCode details = IO.Error.interrupted filename_1 osCode_1 details_1 →
    filename = filename_1 ∧ osCode = osCode_1 ∧ details = details_1
-- Mathlib.LinearAlgebra.Matrix.ToLinearEquiv
Matrix.Nondegenerate.smul_iff : ∀ {n : Type u_1} {A : Type u_4} [inst : CommRing A] [IsDomain A] {M : Matrix n n A} [inst_2 : Finite n] {t : A},
  t ≠ 0 → ((t • M).Nondegenerate ↔ M.Nondegenerate)
-- Mathlib.Logic.Encodable.Basic
Encodable.encode_some : ∀ {α : Type u_1} [inst : Encodable α] (a : α), Encodable.encode (some a) = (Encodable.encode a).succ
-- Mathlib.Algebra.Module.Presentation.Free
Module.free_iff_exists_presentation : ∀ (A : Type u) [inst : Ring A] (M : Type v) [inst_1 : AddCommGroup M] [inst_2 : Module A M],
  Module.Free A M ↔ ∃ p, IsEmpty p.R
-- Mathlib.Algebra.Order.WithTop.Untop0
WithTop.untop₀_eq_zero : ∀ {α : Type u_1} [inst : Zero α] {a : WithTop α}, a.untop₀ = 0 ↔ a = 0 ∨ a = ⊤
-- Mathlib.Algebra.Category.Semigrp.Basic
AddMagmaCat.ofHom_comp : ∀ {M N P : Type u} [inst : Add M] [inst_1 : Add N] [inst_2 : Add P] (f : M →ₙ+ N) (g : N →ₙ+ P),
  AddMagmaCat.ofHom (g.comp f) = CategoryTheory.CategoryStruct.comp (AddMagmaCat.ofHom f) (AddMagmaCat.ofHom g)
-- Init.Data.Nat.Basic
Nat.le_pred_of_lt : ∀ {n m : ℕ}, n < m → n ≤ m.pred
-- Std.Data.DHashMap.Lemmas
Std.DHashMap.isEmpty_filter_iff : ∀ {α : Type u} {β : α → Type v} {x : BEq α} {x_1 : Hashable α} {m : Std.DHashMap α β} [inst : LawfulBEq α]
  {f : (a : α) → β a → Bool}, (Std.DHashMap.filter f m).isEmpty = true ↔ ∀ (k : α) (h : k ∈ m), f k (m.get k h) = false
-- Mathlib.Topology.Bornology.BoundedOperation
mul_bounded_of_bounded_of_bounded : ∀ {R : Type u_1} {X : Type u_2} [inst : PseudoMetricSpace R] [inst_1 : Mul R] [BoundedMul R] {f g : X → R},
  (∃ C, ∀ (x y : X), dist (f x) (f y) ≤ C) →
    (∃ C, ∀ (x y : X), dist (g x) (g y) ≤ C) → ∃ C, ∀ (x y : X), dist ((f * g) x) ((f * g) y) ≤ C
-- Mathlib.RingTheory.MvPowerSeries.Basic
MvPolynomial.coe_eq_one_iff : ∀ {σ : Type u_1} {R : Type u_2} [inst : CommSemiring R] {φ : MvPolynomial σ R}, ↑φ = 1 ↔ φ = 1
-- Init.Data.SInt.Lemmas
ISize.toNatClampNeg_ofInt_eq_zero : ∀ {n : ℤ}, -2 ^ 31 ≤ n → n ≤ 0 → (ISize.ofInt n).toNatClampNeg = 0
-- Mathlib.Order.BooleanGenerators
IsCompactlyGenerated.BooleanGenerators.eq_atoms_of_sSup_eq_top : ∀ {α : Type u_1} [inst : CompleteLattice α] {S : Set α} [IsCompactlyGenerated α],
  IsCompactlyGenerated.BooleanGenerators S → sSup S = ⊤ → S = {a | IsAtom a}
-- Mathlib.Combinatorics.Matroid.Sum
Matroid.disjointSum_indep_iff : ∀ {α : Type u_1} {M N : Matroid α} {h : Disjoint M.E N.E} {I : Set α},
  (M.disjointSum N h).Indep I ↔ M.Indep (I ∩ M.E) ∧ N.Indep (I ∩ N.E) ∧ I ⊆ M.E ∪ N.E
-- Mathlib.Order.WithBot
WithBot.le_unbotA_iff : ∀ {α : Type u_1} {a : α} [inst : LE α] {x : WithBot α} [inst_1 : Nonempty α], x ≠ ⊥ → (a ≤ x.unbotA ↔ ↑a ≤ x)
-- Mathlib.CategoryTheory.Products.Basic
CategoryTheory.whiskeringLeftCompEvaluation_hom_app : ∀ {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 : CategoryTheory.Functor A B) (a : A)
  (X : CategoryTheory.Functor B C),
  (CategoryTheory.whiskeringLeftCompEvaluation F a).hom.app X = CategoryTheory.CategoryStruct.id (X.obj (F.obj a))
-- Mathlib.Algebra.Group.Subsemigroup.Defs
Subsemigroup.instBot.eq_1 : ∀ {M : Type u_1} [inst : Mul M], Subsemigroup.instBot = { bot := { carrier := ∅, mul_mem' := ⋯ } }
-- Mathlib.Data.WSeq.Basic
/-- Append two weak sequences. As with `Seq.append`, this may not use
the second sequence if the first one takes forever to compute  -/
Stream'.WSeq.append : {α : Type u} → Stream'.WSeq α → Stream'.WSeq α → Stream'.WSeq α
-- Mathlib.RingTheory.PowerSeries.Basic
PowerSeries.instNontrivialSubalgebra : ∀ {R : Type u_1} [inst : CommSemiring R] [Nontrivial R], Nontrivial (Subalgebra R (PowerSeries R))
-- Mathlib.NumberTheory.FLT.Three
/-- If `p : 𝓞 K` is a prime that divides both `S.a + S.b` and `S.a + η ^ 2 * S.b`, then `p`
is associated with `λ`.  -/
_private.Mathlib.NumberTheory.FLT.Three.0.FermatLastTheoremForThreeGen.Solution.associated_of_dvd_a_add_b_of_dvd_a_add_eta_sq_mul_b : ∀ {K : Type u_1} [inst : Field K] {ζ : K} {hζ : IsPrimitiveRoot ζ 3} (S : FermatLastTheoremForThreeGen.Solution✝ hζ)
  [inst_1 : NumberField K] [IsCyclotomicExtension {3} ℚ K] {p : NumberField.RingOfIntegers K},
  Prime p →
    p ∣
        FermatLastTheoremForThreeGen.Solution'.a✝ (FermatLastTheoremForThreeGen.Solution.toSolution'✝ S) +
          FermatLastTheoremForThreeGen.Solution'.b✝ (FermatLastTheoremForThreeGen.Solution.toSolution'✝ S) →
      p ∣
          FermatLastTheoremForThreeGen.Solution'.a✝ (FermatLastTheoremForThreeGen.Solution.toSolution'✝ S) +
            ↑⋯.unit ^ 2 *
              FermatLastTheoremForThreeGen.Solution'.b✝ (FermatLastTheoremForThreeGen.Solution.toSolution'✝ S) →
        Associated p (hζ.toInteger - 1)
-- Mathlib.FieldTheory.SeparableClosure
IntermediateField.sepDegree_bot : ∀ (F : Type u) (E : Type v) [inst : Field F] [inst_1 : Field E] [inst_2 : Algebra F E], Field.sepDegree F ↥⊥ = 1
-- Lean.Parser.Types
Lean.Parser.instCoeParserContextInputContext : Coe Lean.Parser.ParserContext Lean.Parser.InputContext
-- Mathlib.Algebra.Category.Grp.Basic
CommGrpCat.fullyFaithfulForget₂ToGrp.eq_1 : CommGrpCat.fullyFaithfulForget₂ToGrp =
  { preimage := fun {X Y} f => CommGrpCat.ofHom (GrpCat.Hom.hom f),
    map_preimage := @CommGrpCat.fullyFaithfulForget₂ToGrp._proof_1,
    preimage_map := @CommGrpCat.fullyFaithfulForget₂ToGrp._proof_2 }
-- Init.Data.SInt.Lemmas
ISize.toNatClampNeg_lt_two_pow_numBits : ∀ (x : ISize), x.toNatClampNeg < 2 ^ (System.Platform.numBits - 1)
-- Std.Data.DTreeMap.Internal.Model
Std.DTreeMap.Internal.Impl.getEntryGT?.go.eq_2 : ∀ {α : Type u} {β : α → Type v} [inst : Ord α] (k : α) (best : Option ((a : α) × β a)) (size : ℕ) (k' : α) (v : β k')
  (l r : Std.DTreeMap.Internal.Impl α β),
  Std.DTreeMap.Internal.Impl.getEntryGT?.go k best (Std.DTreeMap.Internal.Impl.inner size k' v l r) =
    match compare k k' with
    | Ordering.lt => Std.DTreeMap.Internal.Impl.getEntryGT?.go k (some ⟨k', v⟩) l
    | x => Std.DTreeMap.Internal.Impl.getEntryGT?.go k best r
-- Mathlib.Algebra.Homology.HomologicalComplex
ChainComplex.mkHom_f_0 : ∀ {V : Type u} [inst : CategoryTheory.Category.{v, u} V] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms V]
  (P Q : ChainComplex V ℕ) (zero : P.X 0 ⟶ Q.X 0) (one : P.X 1 ⟶ Q.X 1)
  (one_zero_comm : CategoryTheory.CategoryStruct.comp one (Q.d 1 0) = CategoryTheory.CategoryStruct.comp (P.d 1 0) zero)
  (succ :
    (n : ℕ) →
      (p :
          (f : P.X n ⟶ Q.X n) ×'
            (f' : P.X (n + 1) ⟶ Q.X (n + 1)) ×'
              CategoryTheory.CategoryStruct.comp f' (Q.d (n + 1) n) =
                CategoryTheory.CategoryStruct.comp (P.d (n + 1) n) f) →
        (f'' : P.X (n + 2) ⟶ Q.X (n + 2)) ×'
          CategoryTheory.CategoryStruct.comp f'' (Q.d (n + 2) (n + 1)) =
            CategoryTheory.CategoryStruct.comp (P.d (n + 2) (n + 1)) p.snd.fst),
  (P.mkHom Q zero one one_zero_comm succ).f 0 = zero
-- Mathlib.MeasureTheory.Measure.Lebesgue.Basic
Real.volume_uIoo : ∀ {a b : ℝ}, MeasureTheory.volume (Set.uIoo a b) = ENNReal.ofReal |b - a|
-- Mathlib.MeasureTheory.Integral.Bochner.Set
/-- **Alias** of `MeasureTheory.setIntegral_eq_of_subset_of_ae_sdiff_eq_zero`.

---

If a function vanishes almost everywhere on `t \ s` with `s ⊆ t`, then its integrals on `s`
and `t` coincide if `t` is null-measurable.  -/
MeasureTheory.setIntegral_eq_of_subset_of_ae_diff_eq_zero : ∀ {X : Type u_1} {E : Type u_3} {mX : MeasurableSpace X} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E]
  {f : X → E} {s t : Set X} {μ : MeasureTheory.Measure X},
  MeasureTheory.NullMeasurableSet t μ →
    s ⊆ t → (∀ᵐ (x : X) ∂μ, x ∈ t \ s → f x = 0) → ∫ (x : X) in t, f x ∂μ = ∫ (x : X) in s, f x ∂μ
-- Mathlib.Analysis.CStarAlgebra.Basic
instNormedSpaceSubtypeMemAddSubgroupSelfAdjointOfTrivialStarOfStarModule : {𝕜 : Type u_1} →
  {E : Type u_2} →
    [inst : SeminormedAddCommGroup E] →
      [inst_1 : StarAddMonoid E] →
        [inst_2 : NormedField 𝕜] →
          [inst_3 : NormedSpace 𝕜 E] →
            [inst_4 : Star 𝕜] → [TrivialStar 𝕜] → [StarModule 𝕜 E] → NormedSpace 𝕜 ↥(selfAdjoint E)
-- Mathlib.Tactic.Ring.Compare
/-- Inductive type carrying the two kinds of errors which can arise in the metaprograms
`Mathlib.Tactic.Ring.evalLE.lean` and `Mathlib.Tactic.Ring.evalLT.lean`.  -/
Mathlib.Tactic.Ring.ExceptType : Type
-- Mathlib.AlgebraicGeometry.Birational.RationalMap
AlgebraicGeometry.Scheme.PartialMap.equiv_of_fromSpecStalkOfMem_eq : ∀ {X Y : AlgebraicGeometry.Scheme} [IrreducibleSpace ↥X] {x : ↥X} [X.IsGermInjectiveAt x] (f g : X.PartialMap Y)
  (hxf : x ∈ f.domain) (hxg : x ∈ g.domain), f.fromSpecStalkOfMem hxf = g.fromSpecStalkOfMem hxg → f.equiv g
-- Mathlib.Algebra.Order.Monoid.Unbundled.Units
/-- **Alias** of the forward direction of `IsUnit.mul_le_mul_left`. -/
IsUnit.le_of_mul_le_mul_left : ∀ {M : Type u_1} [inst : Monoid M] [inst_1 : LE M] [MulLeftMono M] {a b c : M}, IsUnit a → a * b ≤ a * c → b ≤ c
-- Mathlib.Analysis.Calculus.Deriv.Inv
/-- Eta-expanded form of `HasDerivAt.inv` -/
HasDerivAt.fun_inv : ∀ {𝕜 : Type u} [inst : NontriviallyNormedField 𝕜] {x : 𝕜} {𝕜' : Type u_1} [inst_1 : NontriviallyNormedField 𝕜']
  [inst_2 : NormedAlgebra 𝕜 𝕜'] {c : 𝕜 → 𝕜'} {c' : 𝕜'},
  HasDerivAt c c' x → c x ≠ 0 → HasDerivAt (fun i => (c i)⁻¹) (-c' / c x ^ 2) x
-- Mathlib.Algebra.Order.Monoid.Unbundled.Basic
le_mul_of_one_le_of_le : ∀ {α : Type u_1} [inst : MulOneClass α] [inst_1 : Preorder α] [MulRightMono α] {a b c : α}, 1 ≤ a → b ≤ c → b ≤ a * c
-- Mathlib.AlgebraicGeometry.EllipticCurve.Affine.Point
WeierstrassCurve.Affine.CoordinateRing.C_addPolynomial : ∀ {R : Type r} [inst : CommRing R] {W' : WeierstrassCurve.Affine R} (x y ℓ : R),
  (WeierstrassCurve.Affine.CoordinateRing.mk W') (Polynomial.C (W'.addPolynomial x y ℓ)) =
    (WeierstrassCurve.Affine.CoordinateRing.mk W')
      ((Polynomial.X - Polynomial.C (WeierstrassCurve.Affine.linePolynomial x y ℓ)) *
        (W'.negPolynomial - Polynomial.C (WeierstrassCurve.Affine.linePolynomial x y ℓ)))
-- Mathlib.Tactic.Widget.LibraryRewrite
Mathlib.Tactic.LibraryRewrite.RewriteInterface.mk.sizeOf_spec : ∀ (symm : Bool) (tactic : String) (replacement : Lean.Expr) (replacementString : String)
  (extraGoals : Array Lean.Widget.CodeWithInfos) (prettyLemma : Lean.Widget.CodeWithInfos) (lemmaType : Lean.Expr)
  (makesNewMVars : Bool),
  sizeOf
      { symm := symm, tactic := tactic, replacement := replacement, replacementString := replacementString,
        extraGoals := extraGoals, prettyLemma := prettyLemma, lemmaType := lemmaType, makesNewMVars := makesNewMVars } =
    1 + sizeOf symm + sizeOf tactic + sizeOf replacement + sizeOf replacementString + sizeOf extraGoals +
          sizeOf prettyLemma +
        sizeOf lemmaType +
      sizeOf makesNewMVars
-- Mathlib.Algebra.Category.MonCat.Limits
MonCat.HasLimits.limitConeIsLimit.eq_1 : ∀ {J : Type v} [inst : CategoryTheory.Category.{w, v} J] (F : CategoryTheory.Functor J MonCat)
  [inst_1 : Small.{u, max u v} ↑(F.comp (CategoryTheory.forget MonCat)).sections],
  MonCat.HasLimits.limitConeIsLimit F =
    CategoryTheory.Limits.IsLimit.ofFaithful (CategoryTheory.forget MonCat)
      (CategoryTheory.Limits.Types.Small.limitConeIsLimit (F.comp (CategoryTheory.forget MonCat)))
      (fun s =>
        MonCat.ofHom
          {
            toFun := fun v =>
              EquivLike.coe (equivShrink ↑(F.comp (CategoryTheory.forget MonCat)).sections)
                ⟨fun j => (CategoryTheory.ConcreteCategory.hom (((CategoryTheory.forget MonCat).mapCone s).π.app j)) v,
                  ⋯⟩,
            map_one' := ⋯, map_mul' := ⋯ })
      ⋯
-- Mathlib.Topology.Algebra.FilterBasis
GroupFilterBasis.hasBasis : ∀ {G : Type u} [inst : Group G] (B : GroupFilterBasis G) (x : G),
  (B.N x).HasBasis (fun V => V ∈ B) fun V => (fun y => x * y) '' V
-- Mathlib.Analysis.Convex.Between
Sbtw.trans_expand_right : ∀ {R : Type u_1} {V : Type u_2} {P : Type u_4} [inst : Field R] [inst_1 : LinearOrder R] [IsStrictOrderedRing R]
  [inst_3 : AddCommGroup V] [inst_4 : Module R V] [inst_5 : AddTorsor V P] {w x y z : P},
  Sbtw R w x y → Sbtw R x y z → Sbtw R w y z
-- Mathlib.Algebra.Category.Semigrp.Basic
addEquivIsoAddSemigrpIso.eq_1 : ∀ {X Y : Type u} [inst : AddSemigroup X] [inst_1 : AddSemigroup Y],
  addEquivIsoAddSemigrpIso =
    { hom := TypeCat.ofHom fun e => e.toAddSemigrpIso, inv := TypeCat.ofHom fun i => i.addSemigrpIsoToAddEquiv,
      hom_inv_id := ⋯, inv_hom_id := ⋯ }
-- Std.Data.TreeMap.Lemmas
Std.TreeMap.getElem!_eq_default_of_contains_eq_false : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Std.TreeMap α β cmp} [Std.TransCmp cmp] [inst : Inhabited β]
  {a : α}, t.contains a = false → t[a]! = default
-- Init.Data.List.Nat.TakeDrop
List.getElem_zip : ∀ {α : Type u_1} {β : Type u_2} {l : List α} {l' : List β} {i : ℕ} {h : i < (l.zip l').length},
  (l.zip l')[i] = (l[i], l'[i])
-- Mathlib.Analysis.Complex.Basic
Complex.reCLM_apply : ∀ (z : ℂ), Complex.reCLM z = z.re
-- Lean.Data.OpenDecl
Lean.OpenDecl.simple : Lean.Name → List Lean.Name → Lean.OpenDecl
-- Mathlib.Data.Rat.Defs
Rat.neg_def : ∀ (q : ℚ), -q = Rat.divInt (-q.num) ↑q.den
-- Mathlib.Geometry.Manifold.Immersion
Manifold.IsImmersionAtOfComplement.small : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} {E'' : Type u} {F : Type u_5}
  [inst_1 : NormedAddCommGroup E] [inst_2 : NormedSpace 𝕜 E] [inst_3 : NormedAddCommGroup E'']
  [inst_4 : NormedSpace 𝕜 E''] [inst_5 : NormedAddCommGroup F] [inst_6 : NormedSpace 𝕜 F] {H : Type u_7}
  [inst_7 : TopologicalSpace H] {G : Type u_9} [inst_8 : TopologicalSpace G] {I : ModelWithCorners 𝕜 E H}
  {J : ModelWithCorners 𝕜 E'' G} {M : Type u_11} [inst_9 : TopologicalSpace M] [inst_10 : ChartedSpace H M]
  {N : Type u_13} [inst_11 : TopologicalSpace N] [inst_12 : ChartedSpace G N] {n : WithTop ℕ∞} {f : M → N} {x : M},
  Manifold.IsImmersionAtOfComplement F I J n f x → Small.{u, u_5} F
-- Mathlib.Data.Multiset.ZeroCons
Multiset.cons_inj_right : ∀ {α : Type u_1} (a : α) {s t : Multiset α}, a ::ₘ s = a ::ₘ t ↔ s = t
-- Mathlib.CategoryTheory.Monoidal.Category
CategoryTheory.MonoidalCategory.associator_inv_naturality_assoc : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.MonoidalCategory C]
  {X Y Z X' Y' Z' : C} (f : X ⟶ X') (g : Y ⟶ Y') (h : Z ⟶ Z') {Z_1 : C}
  (h_1 :
    CategoryTheory.MonoidalCategoryStruct.tensorObj (CategoryTheory.MonoidalCategoryStruct.tensorObj X' Y') Z' ⟶ Z_1),
  CategoryTheory.CategoryStruct.comp
      (CategoryTheory.MonoidalCategoryStruct.tensorHom f (CategoryTheory.MonoidalCategoryStruct.tensorHom g h))
      (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.associator X' Y' Z').inv h_1) =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.associator X Y Z).inv
      (CategoryTheory.CategoryStruct.comp
        (CategoryTheory.MonoidalCategoryStruct.tensorHom (CategoryTheory.MonoidalCategoryStruct.tensorHom f g) h) h_1)
-- Mathlib.Data.List.Sigma
/-- Finds the first entry with a given key `a` and returns its value (as an `Option` because there
might be no entry with key `a`) alongside with the rest of the entries.  -/
List.kextract : {α : Type u} → {β : α → Type v} → [DecidableEq α] → (a : α) → List (Sigma β) → Option (β a) × List (Sigma β)
-- Mathlib.AlgebraicTopology.SimplicialSet.Basic
/-- Truncated simplicial sets.  -/
SSet.Truncated : ℕ → Type (u + 1)
-- Mathlib.Order.Hom.PowersetCard
Set.powersetCard.orderIsoOfFin_symm_apply_val : ∀ {n : ℕ} {I : Type u_2} [inst : LinearOrder I] (s : ↑(Set.powersetCard I n)) (a : ↥↑s),
  ↑((RelIso.symm (Set.powersetCard.orderIsoOfFin s)) a) =
    List.idxOf (↑((OrderIso.setCongr {x | x ∈ (↑s).sort fun x1 x2 => x1 ≤ x2} ↑s ⋯).symm a))
      ((↑s).sort fun a b => a ≤ b)
-- Mathlib.Tactic.NormNum.Core
Mathlib.Meta.NormNum.NormNumExt.mk.inj : ∀ {pre post : Bool}
  {eval : {u : Lean.Level} → {α : Q(Type u)} → (e : Q(«$α»)) → Lean.MetaM (Mathlib.Meta.NormNum.Result e)}
  {name : autoParam Lean.Name Mathlib.Meta.NormNum.NormNumExt.name._autoParam} {pre_1 post_1 : Bool}
  {eval_1 : {u : Lean.Level} → {α : Q(Type u)} → (e : Q(«$α»)) → Lean.MetaM (Mathlib.Meta.NormNum.Result e)}
  {name_1 : autoParam Lean.Name Mathlib.Meta.NormNum.NormNumExt.name._autoParam},
  { pre := pre, post := post, eval := eval, name := name } =
      { pre := pre_1, post := post_1, eval := eval_1, name := name_1 } →
    pre = pre_1 ∧ post = post_1 ∧ eval = eval_1 ∧ name = name_1
-- Mathlib.Probability.ProbabilityMassFunction.Basic
PMF.toOuterMeasure_apply_eq_zero_iff : ∀ {α : Type u_1} (p : PMF α) (s : Set α), p.toOuterMeasure s = 0 ↔ Disjoint p.support s
-- Mathlib.CategoryTheory.Conj
CategoryTheory.Iso.conj_apply : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {X Y : C} (α : X ≅ Y) (f : CategoryTheory.End X),
  α.conj f = CategoryTheory.CategoryStruct.comp α.inv (CategoryTheory.CategoryStruct.comp f α.hom)
-- Mathlib.Data.Finset.Union
Finset.inter_biUnion : ∀ {α : Type u_1} {β : Type u_2} [inst : DecidableEq β] (t : Finset β) (s : Finset α) (f : α → Finset β),
  t ∩ s.biUnion f = s.biUnion fun x => t ∩ f x
-- Mathlib.MeasureTheory.Measure.WithDensityFinite
MeasureTheory.toFinite_eq_self : ∀ {α : Type u_1} {mα : MeasurableSpace α} {μ : MeasureTheory.Measure α} [inst : MeasureTheory.IsProbabilityMeasure μ],
  μ.toFinite = μ
-- Mathlib.CategoryTheory.Localization.DerivabilityStructure.PointwiseRightDerived
CategoryTheory.LocalizerMorphism.rightDerivedFunctorComparison_fac_app_assoc : ∀ {C₁ : Type u₁} {C₂ : Type u₂} {H : Type u₃} [inst : CategoryTheory.Category.{v₁, u₁} C₁]
  [inst_1 : CategoryTheory.Category.{v₂, u₂} C₂] [inst_2 : CategoryTheory.Category.{v₃, u₃} H] {D₁ : Type u₄}
  {D₂ : Type u₅} [inst_3 : CategoryTheory.Category.{v₄, u₄} D₁] [inst_4 : CategoryTheory.Category.{v₅, u₅} D₂]
  {W₁ : CategoryTheory.MorphismProperty C₁} {W₂ : CategoryTheory.MorphismProperty C₂}
  (Φ : CategoryTheory.LocalizerMorphism W₁ W₂) (L₁ : CategoryTheory.Functor C₁ D₁) (L₂ : CategoryTheory.Functor C₂ D₂)
  [inst_5 : L₁.IsLocalization W₁] [inst_6 : L₂.IsLocalization W₂] (F : CategoryTheory.Functor C₂ H)
  (F₁ : CategoryTheory.Functor D₁ H) (α₁ : Φ.functor.comp F ⟶ L₁.comp F₁) (F₂ : CategoryTheory.Functor D₂ H)
  (α₂ : F ⟶ L₂.comp F₂) [inst_7 : F₁.IsRightDerivedFunctor α₁ W₁] (X : C₁) {Z : H}
  (h : F₂.obj ((Φ.localizedFunctor L₁ L₂).obj (L₁.obj X)) ⟶ Z),
  CategoryTheory.CategoryStruct.comp (α₁.app X)
      (CategoryTheory.CategoryStruct.comp ((Φ.rightDerivedFunctorComparison L₁ L₂ F F₁ α₁ F₂ α₂).app (L₁.obj X)) h) =
    CategoryTheory.CategoryStruct.comp (α₂.app (Φ.functor.obj X))
      (CategoryTheory.CategoryStruct.comp
        (F₂.map ((CategoryTheory.CatCommSq.iso Φ.functor L₁ L₂ (Φ.localizedFunctor L₁ L₂)).hom.app X)) h)
-- Mathlib.RingTheory.PolynomialLaw.Basic
PolynomialLaw.ext_iff : ∀ {R : Type u} {inst : CommSemiring R} {M : Type u_1} {inst_1 : AddCommMonoid M} {inst_2 : Module R M} {N : Type u_2}
  {inst_3 : AddCommMonoid N} {inst_4 : Module R N} {x y : M →ₚₗ[R] N}, x = y ↔ x.toFun' = y.toFun'