mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Logic.Equiv.PartialEquiv
/-- Combine two `PartialEquiv`s with disjoint sources and disjoint targets. We reuse
`PartialEquiv.piecewise`, then override `source` and `target` to ensure better definitional
equalities.  -/
PartialEquiv.disjointUnion : {α : Type u_1} →
  {β : Type u_2} →
    (e e' : PartialEquiv α β) →
      Disjoint e.source e'.source →
        Disjoint e.target e'.target →
          [(x : α) → Decidable (x ∈ e.source)] → [(y : β) → Decidable (y ∈ e.target)] → PartialEquiv α β
-- Mathlib.CategoryTheory.Sites.CompatiblePlus
CategoryTheory.GrothendieckTopology.plusCompIso_whiskerLeft : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] (J : CategoryTheory.GrothendieckTopology C) {D : Type u_1}
  [inst_1 : CategoryTheory.Category.{v_1, u_1} D] {E : Type u_2} [inst_2 : CategoryTheory.Category.{v_2, u_2} E]
  [inst_3 :
    ∀ (J : CategoryTheory.Limits.MulticospanShape),
      CategoryTheory.Limits.HasLimitsOfShape (CategoryTheory.Limits.WalkingMulticospan J) D]
  [inst_4 :
    ∀ (J : CategoryTheory.Limits.MulticospanShape),
      CategoryTheory.Limits.HasLimitsOfShape (CategoryTheory.Limits.WalkingMulticospan J) E]
  [inst_5 : ∀ (X : C), CategoryTheory.Limits.HasColimitsOfShape (J.Cover X)ᵒᵖ D]
  [inst_6 : ∀ (X : C), CategoryTheory.Limits.HasColimitsOfShape (J.Cover X)ᵒᵖ E] {F G : CategoryTheory.Functor D E}
  (η : F ⟶ G) (P : CategoryTheory.Functor Cᵒᵖ D)
  [inst_7 : ∀ (X : C), CategoryTheory.Limits.PreservesColimitsOfShape (J.Cover X)ᵒᵖ F]
  [inst_8 :
    ∀ (X : C) (W : J.Cover X) (P : CategoryTheory.Functor Cᵒᵖ D),
      CategoryTheory.Limits.PreservesLimit (W.index P).multicospan F]
  [inst_9 : ∀ (X : C), CategoryTheory.Limits.PreservesColimitsOfShape (J.Cover X)ᵒᵖ G]
  [inst_10 :
    ∀ (X : C) (W : J.Cover X) (P : CategoryTheory.Functor Cᵒᵖ D),
      CategoryTheory.Limits.PreservesLimit (W.index P).multicospan G],
  CategoryTheory.CategoryStruct.comp ((J.plusObj P).whiskerLeft η) (J.plusCompIso G P).hom =
    CategoryTheory.CategoryStruct.comp (J.plusCompIso F P).hom (J.plusMap (P.whiskerLeft η))
