mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.CategoryTheory.Dialectica.Basic
/-- Maps the targets (contravariantly)  -/
CategoryTheory.Dial.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.Hom Y → (X.src ⨯ Y.tgt ⟶ X.tgt)
-- Mathlib.Data.List.Forall2
List.sublistForall₂_map_left_iff : ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} {R : α → β → Prop} {f : γ → α} {l₁ : List γ} {l₂ : List β},
  List.SublistForall₂ R (List.map f l₁) l₂ ↔ List.SublistForall₂ (fun c b => R (f c) b) l₁ l₂
-- Lean.Parser.Extension
Lean.Parser.builtinSyntaxNodeKindSetRef : IO.Ref Lean.Parser.SyntaxNodeKindSet
-- Mathlib.Topology.Category.Locale
topToLocale_obj : ∀ (X : TopCat), topToLocale.obj X = Opposite.op (topCatOpToFrm.obj (Opposite.op X))
-- Mathlib.Data.Finset.Image
Finset.map_disjUnion : ∀ {α : Type u_1} {β : Type u_2} {f : α ↪ β} (s₁ s₂ : Finset α) (h : Disjoint s₁ s₂)
  (h' : optParam (Disjoint (Finset.map f s₁) (Finset.map f s₂)) ⋯),
  Finset.map f (s₁.disjUnion s₂ h) = (Finset.map f s₁).disjUnion (Finset.map f s₂) h'
-- Mathlib.Data.NNRat.Floor
Mathlib.Meta.NormNum.IsInt.natCeil : ∀ {R : Type u_1} [inst : Ring R] [inst_1 : LinearOrder R] [IsStrictOrderedRing R] [inst_3 : FloorSemiring R] (r : R)
  (m : ℕ), Mathlib.Meta.NormNum.IsInt r (Int.negOfNat m) → Mathlib.Meta.NormNum.IsNat ⌈r⌉₊ 0
-- Mathlib.Tactic.Linarith.Oracle.SimplexAlgorithm.SimplexAlgorithm
Mathlib.Tactic.Linarith.SimplexAlgorithm.SimplexAlgorithmException.infeasible.sizeOf_spec : sizeOf Mathlib.Tactic.Linarith.SimplexAlgorithm.SimplexAlgorithmException.infeasible = 1
-- Std.Data.DTreeMap.Lemmas
Std.DTreeMap.Const.length_toList : ∀ {α : Type u} {cmp : α → α → Ordering} {β : Type v} {t : Std.DTreeMap α (fun x => β) cmp},
  (Std.DTreeMap.Const.toList t).length = t.size
-- Mathlib.CategoryTheory.Limits.Cones
CategoryTheory.Limits.Cocone.whisker.eq_1 : ∀ {J : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} J] {K : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} K]
  {C : Type u₃} [inst_2 : CategoryTheory.Category.{v₃, u₃} C] {F : CategoryTheory.Functor J C}
  (E : CategoryTheory.Functor K J) (c : CategoryTheory.Limits.Cocone F),
  CategoryTheory.Limits.Cocone.whisker E c = { pt := c.pt, ι := E.whiskerLeft c.ι }
-- Lean.Data.Lsp.LanguageFeatures
Lean.Lsp.FoldingRangeParams.textDocument : Lean.Lsp.FoldingRangeParams → Lean.Lsp.TextDocumentIdentifier
-- Mathlib.Topology.Algebra.Group.Basic
Submonoid.units_isCompact : ∀ {α : Type u} [inst : Monoid α] [inst_1 : TopologicalSpace α] [T1Space α] [ContinuousMul α] {S : Submonoid α},
  IsCompact ↑S → IsCompact ↑S.units
-- Lean.Expr
/-- Annotate `e` with `pp.funBinderTypes := flag`
The delaborator uses `pp` options.
 -/
Lean.Expr.setPPFunBinderTypes : Lean.Expr → Bool → Lean.Expr
-- Batteries.Data.BinomialHeap.Basic
Batteries.BinomialHeap.Imp.Heap.realSize_merge : ∀ {α : Type u_1} (le : α → α → Bool) (s₁ s₂ : Batteries.BinomialHeap.Imp.Heap α),
  (Batteries.BinomialHeap.Imp.Heap.merge le s₁ s₂).realSize = s₁.realSize + s₂.realSize
