mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.CategoryTheory.SmallObject.Construction
CategoryTheory.SmallObject.functorMapSrc.eq_1 : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {I : Type w} {A B : I → C} (f : (i : I) → A i ⟶ B i)
  {S T X Y : C} {πX : X ⟶ S} {πY : Y ⟶ T} (τ : CategoryTheory.Arrow.mk πX ⟶ CategoryTheory.Arrow.mk πY)
  [inst_1 :
    CategoryTheory.Limits.HasColimitsOfShape (CategoryTheory.Discrete (CategoryTheory.SmallObject.FunctorObjIndex f πX))
      C]
  [inst_2 :
    CategoryTheory.Limits.HasColimitsOfShape (CategoryTheory.Discrete (CategoryTheory.SmallObject.FunctorObjIndex f πY))
      C],
  CategoryTheory.SmallObject.functorMapSrc f τ =
    CategoryTheory.Limits.Sigma.map'
      (fun x =>
        { i := x.i, t := CategoryTheory.CategoryStruct.comp x.t (CategoryTheory.Arrow.Hom.left τ),
          b := CategoryTheory.CategoryStruct.comp x.b (CategoryTheory.Arrow.Hom.right τ), w := ⋯ })
      fun x => CategoryTheory.CategoryStruct.id (CategoryTheory.SmallObject.functorObjSrcFamily f πX x)
-- Std.Data.DTreeMap.Internal.Model
Std.DTreeMap.Internal.Impl.updateCell.eq_1 : ∀ {α : Type u} {β : α → Type v} [inst : Ord α] (k : α)
  (f : Std.DTreeMap.Internal.Cell α β (compare k) → Std.DTreeMap.Internal.Cell α β (compare k))
  (hl_2 : Std.DTreeMap.Internal.Impl.leaf.Balanced),
  Std.DTreeMap.Internal.Impl.updateCell k f Std.DTreeMap.Internal.Impl.leaf hl_2 =
    match (f Std.DTreeMap.Internal.Cell.empty).inner with
    | none =>
      { impl := Std.DTreeMap.Internal.Impl.leaf, balanced_impl := ⋯, lb_le_size_impl := ⋯, size_impl_le_ub := ⋯ }
    | some ⟨k', v'⟩ =>
      {
        impl :=
          Std.DTreeMap.Internal.Impl.inner 1 k' v' Std.DTreeMap.Internal.Impl.leaf Std.DTreeMap.Internal.Impl.leaf,
        balanced_impl := ⋯, lb_le_size_impl := ⋯, size_impl_le_ub := ⋯ }
-- Init.Data.String.Lemmas.FindPos
String.Pos.prev?_eq_dif : ∀ {s : String} {p : s.Pos}, p.prev? = if h : p = s.startPos then none else some (p.prev h)
-- Mathlib.Order.Interval.Set.Fin
Fin.preimage_castAdd_Ioc_castAdd : ∀ {n : ℕ} (m : ℕ) (i j : Fin n), Fin.castAdd m ⁻¹' Set.Ioc (Fin.castAdd m i) (Fin.castAdd m j) = Set.Ioc i j
-- Mathlib.CategoryTheory.Adjunction.Opposites
CategoryTheory.Adjunction.leftOp_eq : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  {F : CategoryTheory.Functor C Dᵒᵖ} {G : CategoryTheory.Functor D Cᵒᵖ} (a : F ⊣ G.leftOp),
  a.leftOp = (CategoryTheory.opOpEquivalence D).symm.toAdjunction.comp a.op
-- Mathlib.LinearAlgebra.ExteriorAlgebra.Basic
ExteriorAlgebra.ιInv_comp_map : ∀ {R : Type u1} [inst : CommRing R] {M : Type u2} [inst_1 : AddCommGroup M] [inst_2 : Module R M] {N : Type u4}
  [inst_3 : AddCommGroup N] [inst_4 : Module R N] (f : M →ₗ[R] N),
  ExteriorAlgebra.ιInv ∘ₗ (ExteriorAlgebra.map f).toLinearMap = f ∘ₗ ExteriorAlgebra.ιInv
