mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.CategoryTheory.FintypeCat
FintypeCat.comp_hom : ∀ {X Y Z : FintypeCat} (f : X ⟶ Y) (g : Y ⟶ Z),
  CategoryTheory.CategoryStruct.comp f.hom g.hom =
    TypeCat.ofHom (⇑(CategoryTheory.ConcreteCategory.hom g.hom) ∘ ⇑(CategoryTheory.ConcreteCategory.hom f.hom))
-- Mathlib.Topology.FiberBundle.Basic
FiberPrebundle.mem_base_pretrivializationAt : ∀ {B : Type u_2} {F : Type u_3} {E : B → Type u_5} [inst : TopologicalSpace B] [inst_1 : TopologicalSpace F]
  [inst_2 : (x : B) → TopologicalSpace (E x)] (self : FiberPrebundle F E) (x : B),
  x ∈ (self.pretrivializationAt x).baseSet
-- Init.Data.Iterators.Lemmas.Combinators.Monadic.FlatMap
Std.IterM.flatMap.eq_1 : ∀ {α β α₂ γ : Type w} {m : Type w → Type w'} [inst : Monad m] [inst_1 : Std.Iterator α m β]
  [inst_2 : Std.Iterator α₂ m γ] (f : β → Std.IterM m γ) (it : Std.IterM m β),
  Std.IterM.flatMap f it = Std.IterM.flatMapAfter f it none
-- Lean.Meta.Tactic.Simp.Types
Lean.Meta.Simp.instInhabitedDiagnostics.default : Lean.Meta.Simp.Diagnostics
-- Mathlib.Data.Sym.Basic
Sym.instZeroSym : {α : Type u_1} → Zero (Sym α 0)
-- Aesop.Stats.Basic
Aesop.RuleStats.mk : Aesop.DisplayRuleName → Aesop.Nanos → Bool → Aesop.RuleStats
-- Mathlib.CategoryTheory.Category.Cat
/-- The 2-iso in Cat corresponding to a natural isomorphism.  -/
CategoryTheory.Cat.Hom.isoMk : {C D : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    [inst_1 : CategoryTheory.Category.{v, u} D] →
      {F G : CategoryTheory.Functor C D} → (F ≅ G) → (F.toCatHom ≅ G.toCatHom)
-- Mathlib.CategoryTheory.Sites.Precoverage.Subsheaf
_private.Mathlib.CategoryTheory.Sites.Precoverage.Subsheaf.0.CategoryTheory.Precoverage.SmallConstruction.Witness.base.inj : ∀ {C : Type u} {inst : CategoryTheory.Category.{v, u} C} {K : CategoryTheory.Precoverage C} {ι : C → Type w} {X : C}
  {a a_1 : ι X},
  CategoryTheory.Precoverage.SmallConstruction.Witness.base✝ X a =
      CategoryTheory.Precoverage.SmallConstruction.Witness.base✝ X a_1 →
    a = a_1
-- Mathlib.GroupTheory.Index
AddSubgroup.relIndex_inf_le : ∀ {G : Type u_1} [inst : AddGroup G] {H K L : AddSubgroup G}, (H ⊓ K).relIndex L ≤ H.relIndex L * K.relIndex L
-- Mathlib.Algebra.Group.Action.Faithful
/-- `Add.toVAddAddOpposite` is faithful when addition is left cancellative  -/
instFaithfulVAddAddOppositeOfIsLeftCancelAdd : ∀ (R : Type u_4) [inst : Add R] [IsLeftCancelAdd R], FaithfulVAdd Rᵃᵒᵖ R
-- Mathlib.Data.Sum.Order
Sum.Lex.toLexRelIsoLE_coe : ∀ {α : Type u_1} {β : Type u_2} [inst : LE α] [inst_1 : LE β], ⇑Sum.Lex.toLexRelIsoLE = ⇑toLex
-- Mathlib.Geometry.Euclidean.Angle.Oriented.Rotation
/-- The angle between two vectors is `θ` if and only if they are nonzero and the second vector
is the first rotated by `θ` and scaled by a positive real, or `θ` and at least one of the
vectors are zero.  -/
Orientation.oangle_eq_iff_eq_pos_smul_rotation_or_eq_zero : ∀ {V : Type u_1} [inst : NormedAddCommGroup V] [inst_1 : InnerProductSpace ℝ V] [inst_2 : Fact (Module.finrank ℝ V = 2)]
  (o : Orientation ℝ V (Fin 2)) {x y : V} (θ : Real.Angle),
  o.oangle x y = θ ↔ (x ≠ 0 ∧ y ≠ 0 ∧ ∃ r, 0 < r ∧ y = r • (o.rotation θ) x) ∨ θ = 0 ∧ (x = 0 ∨ y = 0)
-- Lean.Meta.Tactic.Grind.Arith.CommRing.Types
Lean.Meta.Grind.Arith.CommRing.EqCnstrProof.mul.inj : ∀ {k : ℤ} {e : Lean.Meta.Grind.Arith.CommRing.EqCnstr} {k_1 : ℤ} {e_1 : Lean.Meta.Grind.Arith.CommRing.EqCnstr},
  Lean.Meta.Grind.Arith.CommRing.EqCnstrProof.mul k e = Lean.Meta.Grind.Arith.CommRing.EqCnstrProof.mul k_1 e_1 →
    k = k_1 ∧ e = e_1
-- Mathlib.Control.Monad.Cont
OptionT.callCC : {m : Type u → Type v} →
  [Monad m] → [MonadCont m] → {α β : Type u} → (MonadCont.Label α (OptionT m) β → OptionT m α) → OptionT m α
-- Mathlib.MeasureTheory.VectorMeasure.Basic
/-- The negative of a vector measure is a vector measure.  -/
MeasureTheory.VectorMeasure.neg : {α : Type u_1} →
  {m : MeasurableSpace α} →
    {M : Type u_3} →
      [inst : AddCommGroup M] →
        [inst_1 : TopologicalSpace M] →
          [IsTopologicalAddGroup M] → MeasureTheory.VectorMeasure α M → MeasureTheory.VectorMeasure α M
-- Mathlib.LinearAlgebra.Matrix.Stochastic
/-- Every entry of a column stochastic matrix is nonnegative.  -/
Matrix.nonneg_of_mem_colStochastic : ∀ {R : Type u_1} {n : Type u_2} [inst : Fintype n] [inst_1 : DecidableEq n] [inst_2 : Semiring R]
  [inst_3 : PartialOrder R] [inst_4 : IsOrderedRing R] {M : Matrix n n R},
  M ∈ Matrix.colStochastic R n → ∀ {i j : n}, 0 ≤ M i j
-- Mathlib.SetTheory.Ordinal.Enum
/-- A characterization of `enumOrd`: it is the unique strict monotonic function with range `s`.  -/
Ordinal.eq_enumOrd : ∀ {s : Set Ordinal.{u}} (f : Ordinal.{u} → Ordinal.{u}),
  ¬BddAbove s → (Ordinal.enumOrd s = f ↔ StrictMono f ∧ Set.range f = s)
-- Mathlib.CategoryTheory.Filtered.Basic
/-- The triangles consisting of a morphism in `H` and the maps from `inf O H` commute.
 -/
CategoryTheory.IsCofiltered.infTo_commutes : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.IsCofiltered C] (O : Finset C)
  (H : Finset ((X : C) ×' (Y : C) ×' (_ : X ∈ O) ×' (_ : Y ∈ O) ×' (X ⟶ Y))) {X Y : C} (mX : X ∈ O) (mY : Y ∈ O)
  {f : X ⟶ Y},
  ⟨X, ⟨Y, ⟨mX, ⟨mY, f⟩⟩⟩⟩ ∈ H →
    CategoryTheory.CategoryStruct.comp (CategoryTheory.IsCofiltered.infTo O H mX) f =
      CategoryTheory.IsCofiltered.infTo O H mY
-- Std.Data.DTreeMap.Internal.Lemmas
Std.DTreeMap.Internal.Impl.Const.isEmpty_filter_eq_false_iff : ∀ {α : Type u} {instOrd : Ord α} {β : Type v} {t : Std.DTreeMap.Internal.Impl α fun x => β} [Std.TransOrd α]
  {f : α → β → Bool} (h : t.WF),
  (Std.DTreeMap.Internal.Impl.filter f t ⋯).impl.isEmpty = false ↔
    ∃ k,
      ∃ (h : Std.DTreeMap.Internal.Impl.contains k t = true),
        f (t.getKey k h) (Std.DTreeMap.Internal.Impl.Const.get t k h) = true
-- Mathlib.Computability.TuringMachine.ToPartrec
_private.Mathlib.Computability.TuringMachine.ToPartrec.0.Turing.PartrecToTM2.Λ'.Supports.match_1.splitter : (motive : Turing.PartrecToTM2.Λ' → Sort u_1) →
  (x : Turing.PartrecToTM2.Λ') →
    ((p : Turing.PartrecToTM2.Γ' → Bool) →
        (k₁ k₂ : Turing.PartrecToTM2.K') →
          (q : Turing.PartrecToTM2.Λ') → motive (Turing.PartrecToTM2.Λ'.move p k₁ k₂ q)) →
      ((k : Turing.PartrecToTM2.K') →
          (s : Option Turing.PartrecToTM2.Γ' → Option Turing.PartrecToTM2.Γ') →
            (q : Turing.PartrecToTM2.Λ') → motive (Turing.PartrecToTM2.Λ'.push k s q)) →
        ((q : Option Turing.PartrecToTM2.Γ' → Turing.PartrecToTM2.Λ') → motive (Turing.PartrecToTM2.Λ'.read q)) →
          ((p : Turing.PartrecToTM2.Γ' → Bool) →
              (k : Turing.PartrecToTM2.K') →
                (q : Turing.PartrecToTM2.Λ') → motive (Turing.PartrecToTM2.Λ'.clear p k q)) →
            ((q : Turing.PartrecToTM2.Λ') → motive q.copy) →
              ((q : Turing.PartrecToTM2.Λ') → motive q.succ) →
                ((q₁ q₂ : Turing.PartrecToTM2.Λ') → motive (q₁.pred q₂)) →
                  ((k : Turing.PartrecToTM2.Cont') → motive (Turing.PartrecToTM2.Λ'.ret k)) → motive x
-- Mathlib.CategoryTheory.Sites.Sieves
/-- An auxiliary definition in order to fix the choice of the preimages between various definitions.
 -/
CategoryTheory.Presieve.FunctorPushforwardStructure : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    {D : Type u₂} →
      [inst_1 : CategoryTheory.Category.{v₂, u₂} D] →
        (F : CategoryTheory.Functor C D) →
          {X : C} → CategoryTheory.Presieve X → {Y : D} → (Y ⟶ F.obj X) → Type (max (max u₁ v₁) v₂)
-- Mathlib.CategoryTheory.Subobject.Classifier.Defs
/-- `h.iso m` is the isomorphism between `m` and the pullback of `Ω₀`
along the characteristic map of `m`.  -/
CategoryTheory.SubobjectRepresentableBy.iso : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    [inst_1 : CategoryTheory.Limits.HasPullbacks C] →
      {Ω : C} →
        (h : CategoryTheory.SubobjectRepresentableBy Ω) →
          {U X : C} →
            (m : U ⟶ X) →
              [inst_2 : CategoryTheory.Mono m] →
                CategoryTheory.MonoOver.mk m ≅
                  CategoryTheory.Subobject.representative.obj ((CategoryTheory.Subobject.pullback (h.χ m)).obj h.Ω₀)
-- Mathlib.Data.Part
Part.bind_assoc : ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_4} (f : Part α) (g : α → Part β) (k : β → Part γ),
  (f.bind g).bind k = f.bind fun x => (g x).bind k
-- Init.Omega.Constraint
_private.Init.Omega.Constraint.0.Option.merge.match_1.eq_3 : ∀ {α : Type u_1} (motive : Option α → Option α → Sort u_2) (y : α) (h_1 : Unit → motive none none)
  (h_2 : (x : α) → motive (some x) none) (h_3 : (y : α) → motive none (some y))
  (h_4 : (x y : α) → motive (some x) (some y)),
  (match none, some y with
    | none, none => h_1 ()
    | some x, none => h_2 x
    | none, some y => h_3 y
    | some x, some y => h_4 x y) =
    h_3 y
-- Mathlib.Analysis.CStarAlgebra.Matrix
Matrix.l2_opNNNorm_mul : ∀ {𝕜 : Type u_1} {m : Type u_2} {n : Type u_3} {l : Type u_4} [inst : RCLike 𝕜] [inst_1 : Fintype m]
  [inst_2 : Fintype n] [inst_3 : DecidableEq n] [inst_4 : Fintype l] [inst_5 : DecidableEq l] (A : Matrix m n 𝕜)
  (B : Matrix n l 𝕜), ‖A * B‖₊ ≤ ‖A‖₊ * ‖B‖₊
-- Mathlib.NumberTheory.LSeries.HurwitzZetaEven
/-- Formula for `hurwitzZetaEven` as a Dirichlet series in the convergence range, with sum over `ℕ`
(version with absolute values)  -/
HurwitzZeta.hasSum_nat_hurwitzZetaEven : ∀ (a : ℝ) {s : ℂ},
  1 < s.re → HasSum (fun n => (1 / ↑|↑n + a| ^ s + 1 / ↑|↑n + 1 - a| ^ s) / 2) (HurwitzZeta.hurwitzZetaEven (↑a) s)
-- Mathlib.CategoryTheory.Sites.EffectiveEpimorphic
CategoryTheory.Sieve.EffectiveEpimorphic.iff_forall_isSheafFor_yoneda : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {X : C} (S : CategoryTheory.Sieve X),
  S.EffectiveEpimorphic ↔ ∀ (Y : C), CategoryTheory.Presieve.IsSheafFor (CategoryTheory.yoneda.obj Y) S.arrows
-- Mathlib.Data.NNRat.Defs
/-- Define a (dependent) function or prove `∀ r : ℚ, p r` by dealing with nonnegative rational
numbers of the form `n / d` with `d ≠ 0` and `n`, `d` coprime.  -/
NNRat.numDenCasesOn : {C : ℚ≥0 → Sort u} → (q : ℚ≥0) → ((n d : ℕ) → d ≠ 0 → n.Coprime d → C (NNRat.divNat n d)) → C q
-- Mathlib.Analysis.Complex.UpperHalfPlane.Basic
UpperHalfPlane.canLift : CanLift ℂ UpperHalfPlane UpperHalfPlane.coe fun z => 0 < z.im
-- Mathlib.Algebra.Lie.Sl2
IsSl2Triple.lie_lie_smul_f : ∀ (R : Type u_1) {L : Type u_2} [inst : CommRing R] [inst_1 : LieRing L] [inst_2 : LieAlgebra R L] {h e f : L},
  IsSl2Triple h e f → ⁅h, f⁆ = -(2 • f)
-- Mathlib.Lean.Thunk
/-- The Cartesian product of two thunks.  -/
Thunk.prod : {α : Type u} → {β : Type v} → Thunk α → Thunk β → Thunk (α × β)
-- Mathlib.MeasureTheory.Function.LpSpace.Basic
MeasureTheory.Lp.coe_mk : ∀ {α : Type u_1} {E : Type u_4} {m : MeasurableSpace α} {p : ENNReal} {μ : MeasureTheory.Measure α}
  [inst : NormedAddCommGroup E] {f : α →ₘ[μ] E} (hf : MeasureTheory.eLpNorm (↑f) p μ < ⊤), ↑⟨f, hf⟩ = f
-- Mathlib.CategoryTheory.Sites.SheafHom
CategoryTheory.presheafHom_obj : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {A : Type u'} [inst_1 : CategoryTheory.Category.{v', u'} A]
  (F G : CategoryTheory.Functor Cᵒᵖ A) (X : Cᵒᵖ),
  (CategoryTheory.presheafHom F G).obj X =
    ((CategoryTheory.Over.forget (Opposite.unop X)).op.comp F ⟶
      (CategoryTheory.Over.forget (Opposite.unop X)).op.comp G)
-- Mathlib.Algebra.Order.Floor.Semiring
Nat.add_one_le_ceil_iff : ∀ {R : Type u_1} [inst : Semiring R] [inst_1 : LinearOrder R] [inst_2 : FloorSemiring R] {a : R} {n : ℕ},
  n + 1 ≤ ⌈a⌉₊ ↔ ↑n < a
-- Mathlib.Data.Stream.Init
Stream'.all_def : ∀ {α : Type u} (p : α → Prop) (s : Stream' α), Stream'.All p s = ∀ (n : ℕ), p (s.get n)
-- Init.Data.List.Monadic
List.zipWithM.loop.eq_1 : ∀ {m : Type u → Type v} [inst : Monad m] {α : Type w} {β : Type x} {γ : Type u} (f : α → β → m γ) (x : Array γ) (a : α)
  (as : List α) (b : β) (bs : List β),
  List.zipWithM.loop f (a :: as) (b :: bs) x = do
    let __do_lift ← f a b
    List.zipWithM.loop f as bs (x.push __do_lift)
-- Mathlib.Algebra.Group.Pointwise.Finset.Basic
/-- The finset `0 : Finset α` is defined as `{0}` in scope `Pointwise`.  -/
Finset.zero : {α : Type u_2} → [Zero α] → Zero (Finset α)
-- Lean.Data.Lsp.LanguageFeatures
Lean.Lsp.SemanticTokenType.property : Lean.Lsp.SemanticTokenType
-- Mathlib.Order.Hom.BoundedLattice
InfTopHom.coe_top : ∀ {α : Type u_2} {β : Type u_3} [inst : Min α] [inst_1 : Top α] [inst_2 : SemilatticeInf β] [inst_3 : OrderTop β],
  ⇑⊤ = ⊤
-- Mathlib.Algebra.Homology.HomotopyCategory.ShiftSequence
CochainComplex.shiftShortComplexFunctorIso_hom_app_τ₁ : ∀ (C : Type u_1) [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Preadditive C] (n i i' : ℤ)
  (hi : n + i = i') (X : CochainComplex C ℤ),
  ((CochainComplex.shiftShortComplexFunctorIso C n i i' hi).hom.app X).τ₁ =
    (n.negOnePow •
        (CochainComplex.shiftEval C n ((ComplexShape.up ℤ).prev i) ((ComplexShape.up ℤ).prev i') ⋯).app X).hom
-- Mathlib.CategoryTheory.Limits.Shapes.Opposites.Products
CategoryTheory.Limits.opProdIsoCoprod_hom_snd : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {A B : C}
  [inst_1 : CategoryTheory.Limits.HasBinaryProduct A B],
  CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.opProdIsoCoprod A B).hom.unop
      CategoryTheory.Limits.prod.snd =
    CategoryTheory.Limits.coprod.inr.unop
-- Mathlib.MeasureTheory.Covering.VitaliFamily
VitaliFamily.FineSubfamilyOn.covering_disjoint_subtype : ∀ {X : Type u_1} [inst : PseudoMetricSpace X] {m0 : MeasurableSpace X} {μ : MeasureTheory.Measure X}
  {v : VitaliFamily μ} {f : X → Set (Set X)} {s : Set X} (h : v.FineSubfamilyOn f s),
  Pairwise (Function.onFun Disjoint fun x => h.covering ↑x)
-- Mathlib.CategoryTheory.IsConnected
/-- Implementation detail of `isoConstant`.  -/
_private.Mathlib.CategoryTheory.IsConnected.0.CategoryTheory.IsPreconnected.IsoConstantAux.liftToDiscrete : {J : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} J] →
    {α : Type u₂} →
      CategoryTheory.Functor J (CategoryTheory.Discrete α) → CategoryTheory.Functor J (CategoryTheory.Discrete J)
-- Std.Data.DTreeMap.Raw.Lemmas
Std.DTreeMap.Raw.toList_filter : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t : Std.DTreeMap.Raw α β cmp} {f : (a : α) → β a → Bool},
  t.WF → (Std.DTreeMap.Raw.filter f t).toList = List.filter (fun p => f p.fst p.snd) t.toList
-- Mathlib.Algebra.Order.Interval.Basic
/-- Extension for the `positivity` tactic: The length of an interval is always nonnegative.  -/
Mathlib.Meta.Positivity.evalNonemptyIntervalLength : Mathlib.Meta.Positivity.PositivityExt
-- Mathlib.Tactic.ClickSuggestions.FindPremises
/-- Compute the discrimination trees for import theorems.  -/
Mathlib.Tactic.ClickSuggestions.computeImportDiscrTrees : Mathlib.Tactic.ClickSuggestions.Choice → Lean.CoreM Unit
-- Mathlib.Topology.Algebra.Valued.LocallyCompact
NormedField.v_eq_valuation : ∀ {K : Type u_1} [inst : NontriviallyNormedField K] [inst_1 : IsUltrametricDist K] (x : K),
  Valued.v x = NormedField.valuation x
-- Mathlib.RingTheory.Ideal.Operations
Ideal.radical_le_radical_iff : ∀ {R : Type u} [inst : CommSemiring R] {I J : Ideal R}, I.radical ≤ J.radical ↔ I ≤ J.radical
-- Std.Data.ExtDTreeMap.Lemmas
Std.ExtDTreeMap.getKey_maxKey!_eq_maxKey : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t : Std.ExtDTreeMap α β cmp} [inst : Std.TransCmp cmp]
  [inst_1 : Inhabited α] {hc : t.maxKey! ∈ t}, t.getKey t.maxKey! hc = t.maxKey ⋯
-- Mathlib.ModelTheory.Types
/-- **Alias** of `FirstOrder.Language.Theory.CompleteType.compl_setOfPred_mem`. -/
FirstOrder.Language.Theory.CompleteType.compl_setOf_mem : ∀ {L : FirstOrder.Language} {T : L.Theory} {α : Type w} {φ : (L.withConstants α).Sentence},
  {p | φ ∈ p}ᶜ = {p | FirstOrder.Language.Formula.not φ ∈ p}
-- Init.Data.SInt.Lemmas
Int64.mul_comm : ∀ (a b : Int64), a * b = b * a
-- Mathlib.Algebra.GradedMonoid
SetLike.coe_list_dProd : ∀ {ι : Type u_1} {R : Type u_2} {α : Type u_3} {S : Type u_4} [inst : SetLike S R] [inst_1 : Monoid R]
  [inst_2 : AddMonoid ι] (A : ι → S) [inst_3 : SetLike.GradedMonoid A] (fι : α → ι) (fA : (a : α) → ↥(A (fι a)))
  (l : List α), ↑(l.dProd fι fA) = (List.map (fun a => ↑(fA a)) l).prod
-- Mathlib.CategoryTheory.Dialectica.Monoidal
CategoryTheory.Dial.braiding_hom_F : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Limits.HasFiniteProducts C]
  [inst_2 : CategoryTheory.Limits.HasPullbacks C] (X Y : CategoryTheory.Dial C),
  (X.braiding Y).hom.F =
    CategoryTheory.Limits.prod.lift
      (CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.prod.snd CategoryTheory.Limits.prod.snd)
      (CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.prod.snd CategoryTheory.Limits.prod.fst)
-- Mathlib.AlgebraicTopology.SimplicialSet.AnodyneExtensions.RelativeCellComplex
SSet.Subcomplex.Pairing.RankFunction.mapN_type₁ : ∀ {X : SSet} {A : X.Subcomplex} {P : A.Pairing} {ι : Type v} [inst : LinearOrder ι] (f : P.RankFunction ι)
  [inst_1 : P.IsProper] [inst_2 : SuccOrder ι] [inst_3 : NoMaxOrder ι] {j : ι} (c : f.Cell j),
  f.mapN (SSet.Subcomplex.Pairing.RankFunction.Cell.type₁ f c) =
    { dim := (↑(P.p c.s)).dim, simplex := (↑(P.p c.s)).simplex }
-- Mathlib.NumberTheory.Padics.Hensel
_private.Mathlib.NumberTheory.Padics.Hensel.0.a_soln_is_unique : ∀ {p : ℕ} [inst : Fact (Nat.Prime p)] {R : Type u_1} [inst_1 : CommSemiring R] [inst_2 : Algebra R ℤ_[p]]
  {F : Polynomial R} {a : ℤ_[p]},
  (Polynomial.aeval a) F = 0 →
    ∀ (z' : ℤ_[p]), (Polynomial.aeval z') F = 0 → ‖z' - a‖ < ‖(Polynomial.aeval a) (Polynomial.derivative F)‖ → z' = a
-- Std.Data.Internal.List.Associative
Std.Internal.List.getValue?_append_of_containsKey_eq_false : ∀ {α : Type u} {β : Type v} [inst : BEq α] {l l' : List ((_ : α) × β)} {a : α},
  Std.Internal.List.containsKey a l' = false → Std.Internal.List.getValue? a (l ++ l') = Std.Internal.List.getValue? a l
-- Mathlib.Data.PFunctor.Multivariate.M
MvPFunctor.M.dest'.eq_1 : ∀ {n : ℕ} (P : MvPFunctor.{u} (n + 1)) {α : TypeVec.{u} n} {x : P.last.M} {a : P.A} {f : P.last.B a → P.last.M}
  (h : x.dest = ⟨a, f⟩) (f' : TypeVec.Arrow (MvPFunctor.M.Path P x) α),
  MvPFunctor.M.dest' P h f' =
    ⟨a, TypeVec.splitFun (MvPFunctor.M.pathDestLeft P h f') fun x_1 => ⟨f x_1, MvPFunctor.M.pathDestRight P h f' x_1⟩⟩
-- Mathlib.LinearAlgebra.FiniteDimensional.Basic
finiteDimensional_finsupp : ∀ {K : Type u} {V : Type v} [inst : DivisionRing K] [inst_1 : AddCommGroup V] [inst_2 : Module K V] {ι : Type u_1}
  [Finite ι] [FiniteDimensional K V], FiniteDimensional K (ι →₀ V)
-- Mathlib.CategoryTheory.Monoidal.Linear
CategoryTheory.tensoringRight_linear : ∀ (R : Type u_1) [inst : Semiring R] {C : Type u_2} [inst_1 : CategoryTheory.Category.{v_1, u_2} C]
  [inst_2 : CategoryTheory.Preadditive C] [inst_3 : CategoryTheory.Linear R C]
  [inst_4 : CategoryTheory.MonoidalCategory C] [inst_5 : CategoryTheory.MonoidalPreadditive C]
  [CategoryTheory.MonoidalLinear R C] (X : C),
  CategoryTheory.Functor.Linear R ((CategoryTheory.MonoidalCategory.tensoringRight C).obj X)
-- Std.Http.Protocol.H1.Message
/-- Gets the version of a `Message`.
 -/
Std.Http.Protocol.H1.Message.Head.version : {dir : Std.Http.Protocol.H1.Direction} → Std.Http.Protocol.H1.Message.Head dir → Std.Http.Version
-- Mathlib.CategoryTheory.Bicategory.Functor.Oplax
/-- More flexible variant of `mapId`. (See the file `Bicategory.Functor.Strict`
for applications to strict bicategories.)  -/
CategoryTheory.OplaxFunctor.mapId' : {B : Type u₁} →
  [inst : CategoryTheory.Bicategory B] →
    {C : Type u₂} →
      [inst_1 : CategoryTheory.Bicategory C] →
        (F : CategoryTheory.OplaxFunctor B C) →
          {b : B} →
            (f : b ⟶ b) →
              autoParam (f = CategoryTheory.CategoryStruct.id b) CategoryTheory.OplaxFunctor.mapId'._auto_1 →
                (F.map f ⟶ CategoryTheory.CategoryStruct.id (F.obj b))
-- Mathlib.Algebra.Group.Pi.Lemmas
Function.update_mul : ∀ {I : Type u} {f : I → Type v} [inst : (i : I) → Mul (f i)] [inst_1 : DecidableEq I] (f₁ f₂ : (i : I) → f i) (i : I)
  (x₁ x₂ : f i), Function.update (f₁ * f₂) i (x₁ * x₂) = Function.update f₁ i x₁ * Function.update f₂ i x₂
-- Mathlib.CategoryTheory.Sites.Grothendieck
CategoryTheory.GrothendieckTopology.Cover.Arrow.mk.injEq : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {X : C} {J : CategoryTheory.GrothendieckTopology C}
  {S : J.Cover X} (Y : C) (f : Y ⟶ X) (hf : (↑S).arrows f) (Y_1 : C) (f_1 : Y_1 ⟶ X) (hf_1 : (↑S).arrows f_1),
  ({ Y := Y, f := f, hf := hf } = { Y := Y_1, f := f_1, hf := hf_1 }) = (Y = Y_1 ∧ f ≍ f_1)
-- Lean.Language.Basic
/-- Applies the transformation to the given info tree.  -/
Lean.Language.SnapshotTreeTransform.transformInfoTree : Lean.Language.SnapshotTreeTransform → Lean.Elab.InfoTree → Lean.Elab.InfoTree
-- Mathlib.Algebra.Homology.ShortComplex.RightHomology
CategoryTheory.ShortComplex.p_opcyclesMap : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  {S₁ S₂ : CategoryTheory.ShortComplex C} [inst_2 : S₁.HasRightHomology] [inst_3 : S₂.HasRightHomology] (φ : S₁ ⟶ S₂),
  CategoryTheory.CategoryStruct.comp S₁.pOpcycles (CategoryTheory.ShortComplex.opcyclesMap φ) =
    CategoryTheory.CategoryStruct.comp φ.τ₂ S₂.pOpcycles
-- Mathlib.Analysis.Convex.Approximation
/-- The real version of `sSup_of_nat_affine_eq`.  -/
ConvexOn.real_sSup_of_nat_affine_eq : ∀ {E : Type u_2} {s : Set E} {φ : E → ℝ} [inst : TopologicalSpace E] [inst_1 : AddCommGroup E] [inst_2 : Module ℝ E]
  [IsTopologicalAddGroup E] [ContinuousSMul ℝ E] [LocallyConvexSpace ℝ E] [HereditarilyLindelofSpace E],
  IsClosed s →
    LowerSemicontinuousOn φ s →
      ConvexOn ℝ s φ →
        ∃ l c,
          (∀ (i : ℕ), s.domRestrict ⇑(l i) + Function.const (↑s) (c i) ≤ s.domRestrict φ) ∧
            ⨆ i, s.domRestrict ⇑(l i) + Function.const (↑s) (c i) = s.domRestrict φ
-- Mathlib.RingTheory.Localization.Away.AdjoinRoot
instFinitePresentationAway : ∀ {R : Type u_1} [inst : CommRing R] {S : Type u_2} [inst_1 : CommRing S] [inst_2 : Algebra R S]
  [Algebra.FinitePresentation R S] (f : S), Algebra.FinitePresentation R (Localization.Away f)
-- Mathlib.RingTheory.Valuation.ValuativeRel.Basic
ValuativeRel.vlt_of_vlt_of_vle : ∀ {R : Type u_1} [inst : Semiring R] [inst_1 : ValuativeRel R] {x y z : R}, x <ᵥ y → y ≤ᵥ z → x <ᵥ z
-- Mathlib.CategoryTheory.Monoidal.Rigid.Basic
/-- The left dual of a tensor product is isomorphic to the reversed tensor product of
the left duals.  -/
CategoryTheory.leftDualTensorIso : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    [inst_1 : CategoryTheory.MonoidalCategory C] →
      (X Y : C) →
        [inst_2 : CategoryTheory.HasLeftDual X] →
          [inst_3 : CategoryTheory.HasLeftDual Y] →
            [inst_4 : CategoryTheory.HasLeftDual (CategoryTheory.MonoidalCategoryStruct.tensorObj X Y)] →
              ᘁ(CategoryTheory.MonoidalCategoryStruct.tensorObj X Y) ≅
                CategoryTheory.MonoidalCategoryStruct.tensorObj ᘁY ᘁX
-- Mathlib.Data.Multiset.Fintype
Multiset.map_univ_comp_coe : ∀ {α : Type u_1} [inst : DecidableEq α] {β : Type u_3} (m : Multiset α) (f : α → β),
  Multiset.map (f ∘ fun x => x.fst) Finset.univ.val = Multiset.map f m
-- Lean.Environment
Lean.Kernel.Environment.Diagnostics.isEnabled : Lean.Kernel.Diagnostics → Bool
-- Mathlib.Algebra.Order.Module.Defs
/-- Scalar multiplication on the left by a positive element preserves strict antitonicity.  -/
StrictAnti.const_smul : ∀ {α : Type u_1} {β : Type u_2} {a : α} [inst : SMul α β] [inst_1 : Preorder α] [inst_2 : Preorder β] [inst_3 : Zero α]
  [PosSMulStrictMono α β] {γ : Type u_3} [inst_5 : Preorder γ] {f : γ → β},
  StrictAnti f → 0 < a → StrictAnti fun x => a • f x
-- Mathlib.NumberTheory.LegendreSymbol.JacobiSymbol
/-- We can pull out a product over a list in the second argument of the Jacobi symbol.  -/
jacobiSym.list_prod_right : ∀ {a : ℤ} {l : List ℕ}, (∀ n ∈ l, n ≠ 0) → jacobiSym a l.prod = (List.map (fun n => jacobiSym a n) l).prod
-- Init.Data.List.MinMax
List.max_le_iff : ∀ {α : Type u_1} [inst : Max α] [inst_1 : LE α] [Std.LawfulOrderSup α] {l : List α} (hl : l ≠ []) {x : α},
  l.max hl ≤ x ↔ ∀ b ∈ l, b ≤ x
-- Mathlib.Data.Set.Sups
Set.Nonempty.of_infs_left : ∀ {α : Type u_2} [inst : SemilatticeInf α] {s t : Set α}, (s ⊼ t).Nonempty → s.Nonempty