-- Mathlib.CategoryTheory.ObjectProperty.ColimitsClosure
CategoryTheory.ObjectProperty.colimitsClosure.brecOn : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {P : CategoryTheory.ObjectProperty C} {α : Type t}
  {J : α → Type u'} [inst_1 : (a : α) → CategoryTheory.Category.{v', u'} (J a)]
  {motive : (a : C) → P.colimitsClosure J a → Prop} {a : C} (t : P.colimitsClosure J a),
  (∀ (a : C) (t : P.colimitsClosure J a), CategoryTheory.ObjectProperty.colimitsClosure.below t → motive a t) →
    motive a t
-- Batteries.Data.BitVec.Lemmas
BitVec.msb_ofFnLE : ∀ {n : ℕ} (f : Fin n → Bool), (BitVec.ofFnLE f).msb = if h : n ≠ 0 then f ⟨n - 1, ⋯⟩ else false
-- Mathlib.Tactic.NormNum.Basic
/-- The `norm_num` extension which identifies an expression `OfNat.ofNat n`, returning `n`.  -/
Mathlib.Meta.NormNum.evalOfNat : Mathlib.Meta.NormNum.NormNumExt
-- Mathlib.Analysis.InnerProductSpace.TensorProduct
TensorProduct.norm_tmul : ∀ {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [inst : RCLike 𝕜] [inst_1 : NormedAddCommGroup E]
  [inst_2 : InnerProductSpace 𝕜 E] [inst_3 : NormedAddCommGroup F] [inst_4 : InnerProductSpace 𝕜 F] (x : E) (y : F),
  ‖x ⊗ₜ[𝕜] y‖ = ‖x‖ * ‖y‖
-- Init.Data.List.Lemmas
List.filter_cons_of_pos : ∀ {α : Type u_1} {p : α → Bool} {a : α} {l : List α}, p a = true → List.filter p (a :: l) = a :: List.filter p l
-- Lean.Meta.Tactic.Grind.Types
Lean.Meta.Grind.instInhabitedGoalState.default : Lean.Meta.Grind.GoalState
-- Mathlib.CategoryTheory.Sites.Hypercover.Zero
CategoryTheory.Precoverage.ZeroHypercover.id_h₀ : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {J : CategoryTheory.Precoverage C} {S : C}
  (x : J.ZeroHypercover S) (x_1 : x.I₀),
  (CategoryTheory.CategoryStruct.id x).h₀ x_1 = CategoryTheory.CategoryStruct.id (x.X x_1)
-- Mathlib.CategoryTheory.Bicategory.Modification.Oplax
/-- Construct a modification isomorphism between strong natural transformations (of oplax functors)
by giving object level isomorphisms, and checking naturality only in the forward direction.
 -/
CategoryTheory.Oplax.StrongTrans.isoMk : {B : Type u₁} →
  [inst : CategoryTheory.Bicategory B] →
    {C : Type u₂} →
      [inst_1 : CategoryTheory.Bicategory C] →
        {F G : CategoryTheory.OplaxFunctor B C} →
          {η θ : F ⟶ G} →
            (app : (a : B) → η.app a ≅ θ.app a) →
              autoParam
                  (∀ {a b : B} (f : a ⟶ b),
                    CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.whiskerLeft (F.map f) (app b).hom)
                        (θ.naturality f).hom =
                      CategoryTheory.CategoryStruct.comp (η.naturality f).hom
                        (CategoryTheory.Bicategory.whiskerRight (app a).hom (G.map f)))
                  CategoryTheory.Oplax.StrongTrans.isoMk._auto_1 →
                (η ≅ θ)
-- Mathlib.MeasureTheory.OuterMeasure.Operations
MeasureTheory.OuterMeasure.map_comap : ∀ {α : Type u_1} {β : Type u_3} (f : α → β) (m : MeasureTheory.OuterMeasure β),
  (MeasureTheory.OuterMeasure.map f) ((MeasureTheory.OuterMeasure.comap f) m) =
    (MeasureTheory.OuterMeasure.restrict (Set.range f)) m
-- Mathlib.Algebra.Polynomial.Eval.Defs
Polynomial.X_pow_comp : ∀ {R : Type u} [inst : Semiring R] {p : Polynomial R} {k : ℕ}, (Polynomial.X ^ k).comp p = p ^ k
-- Mathlib.Algebra.Group.Equiv.Basic
MulEquiv.monoidHomCongrRightEquiv_refl : ∀ {M : Type u_4} {N : Type u_8} [inst : MulOneClass M] [inst_1 : Monoid N],
  (MulEquiv.refl N).monoidHomCongrRightEquiv = Equiv.refl (M →* N)
-- Init.Grind.Ring.CommSolver
Lean.Grind.CommRing.Poly.denoteTerm_eq : ∀ {α : Type u_1} [inst : Lean.Grind.Ring α] (ctx : Lean.Grind.CommRing.Context α) (k : ℤ) (m : Lean.Grind.CommRing.Mon),
  Lean.Grind.CommRing.denoteTerm ctx k m = ↑k * Lean.Grind.CommRing.Mon.denote ctx m
-- Mathlib.GroupTheory.Torsion
/-- A nontrivial torsion additive abelian group is not torsion-free.  -/
not_isAddTorsionFree_of_isAddTorsion : ∀ {G : Type u_1} [inst : AddCommGroup G] [Nontrivial G], IsAddTorsion G → ¬IsAddTorsionFree G
-- Mathlib.ModelTheory.Bundled
FirstOrder.Language.Theory.ModelType.mk.inj : ∀ {L : FirstOrder.Language} {T : L.Theory} {Carrier : Type w} {struc : L.Structure Carrier} {is_model : Carrier ⊨ T}
  {nonempty' : Nonempty Carrier} {Carrier_1 : Type w} {struc_1 : L.Structure Carrier_1} {is_model_1 : Carrier_1 ⊨ T}
  {nonempty'_1 : Nonempty Carrier_1},
  { Carrier := Carrier, struc := struc, is_model := is_model, nonempty' := nonempty' } =
      { Carrier := Carrier_1, struc := struc_1, is_model := is_model_1, nonempty' := nonempty'_1 } →
    Carrier = Carrier_1 ∧ struc ≍ struc_1
-- Std.Data.TreeSet.Raw.Lemmas
Std.TreeSet.Raw.get?_diff : ∀ {α : Type u} {cmp : α → α → Ordering} {t₁ t₂ : Std.TreeSet.Raw α cmp} [Std.TransCmp cmp],
  t₁.WF → t₂.WF → ∀ {k : α}, (t₁ \ t₂).get? k = if k ∈ t₂ then none else t₁.get? k
-- Mathlib.RingTheory.DiscreteValuationRing.Basic
IsDiscreteValuationRing.idealOrderIsoENat_apply : ∀ (R : Type u_1) [inst : CommRing R] [inst_1 : IsDomain R] [inst_2 : IsDiscreteValuationRing R] (I : Ideal R),
  (IsDiscreteValuationRing.idealOrderIsoENat R) I =
    OrderDual.toDual ((IsDiscreteValuationRing.addVal R) (Submodule.IsPrincipal.generator I))
-- Mathlib.RepresentationTheory.Rep.Basic
Rep.tensor_ρ : ∀ {k : Type u} {G : Type v} [inst : CommRing k] [inst_1 : Monoid G] {X Y : Rep.{u, u, v} k G},
  (CategoryTheory.MonoidalCategoryStruct.tensorObj X Y).ρ = X.ρ.tprod Y.ρ
-- Mathlib.Order.Sublattice
Sublattice.mk : {α : Type u_2} → [inst : Lattice α] → (carrier : Set α) → SupClosed carrier → InfClosed carrier → Sublattice α
-- Mathlib.Algebra.Ring.SumsOfSquares
/-- Alternative induction scheme for `IsSumSq` which uses `IsSquare`.  -/
IsSumSq.rec' : ∀ {R : Type u_1} [inst : Mul R] [inst_1 : Add R] [inst_2 : Zero R] {motive : (s : R) → IsSumSq s → Prop},
  motive 0 ⋯ →
    (∀ {x s : R} (hx : IsSquare x) (hs : IsSumSq s), motive s hs → motive (x + s) ⋯) →
      ∀ {s : R} (h : IsSumSq s), motive s h
-- Mathlib.Topology.Category.TopCat.Sphere
/-- The `n`-ball is the set of points in ℝⁿ whose norm is strictly less than `1`,
endowed with the subspace topology.  -/
TopCat.ball : ℕ → TopCat
-- Mathlib.Algebra.Order.Group.Pointwise.Interval
Set.Ico_mul_Icc_subset' : ∀ {α : Type u_1} [inst : Mul α] [inst_1 : PartialOrder α] [MulLeftStrictMono α] [MulRightStrictMono α] (a b c d : α),
  Set.Ico a b * Set.Icc c d ⊆ Set.Ico (a * c) (b * d)
-- Mathlib.Data.TypeVec
TypeVec.drop_append1 : ∀ {n : ℕ} {α : TypeVec.{u_1} n} {β : Type u_1} {i : Fin2 n}, (α ::: β).drop i = α i
-- Mathlib.Combinatorics.SimpleGraph.Regularity.Uniform
Finpartition.nonempty_of_not_uniform : ∀ {α : Type u_1} {𝕜 : Type u_2} [inst : Field 𝕜] [inst_1 : LinearOrder 𝕜] [inst_2 : DecidableEq α] {A : Finset α}
  {P : Finpartition A} {G : SimpleGraph α} [inst_3 : DecidableRel G.Adj] {ε : 𝕜}, ¬P.IsUniform G ε → P.parts.Nonempty
-- Std.Data.DTreeMap.Raw.Lemmas
Std.DTreeMap.Raw.mem_insertIfNew_self : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t : Std.DTreeMap.Raw α β cmp} [Std.TransCmp cmp],
  t.WF → ∀ {k : α} {v : β k}, k ∈ t.insertIfNew k v
-- Init.Data.Nat.Lemmas
Nat.min_max_distrib_right : ∀ (a b c : ℕ), min (max a b) c = max (min a c) (min b c)
-- Mathlib.GroupTheory.Sylow
/-- A generalization of **Sylow's third theorem**.
If the number of Sylow `p`-subgroups is finite, then it is congruent to `1` modulo `p`.  -/
card_sylow_modEq_one : ∀ (p : ℕ) (G : Type u_1) [inst : Group G] [Fact (Nat.Prime p)] [Finite (Sylow p G)], Nat.card (Sylow p G) ≡ 1 [MOD p]
-- Mathlib.RingTheory.DividedPowers.RatAlgebra
/-- The family `ℕ → R → R` given by `dpow n x = x ^ n / n!`.  -/
DividedPowers.RatAlgebra.dpow : {R : Type u_1} → [inst : CommSemiring R] → (I : Ideal R) → [DecidablePred fun x => x ∈ I] → ℕ → R → R
-- Lean.Server.InfoUtils
Lean.Elab.InfoWithCtx.mk : Lean.Elab.ContextInfo → Lean.Elab.Info → Lean.PersistentArray Lean.Elab.InfoTree → Lean.Elab.InfoWithCtx
-- Mathlib.MeasureTheory.Function.SimpleFunc
MeasureTheory.SimpleFunc.piecewise_same : ∀ {α : Type u_1} {β : Type u_2} [inst : MeasurableSpace α] (f : MeasureTheory.SimpleFunc α β) {s : Set α}
  (hs : MeasurableSet s), MeasureTheory.SimpleFunc.piecewise s hs f f = f
-- Std.Data.ExtDTreeMap.Lemmas
Std.ExtDTreeMap.Const.get?_empty : ∀ {α : Type u} {cmp : α → α → Ordering} {β : Type v} [inst : Std.TransCmp cmp] {a : α},
  Std.ExtDTreeMap.Const.get? ∅ a = none
-- Mathlib.Order.ConditionallyCompleteLattice.Indexed
/-- If the set of all `f i j` is bounded above, then so is the set of the supremums of every row  -/
BddAbove.range_iSup_of_iUnion_range : ∀ {α : Type u_1} {ι : Sort u_4} [inst : ConditionallyCompleteLattice α] {κ : ι → Sort u_5} {f : (i : ι) → κ i → α},
  BddAbove (⋃ i, Set.range (f i)) → BddAbove (Set.range fun i => ⨆ j, f i j)
-- Lean.Elab.App
/-- Return `true` if `declName` is a candidate for `ElabElim.main` elaboration.  -/
_private.Lean.Elab.App.0.Lean.Elab.Term.shouldElabAsElim : Lean.Name → Lean.CoreM Bool
-- Init.Data.UInt.Lemmas
USize.ofFin_mod : ∀ (a b : Fin USize.size), USize.ofFin (a % b) = USize.ofFin a % USize.ofFin b
-- Mathlib.Algebra.GroupWithZero.Basic
zpow_add_one₀ : ∀ {G₀ : Type u_2} [inst : GroupWithZero G₀] {a : G₀}, a ≠ 0 → ∀ (n : ℤ), a ^ (n + 1) = a ^ n * a
-- Mathlib.Geometry.Euclidean.Angle.Unoriented.Affine
/-- The angle at a point is nonnegative.  -/
EuclideanGeometry.angle_nonneg : ∀ {V : Type u_1} {P : Type u_2} [inst : NormedAddCommGroup V] [inst_1 : InnerProductSpace ℝ V] [inst_2 : MetricSpace P]
  [inst_3 : NormedAddTorsor V P] (p₁ p₂ p₃ : P), 0 ≤ EuclideanGeometry.angle p₁ p₂ p₃
-- Lean.Compiler.CSimpAttr
Lean.Compiler.CSimp.Entry.mk : Lean.Name → Lean.Name → Lean.Name → Lean.Compiler.CSimp.Entry
-- Lean.Declaration
Lean.ConstructorVal.mk.inj : ∀ {toConstantVal : Lean.ConstantVal} {induct : Lean.Name} {cidx numParams numFields : ℕ} {isUnsafe : Bool}
  {toConstantVal_1 : Lean.ConstantVal} {induct_1 : Lean.Name} {cidx_1 numParams_1 numFields_1 : ℕ} {isUnsafe_1 : Bool},
  { toConstantVal := toConstantVal, induct := induct, cidx := cidx, numParams := numParams, numFields := numFields,
        isUnsafe := isUnsafe } =
      { toConstantVal := toConstantVal_1, induct := induct_1, cidx := cidx_1, numParams := numParams_1,
        numFields := numFields_1, isUnsafe := isUnsafe_1 } →
    toConstantVal = toConstantVal_1 ∧
      induct = induct_1 ∧ cidx = cidx_1 ∧ numParams = numParams_1 ∧ numFields = numFields_1 ∧ isUnsafe = isUnsafe_1
-- Mathlib.Analysis.Calculus.Deriv.Abs
ContDiffOn.abs : ∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] {n : ℕ∞} {f : E → ℝ} {s : Set E},
  ContDiffOn ℝ (↑n) f s → (∀ x ∈ s, f x ≠ 0) → ContDiffOn ℝ (↑n) (fun y => |f y|) s
-- Mathlib.Algebra.Order.Monoid.Unbundled.WithTop
WithBot.ofNat_eq_map_iff : ∀ {α : Type u} {β : Type v} [inst : AddMonoidWithOne α] {f : β → α} {n : ℕ} [inst_1 : n.AtLeastTwo] {a : WithBot β},
  OfNat.ofNat n = WithBot.map f a ↔ ∃ x, a = ↑x ∧ f x = ↑n
-- Mathlib.Algebra.BigOperators.Fin
Fin.partialSum_succ' : ∀ {M : Type u_2} [inst : AddMonoid M] {n : ℕ} (f : Fin (n + 1) → M) (j : Fin (n + 1)),
  Fin.partialSum f j.succ = f 0 + Fin.partialSum (Fin.tail f) j
-- Mathlib.CategoryTheory.Limits.Shapes.End
CategoryTheory.Limits.coend.ι_desc_assoc : ∀ {J : Type u} [inst : CategoryTheory.Category.{v, u} J] {C : Type u'} [inst_1 : CategoryTheory.Category.{v', u'} C]
  {F : CategoryTheory.Functor Jᵒᵖ (CategoryTheory.Functor J C)} [inst_2 : CategoryTheory.Limits.HasCoend F] {X : C}
  (f : (j : J) → (F.obj (Opposite.op j)).obj j ⟶ X)
  (hf :
    ∀ ⦃i j : J⦄ (g : i ⟶ j),
      CategoryTheory.CategoryStruct.comp ((F.map g.op).app i) (f i) =
        CategoryTheory.CategoryStruct.comp ((F.obj (Opposite.op j)).map g) (f j))
  (j : J) {Z : C} (h : X ⟶ Z),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.coend.ι F j)
      (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.coend.desc f hf) h) =
    CategoryTheory.CategoryStruct.comp (f j) h