-- Mathlib.Algebra.Order.Module.PositiveLinearMap
PositiveLinearMap.mk.injEq : ∀ {R : Type u_1} {E₁ : Type u_2} {E₂ : Type u_3} [inst : Semiring R] [inst_1 : AddCommMonoid E₁]
  [inst_2 : PartialOrder E₁] [inst_3 : AddCommMonoid E₂] [inst_4 : PartialOrder E₂] [inst_5 : Module R E₁]
  [inst_6 : Module R E₂] (toLinearMap : E₁ →ₗ[R] E₂) (monotone' : Monotone toLinearMap.toFun)
  (toLinearMap_1 : E₁ →ₗ[R] E₂) (monotone'_1 : Monotone toLinearMap_1.toFun),
  ({ toLinearMap := toLinearMap, monotone' := monotone' } =
      { toLinearMap := toLinearMap_1, monotone' := monotone'_1 }) =
    (toLinearMap = toLinearMap_1)
-- Mathlib.RingTheory.WittVector.Truncated
TruncatedWittVector.out_injective : ∀ {p n : ℕ} {R : Type u_1} [inst : CommRing R], Function.Injective TruncatedWittVector.out
-- Init.Data.String.Basic
/-- Given a position in `s.slice p₀ p₁ h`, obtain the corresponding position in `s`.  -/
String.Pos.ofSlice : {s : String} → {p₀ p₁ : s.Pos} → {h : p₀ ≤ p₁} → (s.slice p₀ p₁ h).Pos → s.Pos
-- Mathlib.Combinatorics.Matroid.Loop
/-- **Alias** of `Matroid.closure_sdiff_loops_eq`. -/
Matroid.closure_diff_loops_eq : ∀ {α : Type u_1} (M : Matroid α) (X : Set α), M.closure (X \ M.loops) = M.closure X
-- Mathlib.RingTheory.KrullDimension.Zero
PrimeSpectrum.subsingleton_iff_isField_of_isReduced : ∀ {R : Type u_2} [inst : CommRing R] [IsReduced R] [Nontrivial R], Subsingleton (PrimeSpectrum R) ↔ IsField R
-- Init.Data.Vector.Range
Vector.range'_append_1 : ∀ {s m n : ℕ}, Vector.range' s m ++ Vector.range' (s + m) n = Vector.range' s (m + n)
-- Mathlib.CategoryTheory.Enriched.Limits.HasConicalLimits
CategoryTheory.Enriched.HasConicalLimitsOfSize.mk : ∀ {V : outParam (Type u')} [inst : CategoryTheory.Category.{v', u'} V] [inst_1 : CategoryTheory.MonoidalCategory V]
  {C : Type u} [inst_2 : CategoryTheory.Category.{v, u} C] [inst_3 : CategoryTheory.EnrichedOrdinaryCategory V C],
  autoParam
      (∀ (J : Type u₁) [inst_4 : CategoryTheory.Category.{v₁, u₁} J],
        CategoryTheory.Enriched.HasConicalLimitsOfShape J V C)
      CategoryTheory.Enriched.HasConicalLimitsOfSize.hasConicalLimitsOfShape._autoParam →
    CategoryTheory.Enriched.HasConicalLimitsOfSize.{v₁, u₁, v', v, u, u'} V C
-- Mathlib.Algebra.Group.Embedding
addLeftEmbedding.eq_1 : ∀ {G : Type u_1} [inst : Add G] [inst_1 : IsLeftCancelAdd G] (g : G),
  addLeftEmbedding g = { toFun := fun h => g + h, inj' := ⋯ }
-- Mathlib.CategoryTheory.Limits.Shapes.BinaryProducts
CategoryTheory.Limits.coprod.mapIso_inv : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {W X Y Z : C}
  [inst_1 : CategoryTheory.Limits.HasBinaryCoproduct W X] [inst_2 : CategoryTheory.Limits.HasBinaryCoproduct Y Z]
  (f : W ≅ Y) (g : X ≅ Z), (CategoryTheory.Limits.coprod.mapIso f g).inv = CategoryTheory.Limits.coprod.map f.inv g.inv
-- Mathlib.Data.Multiset.Pi
Multiset.Pi.cons_swap : ∀ {α : Type u_1} [inst : DecidableEq α] {δ : α → Sort u_2} {a a' : α} {b : δ a} {b' : δ a'} {m : Multiset α}
  {f : (a : α) → a ∈ m → δ a},
  a ≠ a' →
    Multiset.Pi.cons (a' ::ₘ m) a b (Multiset.Pi.cons m a' b' f) ≍
      Multiset.Pi.cons (a ::ₘ m) a' b' (Multiset.Pi.cons m a b f)
-- Mathlib.Topology.Order
nhds_discrete : ∀ (α : Type u_3) [inst : TopologicalSpace α] [DiscreteTopology α], nhds = pure
-- Mathlib.Data.Finset.SDiff
Finset.union_sdiff_distrib : ∀ {α : Type u_1} [inst : DecidableEq α] (s₁ s₂ t : Finset α), (s₁ ∪ s₂) \ t = s₁ \ t ∪ s₂ \ t
-- Mathlib.Topology.Connected.Basic
PreconnectedSpace.connectedComponent_eq_univ : ∀ {X : Type u_3} [inst : TopologicalSpace X] [h : PreconnectedSpace X] (x : X), connectedComponent x = Set.univ
-- Mathlib.Analysis.Matrix.Normed
Matrix.frobenius_nnnorm_diagonal : ∀ {n : Type u_4} {α : Type u_5} [inst : Fintype n] [inst_1 : SeminormedAddCommGroup α] [inst_2 : DecidableEq n]
  (v : n → α), ‖Matrix.diagonal v‖₊ = ‖WithLp.toLp 2 v‖₊
-- Mathlib.SetTheory.Cardinal.Aleph
Cardinal.preBeth_lt_preBeth : ∀ {o₁ o₂ : Ordinal.{u_1}}, Cardinal.preBeth o₁ < Cardinal.preBeth o₂ ↔ o₁ < o₂
-- Mathlib.MeasureTheory.MeasurableSpace.Constructions
measurable_of_measurable_on_compl_singleton : ∀ {α : Type u_1} {β : Type u_2} {m : MeasurableSpace α} {mβ : MeasurableSpace β} [MeasurableSingletonClass α]
  {f : α → β} (a : α), Measurable ({x | x ≠ a}.domRestrict f) → Measurable f
-- Mathlib.Algebra.Category.ModuleCat.Sheaf.Generators
SheafOfModules.GeneratingSections.map_s : ∀ {C : Type u'} [inst : CategoryTheory.Category.{v', u'} C] {J : CategoryTheory.GrothendieckTopology C}
  {R : CategoryTheory.Sheaf J RingCat} [inst_1 : CategoryTheory.HasWeakSheafify J AddCommGrpCat]
  [inst_2 : J.WEqualsLocallyBijective AddCommGrpCat] {C' : Type u₁} [inst_3 : CategoryTheory.Category.{v₁, u₁} C']
  {J' : CategoryTheory.GrothendieckTopology C'} {S : CategoryTheory.Sheaf J' RingCat}
  [inst_4 : CategoryTheory.HasSheafify J' AddCommGrpCat] [inst_5 : J'.WEqualsLocallyBijective AddCommGrpCat]
  {M : SheafOfModules R} (G : M.GeneratingSections) (F : CategoryTheory.Functor (SheafOfModules R) (SheafOfModules S))
  [inst_6 :
    CategoryTheory.Limits.PreservesColimitsOfSize.{u, u, max u u', max u u₁, max (max (u + 1) u') v',
        max (max (u + 1) u₁) v₁}
      F]
  (η : SheafOfModules.unit S ≅ F.obj (SheafOfModules.unit R)) (a : G.I),
  (G.map F η).s a = (F.obj M).freeHomEquiv (G.mapFreeHom F η) a
-- Init.Data.Bool
Bool.eq_false_imp_eq_true_iff : ∀ (a b : Bool), (a = false → b = true ↔ b = false → a = true) = True
-- Mathlib.Algebra.Order.BigOperators.Group.Finset
Finset.sum_pos' : ∀ {ι : Type u_1} {M : Type u_4} [inst : AddCommMonoid M] [inst_1 : Preorder M] [IsOrderedCancelAddMonoid M] {f : ι → M}
  {s : Finset ι} [AddLeftStrictMono M], (∀ i ∈ s, 0 ≤ f i) → (∃ i ∈ s, 0 < f i) → 0 < ∑ i ∈ s, f i
-- Mathlib.GroupTheory.GroupAction.SubMulAction
SetLike.val_vadd : ∀ {S : Type u'} {R : Type u} {M : Type v} [inst : VAdd R M] [inst_1 : SetLike S M] [hS : VAddMemClass S R M] (s : S)
  (r : R) (x : ↥s), ↑(r +ᵥ x) = r +ᵥ ↑x
-- Mathlib.SetTheory.Cardinal.Aleph
/-- The "pre-beth" function is defined so that `preBeth o` is the supremum of `2 ^ preBeth a` for
`a < o`. This implies `beth 0 = 0`, `beth (succ o) = 2 ^ beth o`, and that for a limit ordinal `o`,
`beth o` is the supremum of `beth a` for `a < o`.

For the usual function starting at `ℵ₀`, see `Cardinal.beth`.  -/
Cardinal.preBeth : Ordinal.{u} → Cardinal.{u}
-- Mathlib.Topology.ContinuousOn
continuousOn_empty : ∀ {α : Type u_1} {β : Type u_2} [inst : TopologicalSpace α] [inst_1 : TopologicalSpace β] (f : α → β), ContinuousOn f ∅
-- Mathlib.Algebra.Star.Unitary
Unitary.map_coe : ∀ {R : Type u_2} {S : Type u_3} [inst : Monoid R] [inst_1 : StarMul R] [inst_2 : Monoid S] [inst_3 : StarMul S]
  (f : R →⋆* S) (a : ↥(unitary R)), (Unitary.map f) a = Subtype.map ⇑f ⋯ a
-- Mathlib.Topology.Algebra.InfiniteSum.Order
isLUB_hasProd' : ∀ {ι : Type u_1} {α : Type u_3} [inst : CommMonoid α] [inst_1 : PartialOrder α] [CanonicallyOrderedMul α]
  [inst_3 : TopologicalSpace α] [OrderClosedTopology α] {f : ι → α} {a : α},
  HasProd f a → IsLUB (Set.range fun s => ∏ i ∈ s, f i) a
-- Mathlib.Data.Finset.Filter
/-- If all elements of a `Finset` fail to satisfy the predicate `p`, `s.filter p` is `∅`.  -/
Finset.filter_false_of_mem : ∀ {α : Type u_1} {p : α → Prop} [inst : DecidablePred p] {s : Finset α}, (∀ x ∈ s, ¬p x) → Finset.filter p s = ∅
-- Mathlib.RingTheory.Localization.AtPrime.Basic
IsLocalization.liftAlgHom.congr_simp : ∀ {A : Type u_4} [inst : CommSemiring A] {R : Type u_5} [inst_1 : CommSemiring R] [inst_2 : Algebra A R]
  {M M_1 : Submonoid R} (e_M : M = M_1) {S : Type u_6} [inst_3 : CommSemiring S] [inst_4 : Algebra A S]
  [inst_5 : Algebra R S] [inst_6 : IsScalarTower A R S] {P : Type u_7} [inst_7 : CommSemiring P] [inst_8 : Algebra A P]
  [inst_9 : IsLocalization M S] {f f_1 : R →ₐ[A] P} (e_f : f = f_1) (hf : ∀ (y : ↥M), IsUnit (f ↑y)),
  IsLocalization.liftAlgHom hf = IsLocalization.liftAlgHom ⋯
-- Mathlib.Topology.Sheaves.Over
TopologicalSpace.Opens.sheafEquivOver_inverse_obj_obj_map : ∀ {X : Type u} [inst : TopologicalSpace X] (U : TopologicalSpace.Opens X) {A : Type u_1}
  [inst_1 : CategoryTheory.Category.{v_1, u_1} A] (X_1 : CategoryTheory.Sheaf (Opens.grothendieckTopology ↥U) A)
  {X_2 Y : (CategoryTheory.Over U)ᵒᵖ} (f : X_2 ⟶ Y),
  (U.sheafEquivOver.inverse.obj X_1).obj.map f = X_1.obj.map (U.overEquivalence.functor.map f.unop).op
-- Lean.Elab.PreDefinition.WF.GuessLex
_private.Lean.Elab.PreDefinition.WF.GuessLex.0.Lean.Elab.WF.GuessLex.withRecApps.processApp : {α : Type} →
  (recFnName : Lean.Name) →
    ℕ → (Lean.Expr → Array Lean.Expr → Lean.MetaM α) → Lean.Expr → Lean.Expr → Lean.Elab.WF.GuessLex.M recFnName α Unit
-- Init.Data.String.Bootstrap
String.Internal.trim : String → String
-- Mathlib.CategoryTheory.GradedObject.Unitor
CategoryTheory.GradedObject.mapBifunctorRightUnitor_inv_apply : ∀ {C : Type u_1} {D : Type u_2} {I : Type u_3} {J : Type u_4} [inst : CategoryTheory.Category.{v_1, u_1} C]
  [inst_1 : CategoryTheory.Category.{v_2, u_2} D] [inst_2 : Zero I] [inst_3 : DecidableEq I]
  [inst_4 : CategoryTheory.Limits.HasInitial C] (F : CategoryTheory.Functor D (CategoryTheory.Functor C D)) (Y : C)
  (e : F.flip.obj Y ≅ CategoryTheory.Functor.id D)
  [inst_5 : ∀ (X : D), CategoryTheory.Limits.PreservesColimit (CategoryTheory.Functor.empty C) (F.obj X)]
  (p : J × I → J) (hp : ∀ (j : J), p (j, 0) = j) (X : CategoryTheory.GradedObject J D)
  [inst_6 :
    (((CategoryTheory.GradedObject.mapBifunctor F J I).obj X).obj
          ((CategoryTheory.GradedObject.single₀ I).obj Y)).HasMap
      p]
  (j : J),
  (CategoryTheory.GradedObject.mapBifunctorRightUnitor F Y e p hp X).inv j =
    CategoryTheory.CategoryStruct.comp (e.inv.app (X j))
      (CategoryTheory.CategoryStruct.comp ((F.obj (X j)).map (CategoryTheory.GradedObject.singleObjApplyIso 0 Y).inv)
        (CategoryTheory.GradedObject.ιMapBifunctorMapObj F p X ((CategoryTheory.GradedObject.single₀ I).obj Y) j 0 j ⋯))
-- Init.Data.SInt.Bitwise
instIdempotentOpInt32HOr : Std.IdempotentOp fun x1 x2 => x1 ||| x2
-- Mathlib.CategoryTheory.WithTerminal.Cone
_private.Mathlib.CategoryTheory.WithTerminal.Cone.0.CategoryTheory.WithTerminal.liftFromOverComp.match_1.splitter : {J : Type u_1} →
  (motive : CategoryTheory.WithTerminal J → Sort u_2) →
    (x : CategoryTheory.WithTerminal J) →
      (Unit → motive CategoryTheory.WithTerminal.star) →
        ((a : J) → motive (CategoryTheory.WithTerminal.of a)) → motive x
-- Mathlib.Algebra.Quaternion
QuaternionAlgebra.coe_intCast : ∀ {R : Type u_3} {c₁ c₂ c₃ : R} [inst : AddCommGroupWithOne R] (z : ℤ), ↑↑z = ↑z
-- Mathlib.AlgebraicTopology.FundamentalGroupoid.SimplyConnected
isSimplyConnected_vadd_set_iff : ∀ {X : Type u_1} [inst : TopologicalSpace X] {G : Type u_3} [inst_1 : AddGroup G] [inst_2 : AddAction G X]
  [ContinuousConstVAdd G X] {c : G} {s : Set X}, IsSimplyConnected (c +ᵥ s) ↔ IsSimplyConnected s
-- Std.Data.ExtTreeMap.Basic
/-- Erases multiple mappings from the tree map by iterating over the given collection and calling
`erase`.
 -/
Std.ExtTreeMap.eraseMany : {α : Type u} →
  {β : Type v} →
    {cmp : α → α → Ordering} →
      [Std.TransCmp cmp] → {ρ : Type u_1} → [ForIn Id ρ α] → Std.ExtTreeMap α β cmp → ρ → Std.ExtTreeMap α β cmp
-- Mathlib.CategoryTheory.Triangulated.Opposite.Basic
CategoryTheory.Pretriangulated.shift_unop_opShiftFunctorEquivalence_counitIso_hom_app : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.HasShift C ℤ] (X : Cᵒᵖ) (n : ℤ),
  (CategoryTheory.shiftFunctor C n).map
      ((CategoryTheory.Pretriangulated.opShiftFunctorEquivalence C n).counitIso.hom.app X).unop =
    ((CategoryTheory.Pretriangulated.opShiftFunctorEquivalence C n).unitIso.inv.app
        (Opposite.op ((CategoryTheory.shiftFunctor C n).obj (Opposite.unop X)))).unop
-- Batteries.Data.String.Lemmas
_private.Batteries.Data.String.Lemmas.0.List.filter.match_1.splitter : (motive : Bool → Sort u_1) → (x : Bool) → (Unit → motive true) → (Unit → motive false) → motive x
-- Mathlib.CategoryTheory.Adjunction.Basic
CategoryTheory.Adjunction.mk'_homEquiv : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  {F : CategoryTheory.Functor C D} {G : CategoryTheory.Functor D C}
  (adj : CategoryTheory.Adjunction.CoreHomEquivUnitCounit F G),
  (CategoryTheory.Adjunction.mk' adj).homEquiv = adj.homEquiv
-- Mathlib.Algebra.Group.Action.Pointwise.Set.Basic
Set.mulActionSet.eq_1 : ∀ {α : Type u_2} {β : Type u_3} [inst : Monoid α] [inst_1 : MulAction α β],
  Set.mulActionSet = { toSMul := Set.smulSet, mul_smul := ⋯, one_smul := ⋯ }
-- Mathlib.AlgebraicTopology.DoldKan.FunctorGamma
AlgebraicTopology.DoldKan.Γ₀'_map_f : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Preadditive C]
  [inst_2 : CategoryTheory.Limits.HasFiniteCoproducts C] {K K' : ChainComplex C ℕ} (f : K ⟶ K') (i : ℕ),
  (AlgebraicTopology.DoldKan.Γ₀'.map f).f i = f.f i
-- Mathlib.Topology.Separation.Basic
Filter.Tendsto.eventually_ne : ∀ {Y : Type u_2} {X : Type u_3} [inst : TopologicalSpace Y] [T1Space Y] {g : X → Y} {l : Filter X} {b₁ b₂ : Y},
  Filter.Tendsto g l (nhds b₁) → b₁ ≠ b₂ → ∀ᶠ (z : X) in l, g z ≠ b₂
-- Std.Data.DTreeMap.Internal.Lemmas
Std.DTreeMap.Internal.Impl.forM_eq_forM_keys : ∀ {α : Type u} {β : α → Type v} {t : Std.DTreeMap.Internal.Impl α β} {m : Type w → Type w'} [inst : Monad m]
  [LawfulMonad m] {f : α → m PUnit.{w + 1}}, Std.DTreeMap.Internal.Impl.forM (fun a x => f a) t = t.keys.forM f
-- Init.Data.UInt.Lemmas
USize.toUInt64_ofNatClamp_of_lt : ∀ {n : ℕ} (hn : n < USize.size), (USize.ofNatClamp n).toUInt64 = UInt64.ofNatLT n ⋯
-- Mathlib.Order.Filter.Extr
IsMinOn.add : ∀ {α : Type u} {β : Type v} [inst : AddCommMonoid β] [inst_1 : PartialOrder β] [IsOrderedAddMonoid β] {f g : α → β}
  {a : α} {s : Set α}, IsMinOn f s a → IsMinOn g s a → IsMinOn (fun x => f x + g x) s a
-- Mathlib.GroupTheory.Coset.Basic
AddSubgroup.quotientiInfEmbedding_apply : ∀ {α : Type u_1} [inst : AddGroup α] {ι : Type u_2} (f : ι → AddSubgroup α) (q : α ⧸ ⨅ i, f i) (i : ι),
  (AddSubgroup.quotientiInfEmbedding f) q i = AddSubgroup.quotientMapOfLE ⋯ q
-- Mathlib.Tactic.NormNum.Eq
_private.Mathlib.Tactic.NormNum.Eq.0.Mathlib.Meta.NormNum.evalEq.nnratArm : {v : Lean.Level} →
  {β : Q(Type v)} →
    (e : Q(«$β»)) →
      (u : Lean.Level) →
        (α :
            have u := u;
            Q(Type u)) →
          (a b : Q(«$α»)) →
            Mathlib.Meta.NormNum.Result a →
              Mathlib.Meta.NormNum.Result b → Q(DivisionSemiring «$α») → Lean.MetaM (Mathlib.Meta.NormNum.Result e)
-- Lean.Meta.Match.SolveOverlap
_private.Lean.Meta.Match.SolveOverlap.0.Lean.Meta.Match.InjectionAnyResult.subgoal.inj : ∀ {fvarId : Lean.FVarId} {mvarId : Lean.MVarId} {fvarId_1 : Lean.FVarId} {mvarId_1 : Lean.MVarId},
  Lean.Meta.Match.InjectionAnyResult.subgoal✝ fvarId mvarId =
      Lean.Meta.Match.InjectionAnyResult.subgoal✝ fvarId_1 mvarId_1 →
    fvarId = fvarId_1 ∧ mvarId = mvarId_1
-- Mathlib.Topology.MetricSpace.Pseudo.Constructions
ball_prod_same : ∀ {α : Type u_1} {β : Type u_2} [inst : PseudoMetricSpace α] [inst_1 : PseudoMetricSpace β] (x : α) (y : β) (r : ℝ),
  Metric.ball x r ×ˢ Metric.ball y r = Metric.ball (x, y) r
-- Mathlib.MeasureTheory.MeasurableSpace.Embedding
MeasurableEmbedding.id : ∀ {α : Type u_1} {mα : MeasurableSpace α}, MeasurableEmbedding id
-- Mathlib.Topology.Compactification.OnePoint.Basic
OnePoint.specializes_coe : ∀ {X : Type u_1} [inst : TopologicalSpace X] {x y : X}, ↑x ⤳ ↑y ↔ x ⤳ y
-- Mathlib.CategoryTheory.Action.Monoidal
Action.functorCategoryEquivalenceInverseMonoidal : (V : Type u_1) →
  [inst : CategoryTheory.Category.{v_1, u_1} V] →
    (G : Type u_2) →
      [inst_1 : Monoid G] →
        [inst_2 : CategoryTheory.MonoidalCategory V] → (Action.functorCategoryEquivalence V G).inverse.Monoidal
-- Mathlib.Topology.Algebra.Support
tsupport_eq_empty_iff : ∀ {X : Type u_1} {α : Type u_2} [inst : Zero α] [inst_1 : TopologicalSpace X] {f : X → α}, tsupport f = ∅ ↔ f = 0
-- Mathlib.RingTheory.UniqueFactorizationDomain.ClassGroup
/-- The ideal class group of a GCD domain is trivial.
This includes unique factorization domains.  -/
IsGCDMonoid.subsingleton_classGroup : ∀ {R : Type u_1} [inst : CommRing R] [inst_1 : IsDomain R] [IsGCDMonoid R], Subsingleton (ClassGroup R)
-- Mathlib.CategoryTheory.Monoidal.Ring
CategoryTheory.RingObjCat.id_hom : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.CartesianMonoidalCategory C]
  [inst_2 : CategoryTheory.BraidedCategory C] (X : CategoryTheory.RingObjCat C),
  (CategoryTheory.CategoryStruct.id X).hom = CategoryTheory.CategoryStruct.id X.X
-- Mathlib.CategoryTheory.Bicategory.CatEnriched
CategoryTheory.CatEnrichedOrdinary.Hom.ext_iff : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C]
  [inst_1 : CategoryTheory.EnrichedOrdinaryCategory CategoryTheory.Cat C] {X Y : CategoryTheory.CatEnrichedOrdinary C}
  {f g : X ⟶ Y} {α β : f ⟶ g},
  α = β ↔ CategoryTheory.CatEnrichedOrdinary.Hom.base α = CategoryTheory.CatEnrichedOrdinary.Hom.base β
-- Mathlib.Algebra.BigOperators.Finprod
finsum_mem_eq_zero_of_forall_eq_zero : ∀ {α : Type u_1} {M : Type u_5} [inst : AddCommMonoid M] {f : α → M} {s : Set α},
  (∀ x ∈ s, f x = 0) → ∑ᶠ (i : α) (_ : i ∈ s), f i = 0
-- Mathlib.Order.Basic
LE.le.not_lt_iff_eq' : ∀ {α : Type u_2} [inst : PartialOrder α] {a b : α}, b ≤ a → (¬b < a ↔ a = b)
-- Lean.MetavarContext
/-- Add `mvarId := x` to the metavariable assignment.
This method does not check whether `mvarId` is already assigned, nor does it check whether
a cycle is being introduced, or whether the expression has the right type.
This is a low-level API, and it is safer to use `isDefEq (mkMVar mvarId) x`.
 -/
Lean.MVarId.assign : {m : Type → Type} → [Lean.MonadMCtx m] → Lean.MVarId → Lean.Expr → m Unit
-- Lean.Data.Lsp.LanguageFeatures
Lean.Lsp.SemanticTokensOptions.mk.inj : ∀ {legend : Lean.Lsp.SemanticTokensLegend} {range full : Bool} {legend_1 : Lean.Lsp.SemanticTokensLegend}
  {range_1 full_1 : Bool},
  { legend := legend, range := range, full := full } = { legend := legend_1, range := range_1, full := full_1 } →
    legend = legend_1 ∧ range = range_1 ∧ full = full_1
-- Mathlib.RepresentationTheory.Coinvariants
Representation.coinvariantsToFinsupp.eq_1 : ∀ {k : Type u_6} {G : Type u_7} {V : Type u_8} [inst : CommRing k] [inst_1 : Group G] [inst_2 : AddCommGroup V]
  [inst_3 : Module k V] (ρ : Representation k G V) (α : Type u_9),
  ρ.coinvariantsToFinsupp α =
    Representation.Coinvariants.lift (ρ.finsupp α) (Finsupp.mapRange.linearMap (Representation.Coinvariants.mk ρ)) ⋯
-- Lean.Message
Lean.MessageData.trace.sizeOf_spec : ∀ (data : Lean.TraceData) (msg : Lean.MessageData) (children : Array Lean.MessageData),
  sizeOf (Lean.MessageData.trace data msg children) = 1 + sizeOf data + sizeOf msg + sizeOf children
-- Mathlib.Algebra.Colimit.DirectLimit
DirectLimit.instZero.eq_1 : ∀ {ι : Type u_2} [inst : Preorder ι] {G : ι → Type u_3} {T : ⦃i j : ι⦄ → i ≤ j → Type u_6}
  {f : (x x_1 : ι) → (h : x ≤ x_1) → T h} [inst_1 : (i j : ι) → (h : i ≤ j) → FunLike (T h) (G i) (G j)]
  [inst_2 : DirectedSystem G fun x1 x2 x3 => ⇑(f x1 x2 x3)] [inst_3 : IsDirectedOrder ι] [inst_4 : Nonempty ι]
  [inst_5 : (i : ι) → Zero (G i)], DirectLimit.instZero = { zero := DirectLimit.map₀ f fun x => 0 }
-- Lean.Elab.Do.Legacy
Lean.Elab.Term.Do.mkFreshJP : Array (Lean.Elab.Term.Do.Var × Bool) → Lean.Elab.Term.Do.Code → Lean.Elab.TermElabM Lean.Elab.Term.Do.JPDecl
-- Std.Data.DTreeMap.Internal.Model
Std.DTreeMap.Internal.Impl.erase.eq_2 : ∀ {α : Type u} {β : α → Type v} [inst : Ord α] (k : α) (sz : ℕ) (k' : α) (v' : β k')
  (l' r' : Std.DTreeMap.Internal.Impl α β) (hr_1 : (Std.DTreeMap.Internal.Impl.inner sz k' v' l' r').Balanced),
  Std.DTreeMap.Internal.Impl.erase k (Std.DTreeMap.Internal.Impl.inner sz k' v' l' r') hr_1 =
    match compare k k' with
    | Ordering.lt =>
      match Std.DTreeMap.Internal.Impl.erase k l' ⋯ with
      | { impl := l'_1, balanced_impl := hl'₁, lb_le_size_impl := hl'₂, size_impl_le_ub := hl'₃ } =>
        { impl := Std.DTreeMap.Internal.Impl.balanceRErase k' v' l'_1 r' ⋯ ⋯ ⋯, balanced_impl := ⋯,
          lb_le_size_impl := ⋯, size_impl_le_ub := ⋯ }
    | Ordering.gt =>
      match Std.DTreeMap.Internal.Impl.erase k r' ⋯ with
      | { impl := r'_1, balanced_impl := hr'₁, lb_le_size_impl := hr'₂, size_impl_le_ub := hr'₃ } =>
        { impl := Std.DTreeMap.Internal.Impl.balanceLErase k' v' l' r'_1 ⋯ ⋯ ⋯, balanced_impl := ⋯,
          lb_le_size_impl := ⋯, size_impl_le_ub := ⋯ }
    | Ordering.eq => { impl := l'.glue r' ⋯ ⋯ ⋯, balanced_impl := ⋯, lb_le_size_impl := ⋯, size_impl_le_ub := ⋯ }
-- Mathlib.Data.Set.Subsingleton
Set.Nontrivial.choose_fst_ne_choose_snd : ∀ {α : Type u} {s : Set α} (hs : s.Nontrivial), hs.choose.1 ≠ hs.choose.2
-- Mathlib.CategoryTheory.Sites.Sheaf
/-- Given sieve `S` and presheaf `P : Cᵒᵖ ⥤ A`, their natural associated cone admits at most one
morphism from every cone in the same category (i.e. over the same diagram),
iff `Hom (E, P -)` is separated for the sieve `S` and all `E : A`.  -/
CategoryTheory.Presheaf.subsingleton_iff_isSeparatedFor : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {A : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} A]
  (P : CategoryTheory.Functor Cᵒᵖ A) {X : C} (S : CategoryTheory.Sieve X),
  (∀ (c : CategoryTheory.Limits.Cone (S.arrows.diagram.op.comp P)), Subsingleton (c ⟶ P.mapCone S.arrows.cocone.op)) ↔
    ∀ (E : Aᵒᵖ), CategoryTheory.Presieve.IsSeparatedFor (P.comp (CategoryTheory.coyoneda.obj E)) S.arrows