-- Mathlib.GroupTheory.GroupAction.Defs
MulAction.stabilizer.eq_1 : ∀ (G : Type u_1) {α : Type u_2} [inst : Group G] [inst_1 : MulAction G α] (a : α),
  MulAction.stabilizer G a = { toSubmonoid := MulAction.stabilizerSubmonoid G a, inv_mem' := ⋯ }
-- Mathlib.AlgebraicTopology.SimplicialSet.StrictSegal
SSet.StrictSegalCore.spine_spineToSimplex : ∀ {X : SSet} (h : (n : ℕ) → X.StrictSegalCore n) {n : ℕ} (p : X.Path n),
  X.spine n (SSet.StrictSegalCore.spineToSimplex h p) = p
-- Mathlib.CategoryTheory.Limits.Shapes.WidePullbacks
/-- Construct a cocone over a wide span.  -/
CategoryTheory.Limits.WidePushoutShape.mkCocone : {J : Type w} →
  {C : Type u} →
    [inst : CategoryTheory.Category.{v, u} C] →
      {F : CategoryTheory.Functor (CategoryTheory.Limits.WidePushoutShape J) C} →
        {X : C} →
          (f : F.obj none ⟶ X) →
            (ι : (j : J) → F.obj (some j) ⟶ X) →
              (∀ (j : J),
                  CategoryTheory.CategoryStruct.comp (F.map (CategoryTheory.Limits.WidePushoutShape.Hom.init j)) (ι j) =
                    f) →
                CategoryTheory.Limits.Cocone F
-- Mathlib.MeasureTheory.MeasurableSpace.CountablyGenerated
MeasurableSpace.measurableSet_generateFrom_memPartition_iff : ∀ {α : Type u_1} (t : ℕ → Set α) (n : ℕ) (s : Set α), MeasurableSet s ↔ ∃ S, ↑S ⊆ memPartition t n ∧ s = ⋃₀ ↑S
-- Mathlib.Order.SuccPred.IntervalSucc
/-- If `α` is a linear pred order, `β` is a preorder, and `f : α → β` is a monotone function, then
the intervals `Set.Ioo (f Order.pred n) (f n)` are pairwise disjoint.  -/
Monotone.pairwise_disjoint_on_Ioo_pred : ∀ {α : Type u_1} {β : Type u_2} [inst : LinearOrder α] [inst_1 : PredOrder α] [inst_2 : Preorder β] {f : α → β},
  Monotone f → Pairwise (Function.onFun Disjoint fun n => Set.Ioo (f (Order.pred n)) (f n))
-- Batteries.Data.MLList.Basic
/-- Take the initial segment of the lazy list, until the function `f` first returns `false`.  -/
MLList.takeWhileM : {m : Type u_1 → Type u_1} → {α : Type u_1} → [Monad m] → (α → m (ULift.{u_1, 0} Bool)) → MLList m α → MLList m α
-- Mathlib.CategoryTheory.Limits.FormalCoproducts.Cech
/-- The functoriality of `FormalCoproduct.power` with respect to the index type.  -/
CategoryTheory.Limits.FormalCoproduct.mapPower : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    (U : CategoryTheory.Limits.FormalCoproduct C) →
      {α β : Type t} →
        [inst_1 : CategoryTheory.Limits.HasProductsOfShape α C] →
          [inst_2 : CategoryTheory.Limits.HasProductsOfShape β C] → (α → β) → (U.power β ⟶ U.power α)
-- Mathlib.CategoryTheory.Presentable.Directed
CategoryTheory.IsCardinalFiltered.exists_cardinal_directed.D₁.congr_simp : ∀ {J : Type w} [inst : CategoryTheory.SmallCategory J] {κ : Cardinal.{w}} [inst_1 : Fact κ.IsRegular] {ι : Type w}
  (D D_1 : ι → CategoryTheory.IsCardinalFiltered.exists_cardinal_directed.DiagramWithUniqueTerminal J κ),
  D = D_1 →
    ∀ (hι : HasCardinalLT ι κ) (m m_1 : J),
      m = m_1 →
        CategoryTheory.IsCardinalFiltered.exists_cardinal_directed.D₁ D hι m =
          CategoryTheory.IsCardinalFiltered.exists_cardinal_directed.D₁ D_1 hι m_1
-- Mathlib.Topology.DiscreteQuotient
/-- The projection from `X` to the given discrete quotient.  -/
DiscreteQuotient.proj : {X : Type u_2} → [inst : TopologicalSpace X] → (S : DiscreteQuotient X) → X → Quotient S.toSetoid
-- Mathlib.LinearAlgebra.Matrix.Defs
/-- This is `Matrix.of` bundled as an additive equivalence.  -/
Matrix.ofAddEquiv : {m : Type u_2} → {n : Type u_3} → {α : Type v} → [inst : Add α] → (m → n → α) ≃+ Matrix m n α
-- Mathlib.CategoryTheory.Category.Factorisation
CategoryTheory.Factorisation.initial_ι : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {X Y : C} {f : X ⟶ Y},
  CategoryTheory.Factorisation.initial.ι = CategoryTheory.CategoryStruct.id X
-- Std.Time.DateTime.PlainDateTime
Std.Time.PlainDateTime.mk : Std.Time.PlainDate → Std.Time.PlainTime → Std.Time.PlainDateTime
-- Mathlib.Analysis.InnerProductSpace.Dual
innerSL_inj : ∀ {𝕜 : Type u_1} [inst : RCLike 𝕜] {E : Type u_3} [inst_1 : NormedAddCommGroup E] [inst_2 : InnerProductSpace 𝕜 E]
  {x y : E}, (innerSL 𝕜) x = (innerSL 𝕜) y ↔ x = y
-- Mathlib.LinearAlgebra.Determinant
Matrix.det_comm : ∀ {A : Type u_5} [inst : CommRing A] {n : Type u_7} [inst_1 : Fintype n] [inst_2 : DecidableEq n] (M N : Matrix n n A),
  (M * N).det = (N * M).det
-- Mathlib.Algebra.Homology.Homotopy
/-- Compatibility of `nullHomotopicMap'` with the precomposition by a morphism
of complexes.  -/
Homotopy.comp_nullHomotopicMap' : ∀ {ι : Type u_1} {V : Type u} [inst : CategoryTheory.Category.{v, u} V] [inst_1 : CategoryTheory.Preadditive V]
  {c : ComplexShape ι} {C D E : HomologicalComplex V c} (f : C ⟶ D) (hom : (i j : ι) → c.Rel j i → (D.X i ⟶ E.X j)),
  CategoryTheory.CategoryStruct.comp f (Homotopy.nullHomotopicMap' hom) =
    Homotopy.nullHomotopicMap' fun i j hij => CategoryTheory.CategoryStruct.comp (f.f i) (hom i j hij)
-- Mathlib.Topology.ContinuousMap.Bounded.Normed
BoundedContinuousFunction.norm_eq_iSup_norm : ∀ {α : Type u} {β : Type v} [inst : TopologicalSpace α] [inst_1 : SeminormedAddCommGroup β]
  (f : BoundedContinuousFunction α β), ‖f‖ = ⨆ x, ‖f x‖
-- Lean.DocString.Parser
/-- Recovers from an error by pushing the provided syntax items, without adjusting the position.  -/
_private.Lean.DocString.Parser.0.Lean.Doc.Parser.recoverHereWith : Array Lean.Syntax → Lean.Parser.ParserFn → Lean.Parser.ParserFn
-- Mathlib.Algebra.Lie.Abelian
LieModule.isFaithful_iff_ker_eq_bot : ∀ (R : Type u) (L : Type v) (M : Type w) [inst : CommRing R] [inst_1 : LieRing L] [inst_2 : LieAlgebra R L]
  [inst_3 : AddCommGroup M] [inst_4 : Module R M] [inst_5 : LieRingModule L M] [inst_6 : LieModule R L M],
  LieModule.IsFaithful R L M ↔ LieModule.ker R L M = ⊥
-- Mathlib.Analysis.RCLike.ContinuousMap
/-- `ContinuousMap.realToRCLike` as an order embedding.  -/
ContinuousMap.realToRCLikeOrderEmbedding : (X : Type u_1) → (𝕜 : Type u_2) → [inst : TopologicalSpace X] → [inst_1 : RCLike 𝕜] → C(X, ℝ) ↪o C(X, 𝕜)
-- Mathlib.GroupTheory.FreeGroup.Reduce
FreeGroup.norm_eq_zero : ∀ {α : Type u_1} [inst : DecidableEq α] {x : FreeGroup α}, x.norm = 0 ↔ x = 1
-- Mathlib.GroupTheory.SpecificGroups.Cyclic
ZMod.instIsSimpleAddGroup : ∀ {p : ℕ} [hp : Fact (Nat.Prime p)], IsSimpleAddGroup (ZMod p)
-- Mathlib.RingTheory.Localization.FractionRing
IsFractionRing.fieldEquivOfAlgEquiv_refl : ∀ (A : Type u_8) (B : Type u_9) [inst : CommRing A] [inst_1 : CommRing B] [inst_2 : Algebra A B] (FA : Type u_12)
  (FB : Type u_13) [inst_3 : Field FA] [inst_4 : Field FB] [inst_5 : Algebra A FA] [inst_6 : Algebra B FB]
  [inst_7 : IsFractionRing A FA] [inst_8 : IsFractionRing B FB] [inst_9 : Algebra A FB] [inst_10 : IsScalarTower A B FB]
  [inst_11 : Algebra FA FB] [inst_12 : IsScalarTower A FA FB],
  IsFractionRing.fieldEquivOfAlgEquiv FA FB FB AlgEquiv.refl = AlgEquiv.refl
-- Mathlib.Algebra.Group.Subgroup.Lattice
Subgroup.mem_biSup_of_directedOn : ∀ {G : Type u_1} [inst : Group G] {ι : Type u_2} {p : ι → Prop} {K : ι → Subgroup G} {i : ι},
  p i →
    DirectedOn (Function.onFun (fun x1 x2 => x1 ≤ x2) K) {i | p i} →
      ∀ {x : G}, x ∈ ⨆ i, ⨆ (_ : p i), K i ↔ ∃ i, p i ∧ x ∈ K i
-- Mathlib.CategoryTheory.ComposableArrows.Basic
_private.Mathlib.CategoryTheory.ComposableArrows.Basic.0.CategoryTheory.ComposableArrows.homMk₁.match_1.eq_2 : ∀ (motive : Fin (1 + 1) → Sort u_1) (isLt : 1 < 1 + 1) (h_1 : (isLt : 0 < 1 + 1) → motive ⟨0, isLt⟩)
  (h_2 : (isLt : 1 < 1 + 1) → motive ⟨1, isLt⟩),
  (match ⟨1, isLt⟩ with
    | ⟨0, isLt⟩ => h_1 isLt
    | ⟨1, isLt⟩ => h_2 isLt) =
    h_2 isLt
-- Mathlib.CategoryTheory.EpiMono
CategoryTheory.unop_mono_iff : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {X Y : Cᵒᵖ} (f : Y ⟶ X),
  CategoryTheory.Mono f.unop ↔ CategoryTheory.Epi f
-- Mathlib.Analysis.LConvolution
/-- Multiplicative convolution of functions.  -/
MeasureTheory.mlconvolution : {G : Type u_1} →
  {mG : MeasurableSpace G} → [Mul G] → [Inv G] → (G → ENNReal) → (G → ENNReal) → MeasureTheory.Measure G → G → ENNReal
-- Batteries.Data.Fin.Fold
Fin.dfoldlM_loop : ∀ {m : Type u_1 → Type u_2} {n : ℕ} {α : Fin (n + 1 + 1) → Type u_1} {i : ℕ} [inst : Monad m]
  (f : (i : Fin (n + 1)) → α i.castSucc → m (α i.succ)) (h : i < n + 1) (x : α ⟨i, ⋯⟩),
  Fin.dfoldlM.loop (n + 1) α f i ⋯ x = do
    let x ← f ⟨i, h⟩ x
    Fin.dfoldlM.loop n (α ∘ Fin.succ) (fun x1 x2 => f x1.succ x2) i h x
-- Mathlib.Order.Interval.Set.ProjIcc
Set.IccExtend_of_le_left : ∀ {α : Type u_1} {β : Type u_2} [inst : LinearOrder α] {a b : α} (h : a ≤ b) {x : α} (f : ↑(Set.Icc a b) → β),
  x ≤ a → Set.IccExtend h f x = f ⟨a, ⋯⟩
-- Std.Data.ExtHashMap.Lemmas
Std.ExtHashMap.getThenInsertIfNew?.congr_simp : ∀ {α : Type u} {β : Type v} {x : BEq α} {x_1 : Hashable α} [inst : EquivBEq α] [inst_1 : LawfulHashable α]
  (m m_1 : Std.ExtHashMap α β),
  m = m_1 →
    ∀ (a a_1 : α), a = a_1 → ∀ (b b_1 : β), b = b_1 → m.getThenInsertIfNew? a b = m_1.getThenInsertIfNew? a_1 b_1
-- Mathlib.Order.WithBot
WithTop.toDual_top : ∀ {α : Type u_1}, WithTop.toDual ⊤ = ⊥
-- Mathlib.CategoryTheory.Monoidal.Cartesian.Basic
CategoryTheory.CartesianMonoidalCategory.tensorμ_fst_assoc : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.CartesianMonoidalCategory C]
  [inst_2 : CategoryTheory.BraidedCategory C] (W X Y Z : C) {Z_1 : C}
  (h : CategoryTheory.MonoidalCategoryStruct.tensorObj W Y ⟶ Z_1),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.tensorμ W X Y Z)
      (CategoryTheory.CategoryStruct.comp
        (CategoryTheory.SemiCartesianMonoidalCategory.fst (CategoryTheory.MonoidalCategoryStruct.tensorObj W Y)
          (CategoryTheory.MonoidalCategoryStruct.tensorObj X Z))
        h) =
    CategoryTheory.CategoryStruct.comp
      (CategoryTheory.MonoidalCategoryStruct.tensorHom (CategoryTheory.SemiCartesianMonoidalCategory.fst W X)
        (CategoryTheory.SemiCartesianMonoidalCategory.fst Y Z))
      h