-- Mathlib.Analysis.SpecialFunctions.Trigonometric.DerivHyp
HasStrictFDerivAt.cosh : ∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] {f : E → ℝ} {f' : StrongDual ℝ E} {x : E},
  HasStrictFDerivAt f f' x → HasStrictFDerivAt (fun x => Real.cosh (f x)) (Real.sinh (f x) • f') x
-- Mathlib.CategoryTheory.Limits.Shapes.Pullback.Categorical.CatCospanTransform
CategoryTheory.Limits.CatCospanTransform.mk.injEq : ∀ {A : Type u₁} {B : Type u₂} {C : Type u₃} [inst : CategoryTheory.Category.{v₁, u₁} A]
  [inst_1 : CategoryTheory.Category.{v₂, u₂} B] [inst_2 : CategoryTheory.Category.{v₃, u₃} C]
  {F : CategoryTheory.Functor A B} {G : CategoryTheory.Functor C B} {A' : Type u₄} {B' : Type u₅} {C' : Type u₆}
  [inst_3 : CategoryTheory.Category.{v₄, u₄} A'] [inst_4 : CategoryTheory.Category.{v₅, u₅} B']
  [inst_5 : CategoryTheory.Category.{v₆, u₆} C'] {F' : CategoryTheory.Functor A' B'} {G' : CategoryTheory.Functor C' B'}
  (left : CategoryTheory.Functor A A') (base : CategoryTheory.Functor B B') (right : CategoryTheory.Functor C C')
  (squareLeft :
    autoParam (CategoryTheory.CatCommSq F left base F') CategoryTheory.Limits.CatCospanTransform.squareLeft._autoParam)
  (squareRight :
    autoParam (CategoryTheory.CatCommSq G right base G')
      CategoryTheory.Limits.CatCospanTransform.squareRight._autoParam)
  (left_1 : CategoryTheory.Functor A A') (base_1 : CategoryTheory.Functor B B') (right_1 : CategoryTheory.Functor C C')
  (squareLeft_1 :
    autoParam (CategoryTheory.CatCommSq F left_1 base_1 F')
      CategoryTheory.Limits.CatCospanTransform.squareLeft._autoParam)
  (squareRight_1 :
    autoParam (CategoryTheory.CatCommSq G right_1 base_1 G')
      CategoryTheory.Limits.CatCospanTransform.squareRight._autoParam),
  ({ left := left, base := base, right := right, squareLeft := squareLeft, squareRight := squareRight } =
      { left := left_1, base := base_1, right := right_1, squareLeft := squareLeft_1, squareRight := squareRight_1 }) =
    (left = left_1 ∧ base = base_1 ∧ right = right_1 ∧ squareLeft ≍ squareLeft_1 ∧ squareRight ≍ squareRight_1)
-- Mathlib.Order.Partition.Finpartition
Finpartition.mk.sizeOf_spec : ∀ {α : Type u_1} [inst : Lattice α] [inst_1 : OrderBot α] {a : α} [inst_2 : SizeOf α] (parts : Finset α)
  (supIndep : parts.SupIndep id) (sup_parts : parts.sup id = a) (bot_notMem : ⊥ ∉ parts),
  sizeOf { parts := parts, supIndep := supIndep, sup_parts := sup_parts, bot_notMem := bot_notMem } =
    1 + sizeOf parts + sizeOf sup_parts
-- Mathlib.GroupTheory.FreeGroup.Basic
/-- Equivalent types give rise to additively equivalent additive free groups.  -/
FreeAddGroup.freeAddGroupCongr : {α : Type u_1} → {β : Type u_2} → α ≃ β → FreeAddGroup α ≃+ FreeAddGroup β
-- Mathlib.Algebra.CubicDiscriminant
Cubic.monic_of_d_eq_one : ∀ {R : Type u_1} {P : Cubic R} [inst : Semiring R], P.a = 0 → P.b = 0 → P.c = 0 → P.d = 1 → P.toPoly.Monic
-- Lean.Meta.Tactic.Cases
Lean.Meta.ByCasesSubgoal.mk.injEq : ∀ (mvarId : Lean.MVarId) (fvarId : Lean.FVarId) (mvarId_1 : Lean.MVarId) (fvarId_1 : Lean.FVarId),
  ({ mvarId := mvarId, fvarId := fvarId } = { mvarId := mvarId_1, fvarId := fvarId_1 }) =
    (mvarId = mvarId_1 ∧ fvarId = fvarId_1)
-- Lean.Server.InfoUtils
/-- `InfoTree.visitM` specialized to `Unit` return type  -/
Lean.Elab.InfoTree.visitM' : {m : Type → Type u_1} →
  [inst : Monad m] →
    (optParam (Lean.Elab.ContextInfo → Lean.Elab.Info → Lean.PersistentArray Lean.Elab.InfoTree → m Bool)
        fun x x_1 x_2 => pure true) →
      (optParam (Lean.Elab.ContextInfo → Lean.Elab.Info → Lean.PersistentArray Lean.Elab.InfoTree → m Unit)
          fun x x_1 x_2 => pure ()) →
        optParam (Option Lean.Elab.ContextInfo) none → Lean.Elab.InfoTree → m Unit
-- Mathlib.ModelTheory.Syntax
FirstOrder.Language.LHom.mem_onTheory : ∀ {L : FirstOrder.Language} {L' : FirstOrder.Language} {g : L →ᴸ L'} {T : L.Theory} {φ : L'.Sentence},
  φ ∈ g.onTheory T ↔ ∃ φ₀ ∈ T, g.onSentence φ₀ = φ
-- Mathlib.NumberTheory.ModularForms.QExpansion
_private.Mathlib.NumberTheory.ModularForms.QExpansion.0.«termI∞» : Lean.ParserDescr
-- Mathlib.Algebra.Order.Antidiag.Pi
/-- `finAntidiagonal d n` is the type of `d`-tuples with sum `n`.

TODO: deduplicate with the less general `Finset.Nat.antidiagonalTuple`.  -/
Finset.finAntidiagonal : {μ : Type u_2} →
  [inst : AddCommMonoid μ] → [Finset.HasAntidiagonal μ] → [DecidableEq μ] → (d : ℕ) → μ → Finset (Fin d → μ)
-- Mathlib.Data.Set.Semiring
/-- An alias for `Set α`, which has a semiring structure given by `∪` as "addition" and pointwise
multiplication `*` as "multiplication".  -/
SetSemiring : Type u_3 → Type u_3
-- Mathlib.CategoryTheory.Monoidal.Grp
CategoryTheory.Grp.mkIso'_inv_hom_hom : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.CartesianMonoidalCategory C]
  {G H : C} (e : G ≅ H) [inst_2 : CategoryTheory.GrpObj G] [inst_3 : CategoryTheory.GrpObj H]
  [inst_4 : CategoryTheory.IsMonHom e.hom], (CategoryTheory.Grp.mkIso' e).inv.hom.hom = e.inv
-- Init.Data.List.Lemmas
List.mem_flatMap : ∀ {α : Type u_1} {β : Type u_2} {f : α → List β} {b : β} {l : List α}, b ∈ List.flatMap f l ↔ ∃ a ∈ l, b ∈ f a
-- Mathlib.Analysis.SpecialFunctions.Trigonometric.DerivHyp
Complex.iteratedDeriv_even_cosh : ∀ (n : ℕ), iteratedDeriv (2 * n) Complex.cosh = Complex.cosh
-- Mathlib.CategoryTheory.Sites.Grothendieck
/-- Constructor for `Cover.Relation` which takes as an input
`r : I₁.Relation I₂` with `I₁ I₂ : S.Arrow`.  -/
CategoryTheory.GrothendieckTopology.Cover.Relation.mk' : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    {X : C} →
      {J : CategoryTheory.GrothendieckTopology C} →
        {S : J.Cover X} → {fst snd : S.Arrow} → fst.Relation snd → S.Relation
-- Mathlib.GroupTheory.FreeGroup.IsFreeGroup
/-- Any additive free group is isomorphic to "the" additive free group.  -/
IsFreeAddGroup.addEquiv : (G : Type u_2) → [inst : AddGroup G] → [inst_1 : IsFreeAddGroup G] → FreeAddGroup (IsFreeAddGroup.Generators G) ≃+ G
-- Mathlib.CategoryTheory.Abelian.Preradical.Colon
CategoryTheory.Abelian.Preradical.shortComplex_X₃ : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{u_2, u_1} C] [inst_1 : CategoryTheory.Abelian C]
  (Φ : CategoryTheory.Abelian.Preradical C), Φ.shortComplex.X₃ = Φ.quotient
-- Mathlib.CategoryTheory.WithTerminal.Basic
CategoryTheory.WithInitial.star.sizeOf_spec : ∀ {C : Type u} [inst : SizeOf C], sizeOf CategoryTheory.WithInitial.star = 1
-- Mathlib.CategoryTheory.Limits.Shapes.Pullback.Categorical.CatCospanTransform
CategoryTheory.Limits.CatCospanTransform.leftUnitor_inv_right_app : ∀ {A : Type u₁} {B : Type u₂} {C : Type u₃} {A' : Type u₄} {B' : Type u₅} {C' : Type u₆}
  [inst : CategoryTheory.Category.{v₁, u₁} A] [inst_1 : CategoryTheory.Category.{v₂, u₂} B]
  [inst_2 : CategoryTheory.Category.{v₃, u₃} C] {F : CategoryTheory.Functor A B} {G : CategoryTheory.Functor C B}
  [inst_3 : CategoryTheory.Category.{v₄, u₄} A'] [inst_4 : CategoryTheory.Category.{v₅, u₅} B']
  [inst_5 : CategoryTheory.Category.{v₆, u₆} C'] {F' : CategoryTheory.Functor A' B'} {G' : CategoryTheory.Functor C' B'}
  (φ : CategoryTheory.Limits.CatCospanTransform F G F' G') (X : C),
  φ.leftUnitor.inv.right.app X = CategoryTheory.CategoryStruct.id (φ.right.obj X)
-- Std.Tactic.BVDecide.LRAT.Internal.Entails
/-- For variables of type `α` and formulas of type `β`, `Entails.eval a f` is meant to determine whether
a formula `f` is true under assignment `a`.
 -/
Std.Tactic.BVDecide.LRAT.Internal.Entails : Type u → Type v → Type (max u v)
-- Mathlib.Topology.Algebra.InfiniteSum.Group
HasSum.neg : ∀ {α : Type u_1} {β : Type u_2} {L : SummationFilter β} [inst : AddCommGroup α] [inst_1 : TopologicalSpace α]
  [IsTopologicalAddGroup α] {f : β → α} {a : α}, HasSum f a L → HasSum (fun b => -f b) (-a) L
-- Mathlib.Algebra.Group.Submonoid.Operations
AddSubmonoid.le_pi_iff : ∀ {ι : Type u_4} {M : ι → Type u_5} [inst : (i : ι) → AddZeroClass (M i)] {I : Set ι} {S : (i : ι) → AddSubmonoid (M i)}
  {J : AddSubmonoid ((i : ι) → M i)},
  J ≤ AddSubmonoid.pi I S ↔ ∀ i ∈ I, J ≤ AddSubmonoid.comap (Pi.evalAddMonoidHom M i) (S i)
-- Mathlib.Algebra.Polynomial.Inductions
Polynomial.divX_mul_X_add : ∀ {R : Type u} [inst : Semiring R] (p : Polynomial R), p.divX * Polynomial.X + Polynomial.C (p.coeff 0) = p
-- Mathlib.AlgebraicTopology.ModelCategory.IsCofibrant
HomotopicalAlgebra.isFibrant_iff : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : HomotopicalAlgebra.CategoryWithFibrations C]
  [inst_2 : CategoryTheory.Limits.HasTerminal C] (X : C),
  HomotopicalAlgebra.IsFibrant X ↔ HomotopicalAlgebra.Fibration (CategoryTheory.Limits.terminal.from X)
-- Mathlib.GroupTheory.CoprodI
Monoid.CoprodI.NeWord.toList.eq_1 : ∀ {ι : Type u_1} {M : ι → Type u_2} [inst : (i : ι) → Monoid (M i)] (x : ι) (x_3 : M x) (a : x_3 ≠ 1),
  (Monoid.CoprodI.NeWord.singleton x_3 a).toList = [⟨x, x_3⟩]
-- Std.Data.DHashMap.RawLemmas
Std.DHashMap.Raw.isEmpty_insert : ∀ {α : Type u} {β : α → Type v} {m : Std.DHashMap.Raw α β} [inst : BEq α] [inst_1 : Hashable α] [EquivBEq α]
  [LawfulHashable α], m.WF → ∀ {k : α} {v : β k}, (m.insert k v).isEmpty = false
-- Mathlib.LinearAlgebra.Projection
Submodule.projectionOnto_apply_of_mem_left : ∀ {R : Type u_1} [inst : Ring R] {E : Type u_2} [inst_1 : AddCommGroup E] [inst_2 : Module R E] {p q : Submodule R E}
  (hpq : IsCompl p q) {x : E} (hx : x ∈ p), (p.projectionOnto q hpq) x = ⟨x, hx⟩