-- Mathlib.Analysis.Meromorphic.Basic
/-- Finite sums of meromorphic functions are meromorphic.  -/
MeromorphicOn.sum : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_3} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {U : Set 𝕜} {ι : Type u_5} {s : Finset ι} {f : ι → 𝕜 → E},
  (∀ σ ∈ s, MeromorphicOn (f σ) U) → MeromorphicOn (∑ n ∈ s, f n) U
-- Mathlib.Topology.Sheaves.SheafCondition.OpensLeCover
TopCat.Presheaf.whiskerIsoMapGenerateCocone_inv_hom : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] {X : TopCat} (F : TopCat.Presheaf C X) {ι : Type u_2}
  (U : ι → TopologicalSpace.Opens ↑X) {Y : TopologicalSpace.Opens ↑X} (hY : Y = iSup U),
  (F.whiskerIsoMapGenerateCocone U hY).inv.hom = F.map (CategoryTheory.eqToHom ⋯)
-- Mathlib.Algebra.Order.GroupWithZero.Synonym
OrderDual.instGroupWithZero : {α : Type u_1} → [GroupWithZero α] → GroupWithZero αᵒᵈ
-- Lean.Server.Completion.CompletionCollectors
/-- Adds a new completion item to the state in `M`.  -/
_private.Lean.Server.Completion.CompletionCollectors.0.Lean.Server.Completion.addItem : Lean.Lsp.CompletionItem → optParam (Option Lean.Lsp.CompletionIdentifier) none → Lean.Server.Completion.M✝ Unit
-- Std.Data.DTreeMap.Internal.Lemmas
Std.DTreeMap.Internal.Impl.maxKey?_le : ∀ {α : Type u} {β : α → Type v} {instOrd : Ord α} {t : Std.DTreeMap.Internal.Impl α β} [Std.TransOrd α] {k : α},
  t.WF → ((∀ (k' : α), t.maxKey? = some k' → (compare k' k).isLE = true) ↔ ∀ k' ∈ t, (compare k' k).isLE = true)
-- Mathlib.Data.ENNReal.Operations
ENNReal.iInf₂_add : ∀ {ι : Sort u_1} {a : ENNReal} {κ : ι → Sort u_2} (f : (i : ι) → κ i → ENNReal),
  (⨅ i, ⨅ j, f i j) + a = ⨅ i, ⨅ j, f i j + a
-- Mathlib.Analysis.Convex.Cone.Extension
/-- **Hahn-Banach theorem**: if `N : E → ℝ` is a sublinear map, `f` is a linear map
defined on a subspace of `E`, and `f x ≤ N x` for all `x` in the domain of `f`,
then `f` can be extended to the whole space to a linear map `g` such that `g x ≤ N x`
for all `x`.  -/
exists_extension_of_le_sublinear : ∀ {E : Type u_2} [inst : AddCommGroup E] [inst_1 : Module ℝ E] (f : E →ₗ.[ℝ] ℝ) (N : E → ℝ),
  (∀ (c : ℝ), 0 < c → ∀ (x : E), N (c • x) = c * N x) →
    (∀ (x y : E), N (x + y) ≤ N x + N y) →
      (∀ (x : ↥f.domain), ↑f x ≤ N ↑x) → ∃ g, (∀ (x : ↥f.domain), g ↑x = ↑f x) ∧ ∀ (x : E), g x ≤ N x
-- Mathlib.Algebra.Group.Fin.Basic
Fin.neg_last : ∀ (n : ℕ), -Fin.last n = 1
-- Mathlib.Data.Set.Function
Set.RightInvOn.comp : ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} {t : Set β} {p : Set γ} {f : α → β} {g : β → γ} {f' : β → α}
  {g' : γ → β}, Set.RightInvOn f' f t → Set.RightInvOn g' g p → Set.MapsTo g' p t → Set.RightInvOn (f' ∘ g') (g ∘ f) p
-- Mathlib.Tactic.Linarith.Oracle.SimplexAlgorithm.Datatypes
Mathlib.Tactic.Linarith.SimplexAlgorithm.DenseMatrix.mk.inj : ∀ {n m : ℕ} {data data_1 : Array (Array ℚ)}, { data := data } = { data := data_1 } → data = data_1
-- Mathlib.Algebra.Module.LocalizedModule.Int
/-- Each element `x : M'` has an `S`-multiple which is an integer.  -/
IsLocalizedModule.exists_integer_multiple : ∀ {R : Type u_1} [inst : CommSemiring R] (S : Submonoid R) {M : Type u_2} [inst_1 : AddCommMonoid M]
  [inst_2 : Module R M] {M' : Type u_3} [inst_3 : AddCommMonoid M'] [inst_4 : Module R M'] (f : M →ₗ[R] M')
  [IsLocalizedModule S f] (x : M'), ∃ a, IsLocalizedModule.IsInteger f (↑a • x)
-- Mathlib.Algebra.Group.Action.Pointwise.Set.Basic
Set.mem_neg_vadd_set_iff : ∀ {α : Type u_2} {β : Type u_3} [inst : AddGroup α] [inst_1 : AddAction α β] {A : Set β} {a : α} {x : β},
  x ∈ -a +ᵥ A ↔ a +ᵥ x ∈ A
-- Init.Data.BitVec.Lemmas
BitVec.toFin_sshiftRight'_of_msb_true : ∀ {w : ℕ} {x y : BitVec w},
  x.msb = true → (x.sshiftRight' y).toFin = Fin.ofNat (2 ^ w) (2 ^ w - 1 - (2 ^ w - 1 - x.toNat) >>> y.toNat)
-- Mathlib.CategoryTheory.Limits.Shapes.Biproducts
CategoryTheory.Limits.biproduct.toSubtype_fromSubtype : ∀ {J : Type w} {C : Type u} [inst : CategoryTheory.Category.{v, u} C]
  [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C] (f : J → C) [inst_2 : CategoryTheory.Limits.HasBiproduct f]
  (p : J → Prop) [inst_3 : CategoryTheory.Limits.HasBiproduct (Subtype.restrict p f)] [inst_4 : DecidablePred p],
  CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.biproduct.toSubtype f p)
      (CategoryTheory.Limits.biproduct.fromSubtype f p) =
    CategoryTheory.Limits.biproduct.map fun j => if p j then CategoryTheory.CategoryStruct.id (f j) else 0
-- Init.Data.List.Sort.Impl
_private.Init.Data.List.Sort.Impl.0.List.mergeSort.match_1.splitter : {α : Type u_1} →
  (motive : List α → (α → α → Bool) → Sort u_2) →
    (x : List α) →
      (x_1 : α → α → Bool) →
        ((x : α → α → Bool) → motive [] x) →
          ((a : α) → (x : α → α → Bool) → motive [a] x) →
            ((a b : α) → (xs : List α) → (le : α → α → Bool) → motive (a :: b :: xs) le) → motive x x_1
-- Mathlib.Data.Set.Card
Set.surj_on_of_inj_on_of_ncard_le : ∀ {α : Type u_1} {β : Type u_2} {s : Set α} {t : Set β} (f : (a : α) → a ∈ s → β),
  (∀ (a : α) (ha : a ∈ s), f a ha ∈ t) →
    (∀ (a₁ a₂ : α) (ha₁ : a₁ ∈ s) (ha₂ : a₂ ∈ s), f a₁ ha₁ = f a₂ ha₂ → a₁ = a₂) →
      t.ncard ≤ s.ncard →
        autoParam t.Finite Set.surj_on_of_inj_on_of_ncard_le._auto_1 → ∀ b ∈ t, ∃ a, ∃ (ha : a ∈ s), b = f a ha
-- Mathlib.LinearAlgebra.Orientation
/-- If the index type has cardinality equal to the finite dimension, composing an alternating
map with the same linear equiv on each argument gives the same orientation if and only if the
determinant is positive.  -/
Orientation.map_eq_iff_det_pos : ∀ {R : Type u_1} [inst : Field R] [inst_1 : LinearOrder R] [inst_2 : IsStrictOrderedRing R] {M : Type u_2}
  [inst_3 : AddCommGroup M] [inst_4 : Module R M] {ι : Type u_3} [inst_5 : Fintype ι] [FiniteDimensional R M]
  (x : Orientation R M ι) (f : M ≃ₗ[R] M),
  Fintype.card ι = Module.finrank R M → ((Orientation.map ι f) x = x ↔ 0 < LinearMap.det ↑f)
-- Std.Data.ExtHashSet.Basic
Std.ExtHashSet.mk.sizeOf_spec : ∀ {α : Type u} [inst : BEq α] [inst_1 : Hashable α] [inst_2 : SizeOf α] (inner : Std.ExtHashMap α Unit),
  sizeOf { inner := inner } = 1 + sizeOf inner
-- Mathlib.GroupTheory.Frattini
Order.radical.eq_1 : ∀ (α : Type u_1) [inst : Preorder α] [inst_1 : OrderTop α] [inst_2 : InfSet α],
  Order.radical α = ⨅ a ∈ {H | IsCoatom H}, a
-- Mathlib.Algebra.Star.StarAlgHom
NonUnitalStarAlgHom.coe_restrictScalars' : ∀ (R : Type u_1) {S : Type u_2} {A : Type u_3} {B : Type u_4} [inst : Monoid R] [inst_1 : Monoid S] [inst_2 : Star A]
  [inst_3 : Star B] [inst_4 : NonUnitalNonAssocSemiring A] [inst_5 : NonUnitalNonAssocSemiring B]
  [inst_6 : MulAction R S] [inst_7 : DistribMulAction S A] [inst_8 : DistribMulAction S B]
  [inst_9 : DistribMulAction R A] [inst_10 : DistribMulAction R B] [inst_11 : IsScalarTower R S A]
  [inst_12 : IsScalarTower R S B] (f : A →⋆ₙₐ[S] B), ⇑(NonUnitalStarAlgHom.restrictScalars R f) = ⇑f
-- Mathlib.LinearAlgebra.SesquilinearForm.Basic
LinearMap.IsSymm.domRestrict : ∀ {R : Type u_1} {M : Type u_5} [inst : CommSemiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M] {I : R →+* R}
  {B : M →ₛₗ[I] M →ₗ[R] R}, B.IsSymm → ∀ (p : Submodule R M), (B.domRestrict₁₂ p p).IsSymm
-- Mathlib.CategoryTheory.Limits.Shapes.Kernels
/-- If `c` is a limit kernel fork for `g : X ⟶ Y`, and `g' : X ⟶ Y'` is another morphism,
then there is a limit kernel fork for `g'` with the same point as `c` if for any
morphism `φ : W ⟶ X`, there is an equivalence `φ ≫ g = 0 ↔ φ ≫ g' = 0`.  -/
CategoryTheory.Limits.KernelFork.isLimitOfIsLimitOfIff' : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C] →
      {X Y : C} →
        {g : X ⟶ Y} →
          {c : CategoryTheory.Limits.KernelFork g} →
            CategoryTheory.Limits.IsLimit c →
              {Y' : C} →
                (g' : X ⟶ Y') →
                  (iff :
                      ∀ ⦃W : C⦄ (φ : W ⟶ X),
                        CategoryTheory.CategoryStruct.comp φ g = 0 ↔ CategoryTheory.CategoryStruct.comp φ g' = 0) →
                    CategoryTheory.Limits.IsLimit
                      (CategoryTheory.Limits.KernelFork.ofι (CategoryTheory.Limits.Fork.ι c) ⋯)
-- Mathlib.Combinatorics.SimpleGraph.Clique
SimpleGraph.CliqueFree.cliqueFreeOn : ∀ {α : Type u_1} (G : SimpleGraph α) {s : Set α} {n : ℕ}, G.CliqueFree n → G.CliqueFreeOn s n
-- Mathlib.RingTheory.MvPolynomial.MonomialOrder
/-- Multiplicativity of leading coefficients  -/
MonomialOrder.coeff_mul_of_add_of_degree_le : ∀ {σ : Type u_1} {m : MonomialOrder σ} {R : Type u_2} [inst : CommSemiring R] {f g : MvPolynomial σ R} {a b : σ →₀ ℕ},
  m.toSyn (m.degree f) ≤ m.toSyn a →
    m.toSyn (m.degree g) ≤ m.toSyn b →
      MvPolynomial.coeff (a + b) (f * g) = MvPolynomial.coeff a f * MvPolynomial.coeff b g
-- Mathlib.Topology.Algebra.Group.GroupTopology
AddGroupTopology.instTop : {α : Type u} → [inst : AddGroup α] → Top (AddGroupTopology α)
-- Mathlib.RingTheory.Ideal.Prime
Ideal.IsPrime.mul_mem_right_iff : ∀ {α : Type u} [inst : Semiring α] {I : Ideal α} [I.IsTwoSided] [I.IsPrime] {x y : α}, y ∉ I → (x * y ∈ I ↔ x ∈ I)
-- Std.Do.PostCond
Std.Do.ExceptConds.true_imp : ∀ {ps : Std.Do.PostShape} {x : Std.Do.ExceptConds ps}, (Std.Do.ExceptConds.true →ₑ x) = x
-- ProofWidgets.Component.RefreshComponent
ProofWidgets.RefreshComponent.Props.mk.inj : ∀ {state : Lean.Server.WithRpcRef ProofWidgets.RefreshComponent.RefreshRef}
  {cancelTk : Lean.Server.WithRpcRef IO.CancelToken}
  {state_1 : Lean.Server.WithRpcRef ProofWidgets.RefreshComponent.RefreshRef}
  {cancelTk_1 : Lean.Server.WithRpcRef IO.CancelToken},
  { state := state, cancelTk := cancelTk } = { state := state_1, cancelTk := cancelTk_1 } →
    state = state_1 ∧ cancelTk = cancelTk_1
-- Mathlib.RingTheory.PicardGroup
CommRing.Pic.mk_tensor : ∀ {R : Type u} {M : Type v} {N : Type u_1} [inst : CommSemiring R] [inst_1 : AddCommMonoid M] [inst_2 : AddCommMonoid N]
  [inst_3 : Module R M] [inst_4 : Module R N] [inst_5 : Module.Invertible R M] [inst_6 : Module.Invertible R N],
  CommRing.Pic.mk R (TensorProduct R M N) = CommRing.Pic.mk R M * CommRing.Pic.mk R N
-- Mathlib.CategoryTheory.Limits.Shapes.Pullback.IsPullback.Defs
CategoryTheory.IsPullback.isoIsPullback_inv_fst_assoc : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {P : C} (X Y : C) {Z : C} {fst : P ⟶ X} {snd : P ⟶ Y}
  {f : X ⟶ Z} {g : Y ⟶ Z} {P' : C} {fst' : P' ⟶ X} {snd' : P' ⟶ Y} (h : CategoryTheory.IsPullback fst snd f g)
  (h' : CategoryTheory.IsPullback fst' snd' f g) {Z_1 : C} (h_1 : X ⟶ Z_1),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.IsPullback.isoIsPullback X Y h h').inv
      (CategoryTheory.CategoryStruct.comp fst h_1) =
    CategoryTheory.CategoryStruct.comp fst' h_1
-- Init.System.Promise
_private.Init.System.Promise.0.IO.Promise.mk.injEq : ∀ {α : Type} (prom : IO.PromisePointed✝.type) (h : Nonempty α) (prom_1 : IO.PromisePointed✝.type) (h_1 : Nonempty α),
  ({ prom := prom, h := h } = { prom := prom_1, h := h_1 }) = (prom = prom_1)
-- Lean.Language.Basic
Lean.Language.instToSnapshotTreeOption : {α : Type} → [Lean.Language.ToSnapshotTree α] → Lean.Language.ToSnapshotTree (Option α)
-- Mathlib.ModelTheory.Semantics
FirstOrder.Language.BoundedFormula.Realize.eq_3 : ∀ {L : FirstOrder.Language} {M : Type w} [inst : L.Structure M] {α : Type u'} (x : ℕ) (x_1 : α → M) (x_2 : Fin x → M)
  (l : ℕ) (R : L.Relations l) (ts : Fin l → L.Term (α ⊕ Fin x)),
  (FirstOrder.Language.BoundedFormula.rel R ts).Realize x_1 x_2 =
    FirstOrder.Language.Structure.RelMap R fun i => FirstOrder.Language.Term.realize (Sum.elim x_1 x_2) (ts i)
-- Mathlib.CategoryTheory.Sites.NonabelianCohomology.H1
CategoryTheory.PresheafOfGroups.OneCocycle.instOne : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    (G : CategoryTheory.Functor Cᵒᵖ GrpCat) →
      {I : Type w'} → (U : I → C) → One (CategoryTheory.PresheafOfGroups.OneCocycle G U)
-- Mathlib.Tactic.CategoryTheory.BicategoricalComp
CategoryTheory.BicategoricalCoherence.tensorRight : {B : Type u} →
  [inst : CategoryTheory.Bicategory B] →
    {a b : B} →
      (f : a ⟶ b) →
        (g : b ⟶ b) →
          [CategoryTheory.BicategoricalCoherence (CategoryTheory.CategoryStruct.id b) g] →
            CategoryTheory.BicategoricalCoherence f (CategoryTheory.CategoryStruct.comp f g)