mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Data.List.Cycle
/-- The `s : Cycle α` as a `Finset α`.  -/
Cycle.toFinset : {α : Type u_1} → [DecidableEq α] → Cycle α → Finset α
-- Mathlib.CategoryTheory.ConcreteCategory.Basic
/-- In any concrete category, we can test equality of morphisms by pointwise evaluations.  -/
CategoryTheory.ConcreteCategory.ext : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {FC : C → C → Type u_1} {CC : C → Type w}
  [inst_1 : (X Y : C) → FunLike (FC X Y) (CC X) (CC Y)] [inst_2 : CategoryTheory.ConcreteCategory C FC] {X Y : C}
  {f g : X ⟶ Y}, CategoryTheory.ConcreteCategory.hom f = CategoryTheory.ConcreteCategory.hom g → f = g
-- Mathlib.GroupTheory.GroupAction.SubMulAction.OfStabilizer
SubAddAction.ofStabilizer.neg_addConjMap_comp_apply : ∀ {G : Type u_1} [inst : AddGroup G] {α : Type u_2} [inst_1 : AddAction G α] {g : G} {a b : α} (hg : b = g +ᵥ a)
  (x : ↥(SubAddAction.ofStabilizer G b)),
  (SubAddAction.ofStabilizer.conjMap hg) ((SubAddAction.ofStabilizer.conjMap ⋯) x) = x
-- Mathlib.SetTheory.Cardinal.Arithmetic
Cardinal.add_right_inj_of_lt_aleph0 : ∀ {α β γ : Cardinal.{u_1}}, γ < Cardinal.aleph0 → (α + γ = β + γ ↔ α = β)
-- Mathlib.Data.Finsupp.Sigma
Finsupp.embSigma_apply_self : ∀ {κ : Type u_1} {ι : κ → Type u_2} {M : Type u_3} [inst : Zero M] {k : κ} (f : ι k →₀ M) (i : ι k),
  f.embSigma ⟨k, i⟩ = f i
-- Mathlib.LinearAlgebra.ExteriorAlgebra.Basic
ExteriorAlgebra.isLocalHom_algebraMap : ∀ {R : Type u1} [inst : CommRing R] (M : Type u2) [inst_1 : AddCommGroup M] [inst_2 : Module R M],
  IsLocalHom (algebraMap R (ExteriorAlgebra R M))
-- Mathlib.AlgebraicGeometry.Restrict
AlgebraicGeometry.Scheme.isoOfEq_hom_ι : ∀ (X : AlgebraicGeometry.Scheme) {U V : X.Opens} (e : U = V),
  CategoryTheory.CategoryStruct.comp (X.isoOfEq e).hom V.ι = U.ι
-- Mathlib.Data.ZMod.Basic
RingHom.ext_zmod : ∀ {n : ℕ} {R : Type u_1} [inst : NonAssocSemiring R] (f g : ZMod n →+* R), f = g
-- Mathlib.LinearAlgebra.LinearPMap
LinearPMap.domRestrict_le : ∀ {R : Type u_1} {S : Type u_2} [inst : Ring R] [inst_1 : Ring S] {σ : R →+* S} {E : Type u_4} [inst_2 : AddCommGroup E]
  [inst_3 : Module R E] {F : Type u_5} [inst_4 : AddCommGroup F] [inst_5 : Module S F] {f : E →ₛₗ.[σ] F}
  {S_1 : Submodule R E}, f.domRestrict S_1 ≤ f
-- Mathlib.GroupTheory.Perm.Support
/-- The `Finset` of nonfixed points of a permutation.  -/
Equiv.Perm.support : {α : Type u_1} → [DecidableEq α] → [Fintype α] → Equiv.Perm α → Finset α
-- Mathlib.Algebra.Homology.ShortComplex.Exact
/-- The exact short complex `kernel f ⟶ X ⟶ Y` for any morphism `f : X ⟶ Y`.  -/
CategoryTheory.ShortComplex.kernelSequence : {C : Type u_1} →
  [inst : CategoryTheory.Category.{v_1, u_1} C] →
    [inst_1 : CategoryTheory.Abelian C] → {X Y : C} → (X ⟶ Y) → CategoryTheory.ShortComplex C
-- Mathlib.Tactic.ComputeAsymptotics.Multiseries.Corecursion
/-- Metric space structure on `Seq α` considering `α` as a discrete metric space.  -/
Tactic.ComputeAsymptotics.Seq.instMetricSpaceSeq : {α : Type u_1} → MetricSpace (Stream'.Seq α)
-- Init.Prelude
/-- The number of bytes used by the string's UTF-8 encoding.
 -/
Substring.Raw.bsize : Substring.Raw → ℕ
-- Batteries.Lean.LawfulMonad
instLawfulMonadTermElabM_batteries : LawfulMonad Lean.Elab.TermElabM
-- Init.Data.Array.InsertIdx
Array.toList_insertIdx : ∀ {α : Type u} {xs : Array α} {i : ℕ} {x : α} (h : i ≤ xs.size), (xs.insertIdx i x h).toList = xs.toList.insertIdx i x
-- Init.Sym.Lemmas
Lean.Sym.not_true_eq : (¬True) = False
-- Mathlib.Order.Filter.Prod
Filter.comap_prod : ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} (f : α → β × γ) (b : Filter β) (c : Filter γ),
  Filter.comap f (b ×ˢ c) = Filter.comap (Prod.fst ∘ f) b ⊓ Filter.comap (Prod.snd ∘ f) c
-- Mathlib.Algebra.DualQuaternion
Quaternion.snd_imJ_dualNumberEquiv_symm : ∀ {R : Type u_1} [inst : CommRing R] (d : DualNumber (Quaternion R)),
  TrivSqZeroExt.snd (Quaternion.dualNumberEquiv.symm d).imJ = (TrivSqZeroExt.snd d).imJ
-- Mathlib.Order.CompleteSublattice
CompleteSublattice.sSupClosed : ∀ {α : Type u_1} [inst : CompleteLattice α] {L : CompleteSublattice α} {s : Set α}, s ⊆ ↑L → sSup s ∈ L
-- Mathlib.CategoryTheory.Limits.Shapes.Images
CategoryTheory.Limits.image.lift_fac : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {X Y : C} {f : X ⟶ Y}
  [inst_1 : CategoryTheory.Limits.HasImage f] (F' : CategoryTheory.Limits.MonoFactorisation f),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.image.lift F') F'.m = CategoryTheory.Limits.image.ι f
-- Lean.Elab.Tactic.Basic
Lean.Elab.Tactic.EvalTacticFailure.mk : Lean.Exception → Lean.Elab.Tactic.SavedState → Lean.Elab.Tactic.EvalTacticFailure
-- Mathlib.CategoryTheory.Comma.StructuredArrow.Basic
CategoryTheory.CostructuredArrow.preEquivalence.inverse_obj_left_left : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  {E : Type u₃} [inst_2 : CategoryTheory.Category.{v₃, u₃} E] (F : CategoryTheory.Functor C D)
  {G : CategoryTheory.Functor D E} {e : E} (f : CategoryTheory.CostructuredArrow G e)
  (g : CategoryTheory.CostructuredArrow F f.left),
  ((CategoryTheory.CostructuredArrow.preEquivalence.inverse F f).obj g).left.left = g.left
-- Mathlib.CategoryTheory.Monoidal.Braided.Multifunctor
CategoryTheory.BraidedCategory.ofBifunctor.Forward.firstMap₃_app_app_app : ∀ (C : Type u_1) [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.MonoidalCategory C]
  (x x_1 x_2 : C),
  (((CategoryTheory.BraidedCategory.ofBifunctor.Forward.firstMap₃ C).app x).app x_1).app x_2 =
    (CategoryTheory.MonoidalCategoryStruct.associator x_1 x_2 x).hom
-- Std.Tactic.BVDecide.Bitblast.BVExpr.Circuit.Lemmas.Operations.ShiftLeft
Std.Tactic.BVDecide.BVExpr.bitblast.blastShiftLeftConst.go_get : ∀ {α : Type} [inst : Hashable α] [inst_1 : DecidableEq α] {w : ℕ} (aig : Std.Sat.AIG α) (distance : ℕ)
  (input : aig.RefVec w) (curr : ℕ) (hcurr : curr ≤ w) (s : aig.RefVec curr) (idx : ℕ) (hidx : idx < curr),
  (Std.Tactic.BVDecide.BVExpr.bitblast.blastShiftLeftConst.go aig input distance curr hcurr s).vec.get idx ⋯ =
    (s.get idx hidx).cast ⋯
-- Init.Data.List.Basic
List.range'TR.go.eq_2 : ∀ (step a : ℕ) (a_1 : List ℕ) (n : ℕ),
  List.range'TR.go step n.succ a a_1 = List.range'TR.go step n (a - step) ((a - step) :: a_1)
-- Mathlib.CategoryTheory.Sites.Sieves
CategoryTheory.Sieve.pullback_eq_top_of_mem : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {X Y : C} (S : CategoryTheory.Sieve X) {f : Y ⟶ X},
  S.arrows f → CategoryTheory.Sieve.pullback f S = ⊤
-- Std.Data.ExtDTreeMap.Lemmas
Std.ExtDTreeMap.ofList_eq_empty_iff : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} [Std.TransCmp cmp] {l : List ((a : α) × β a)},
  Std.ExtDTreeMap.ofList l cmp = ∅ ↔ l = []
-- Mathlib.Tactic.GCongr.Core
/-- Get the `gcongr` lemmas whose conclusion has the shape
`relName (head ..) _`, if `forward := true`, or `rel _ (head ..)`, if `forward := false`.
`arity` is the number of arguments in `..`. This is used by the `grw` tactic.  -/
Mathlib.Tactic.GCongr.findGCongrLemmas?' : Lean.Name → Lean.Name → Bool → ℕ → Lean.CoreM (List Mathlib.Tactic.GCongr.GCongrLemma)
-- Mathlib.RingTheory.IntegralClosure.IsIntegralClosure.Basic
IsIntegral.nsmul : ∀ {R : Type u_1} {B : Type u_3} [inst : CommRing R] [inst_1 : Ring B] [inst_2 : Algebra R B] {x : B},
  IsIntegral R x → ∀ (n : ℕ), IsIntegral R (n • x)
-- Lean.Data.Lsp.Ipc
Lean.Lsp.Ipc.CallHierarchy.fromRanges : Lean.Lsp.Ipc.CallHierarchy → Array Lean.Lsp.Range
-- Mathlib.Algebra.Module.Torsion.Basic
Module.isTorsionBy_quotient_element_smul : ∀ {R : Type u_1} (M : Type u_2) [inst : CommRing R] [inst_1 : AddCommGroup M] [inst_2 : Module R M] (r : R),
  Module.IsTorsionBy R (M ⧸ r • ⊤) r
-- Std.Data.ExtDHashMap.Lemmas
Std.ExtDHashMap.get_getKey? : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} {β : α → Type v} {m : Std.ExtDHashMap α β} [inst : EquivBEq α]
  [inst_1 : LawfulHashable α] {a : α} {h : (m.getKey? a).isSome = true}, (m.getKey? a).get h = m.getKey a ⋯
-- Mathlib.AlgebraicGeometry.PullbackCarrier
AlgebraicGeometry.Scheme.Pullback.Triplet.ext_iff : ∀ {X Y S : AlgebraicGeometry.Scheme} {f : X ⟶ S} {g : Y ⟶ S} {t₁ t₂ : AlgebraicGeometry.Scheme.Pullback.Triplet f g},
  t₁ = t₂ ↔ t₁.x = t₂.x ∧ t₁.y = t₂.y
-- Mathlib.CategoryTheory.LocallyCartesianClosed.Over
CategoryTheory.toOverIteratedSliceForwardIsoPullback_inv_app_left : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.ChosenPullbacks C] {X Y : C}
  (f : Y ⟶ X) (X_1 : CategoryTheory.Over X),
  ((CategoryTheory.toOverIteratedSliceForwardIsoPullback f).inv.app X_1).left =
    CategoryTheory.Over.Hom.left
      ((((((((CategoryTheory.Over.mk f).iteratedSliceBackward.comp
                                  (CategoryTheory.Over.forget (CategoryTheory.Over.mk f))).leftUnitor.symm.homCongr
                          (CategoryTheory.Over.map f).rightUnitor.symm).trans
                      (CategoryTheory.TwoSquare.equivNatTrans (CategoryTheory.Functor.id (CategoryTheory.Over Y))
                          (CategoryTheory.Over.map f)
                          ((CategoryTheory.Over.mk f).iteratedSliceBackward.comp
                            (CategoryTheory.Over.forget (CategoryTheory.Over.mk f)))
                          (CategoryTheory.Functor.id (CategoryTheory.Over X))).symm).trans
                  (CategoryTheory.mateEquiv (CategoryTheory.ChosenPullbacksAlong.mapPullbackAdj f)
                    ((CategoryTheory.Over.mk f).iteratedSliceEquiv.symm.toAdjunction.comp
                      (CategoryTheory.forgetAdjToOver (CategoryTheory.Over.mk f))))).trans
              (CategoryTheory.TwoSquare.equivNatTrans (CategoryTheory.ChosenPullbacksAlong.pullback f)
                (CategoryTheory.Functor.id (CategoryTheory.Over X)) (CategoryTheory.Functor.id (CategoryTheory.Over Y))
                ((CategoryTheory.toOver (CategoryTheory.Over.mk f)).comp
                  (CategoryTheory.Over.mk f).iteratedSliceForward)))
            (CategoryTheory.eqToHom ⋯)).app
        X_1)
-- Mathlib.Topology.MetricSpace.Bounded
Metric.isBounded_range_of_tendsto_cofinite : ∀ {α : Type u} {β : Type v} [inst : PseudoMetricSpace α] {f : β → α} {a : α},
  Filter.Tendsto f Filter.cofinite (nhds a) → Bornology.IsBounded (Set.range f)
-- Mathlib.Data.List.Sym
List.sym_one_eq : ∀ {α : Type u_1} {xs : List α}, List.sym 1 xs = List.map (fun x => x ::ₛ Sym.nil) xs
-- Mathlib.Topology.Algebra.Group.GroupTopology
AddGroupTopology.mk.sizeOf_spec : ∀ {α : Type u} [inst : AddGroup α] [inst_1 : SizeOf α] (toTopologicalSpace : TopologicalSpace α)
  (toIsTopologicalAddGroup : IsTopologicalAddGroup α),
  sizeOf { toTopologicalSpace := toTopologicalSpace, toIsTopologicalAddGroup := toIsTopologicalAddGroup } =
    1 + sizeOf toTopologicalSpace + sizeOf toIsTopologicalAddGroup
-- Init.Data.Range.Polymorphic.Lemmas
Std.Roi.toList.congr_simp : ∀ {α : Type u} [inst : Std.PRange.UpwardEnumerable α] [inst_1 : Std.PRange.LawfulUpwardEnumerable α]
  [inst_2 : Std.Rxi.IsAlwaysFinite α] (r r_1 : Std.Roi α), r = r_1 → r.toList = r_1.toList
-- Init.Data.Int.Order
Int.sign_mul_self : ∀ (i : ℤ), i.sign * i = ↑i.natAbs
-- Mathlib.ModelTheory.Arithmetic.Presburger.Semilinear.Basic
/-- **Alias** of `isSemilinearSet_setOfPred_eq`.

---

The set of solutions to a linear equation `a + f x = b + g y` in a finitely generated monoid is
semilinear.  -/
isSemilinearSet_setOf_eq : ∀ {M : Type u_1} {N : Type u_2} [inst : AddCommMonoid M] [inst_1 : AddCommMonoid N] [AddMonoid.FG M] {F : Type u_5}
  {G : Type u_6} [inst_3 : FunLike F M N] [AddMonoidHomClass F M N] [inst_5 : FunLike G M N] [AddMonoidHomClass G M N]
  (a b : N) (f : F) (g : G), IsSemilinearSet {x | a + f x = b + g x}
-- Std.Data.DTreeMap.Lemmas
Std.DTreeMap.getD_inter : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t₁ t₂ : Std.DTreeMap α β cmp} [Std.TransCmp cmp]
  [inst : Std.LawfulEqCmp cmp] {k : α} {fallback : β k},
  (t₁ ∩ t₂).getD k fallback = if k ∈ t₂ then t₁.getD k fallback else fallback
-- Mathlib.RingTheory.FractionalIdeal.Operations
FractionalIdeal.map_ne_zero : ∀ {R : Type u_1} [inst : CommRing R] {K : Type u_3} {K' : Type u_4} [inst_1 : Field K] [inst_2 : Field K']
  [inst_3 : Algebra R K] [IsFractionRing R K] [inst_5 : Algebra R K'] [IsFractionRing R K']
  {I : FractionalIdeal (nonZeroDivisors R) K} (h : K →ₐ[R] K') [Nontrivial R], I ≠ 0 → FractionalIdeal.map h I ≠ 0
-- Mathlib.Combinatorics.SetFamily.AhlswedeZhang
Finset.card_truncatedInf_union_add_card_truncatedInf_sups : ∀ {α : Type u_1} [inst : DecidableEq α] [inst_1 : Fintype α] (𝒜 ℬ : Finset (Finset α)) (s : Finset α),
  ((𝒜 ∪ ℬ).truncatedInf s).card + ((𝒜 ⊻ ℬ).truncatedInf s).card = (𝒜.truncatedInf s).card + (ℬ.truncatedInf s).card
-- Mathlib.CategoryTheory.Limits.Cones
CategoryTheory.Limits.coconeRightOpOfConeEquiv_functor_obj : ∀ {J : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} J] {C : Type u₃} [inst_1 : CategoryTheory.Category.{v₃, u₃} C]
  {F : CategoryTheory.Functor Jᵒᵖ C} (c : (CategoryTheory.Limits.Cone F)ᵒᵖ),
  CategoryTheory.Limits.coconeRightOpOfConeEquiv.functor.obj c =
    CategoryTheory.Limits.coconeRightOpOfCone (Opposite.unop c)
-- Mathlib.CategoryTheory.WithTerminal.Basic
CategoryTheory.WithInitial.opEquiv_unitIso_inv_app : ∀ (C : Type u) [inst : CategoryTheory.Category.{v, u} C] (X : (CategoryTheory.WithInitial C)ᵒᵖ),
  (CategoryTheory.WithInitial.opEquiv C).unitIso.inv.app X =
    (match Opposite.unop X with
      | CategoryTheory.WithInitial.of x => CategoryTheory.Iso.refl (Opposite.op (CategoryTheory.WithInitial.of x))
      | CategoryTheory.WithInitial.star => CategoryTheory.Iso.refl (Opposite.op CategoryTheory.WithInitial.star)).inv
-- Mathlib.Order.Filter.Germ.Basic
/-- Given a map `F : (α → β) → (γ → δ)` that sends functions eventually equal at `l` to functions
eventually equal at `lc`, returns a map from `Germ l β` to `Germ lc δ`.  -/
Filter.Germ.map' : {α : Type u_1} →
  {β : Type u_2} →
    {γ : Type u_3} →
      {δ : Type u_4} →
        {l : Filter α} →
          {lc : Filter γ} →
            (F : (α → β) → γ → δ) → Relator.LiftFun l.EventuallyEq lc.EventuallyEq F F → l.Germ β → lc.Germ δ
-- Mathlib.Topology.MetricSpace.Antilipschitz
/-- **Alias** of the forward direction of `antilipschitzWith_iff_le_mul_dist`. -/
AntilipschitzWith.le_mul_dist : ∀ {α : Type u_1} {β : Type u_2} [inst : PseudoMetricSpace α] [inst_1 : PseudoMetricSpace β] {K : NNReal} {f : α → β},
  AntilipschitzWith K f → ∀ (x y : α), dist x y ≤ ↑K * dist (f x) (f y)
-- Lean.Syntax
Lean.Syntax.updateTrailing : Substring.Raw → Lean.Syntax → Lean.Syntax
-- Mathlib.Algebra.Group.Even
Even.zsmul_left : ∀ {α : Type u_2} [inst : AddGroup α] {n : ℤ}, Even n → ∀ (a : α), Even (n • a)
-- Mathlib.Algebra.Free
FreeSemigroup.ext_iff : ∀ {α : Type u} {x y : FreeSemigroup α}, x = y ↔ x.head = y.head ∧ x.tail = y.tail
-- Lean.Util.Diff
Lean.Diff.instHashableAction.hash : Lean.Diff.Action → UInt64
-- Mathlib.Analysis.Normed.Group.Basic
enorm_neg : ∀ {E : Type u_5} [inst : SeminormedAddGroup E] (a : E), ‖-a‖ₑ = ‖a‖ₑ
-- Mathlib.Order.Category.PartOrdEmb
/-- Let `P` be a predicate on `Set α` where `α : PartOrdEmb`. We assume
that `Subtype P` is directed and nonempty, and that any `a : α` belongs
to some `J : Set α` satisfying `P`. Then, `α` is the colimit in the
category `PartOrdEmb` of these subsets.  -/
PartOrdEmb.isColimitOfPredicateSet : {α : PartOrdEmb} →
  (P : Set ↑α → Prop) →
    [IsDirectedOrder (Subtype P)] →
      [Nonempty (Subtype P)] →
        (∀ (a : ↑α), ∃ J, P J ∧ a ∈ J) → CategoryTheory.Limits.IsColimit (PartOrdEmb.coconeOfPredicateSet P)
-- Mathlib.CategoryTheory.Monoidal.Free.Coherence
CategoryTheory.FreeMonoidalCategory.normalizeMapAux.eq_1 : ∀ {C : Type u} (x : CategoryTheory.FreeMonoidalCategory C),
  CategoryTheory.FreeMonoidalCategory.normalizeMapAux (CategoryTheory.FreeMonoidalCategory.Hom.id x) =
    CategoryTheory.CategoryStruct.id x.normalizeObj'
-- Mathlib.Algebra.AddConstMap.Basic
AddConstMapClass.map_sub_one : ∀ {F : Type u_1} {G : Type u_2} {H : Type u_3} [inst : FunLike F G H] {b : H} [inst_1 : AddGroup G] [inst_2 : One G]
  [inst_3 : AddGroup H] [AddConstMapClass F G H 1 b] (f : F) (x : G), f (x - 1) = f x - b
-- Std.Data.ExtDTreeMap.Lemmas
Std.ExtDTreeMap.insertMany_nil : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t : Std.ExtDTreeMap α β cmp} [inst : Std.TransCmp cmp],
  t.insertMany [] = t
-- Mathlib.Topology.Instances.Nat
Nat.isUniformEmbedding_coe_real : IsUniformEmbedding Nat.cast
-- Mathlib.Data.EReal.Basic
EReal.canLift : CanLift EReal ℝ Real.toEReal fun r => r ≠ ⊤ ∧ r ≠ ⊥
-- Lean.Meta.Tactic.Grind.Types
Lean.Meta.Grind.Goal.mk.sizeOf_spec : ∀ (toGoalState : Lean.Meta.Grind.GoalState) (mvarId : Lean.MVarId),
  sizeOf { toGoalState := toGoalState, mvarId := mvarId } = 1 + sizeOf toGoalState + sizeOf mvarId
-- Mathlib.AlgebraicGeometry.Sites.EtalePoint
AlgebraicGeometry.Scheme.instHasEnoughPointsEtaleSmallEtaleTopology : ∀ {S : AlgebraicGeometry.Scheme}, S.smallEtaleTopology.HasEnoughPoints
-- Mathlib.CategoryTheory.Subobject.Limits
CategoryTheory.Limits.imageSubobject_le : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {A B : C} {X : CategoryTheory.Subobject B} (f : A ⟶ B)
  [inst_1 : CategoryTheory.Limits.HasImage f] (h : A ⟶ CategoryTheory.Subobject.underlying.obj X),
  CategoryTheory.CategoryStruct.comp h X.arrow = f → CategoryTheory.Limits.imageSubobject f ≤ X
-- Mathlib.GroupTheory.Complement
AddSubgroup.IsComplement.existsUnique : ∀ {G : Type u_1} [inst : AddGroup G] {S T : Set G}, AddSubgroup.IsComplement S T → ∀ (g : G), ∃! x, ↑x.1 + ↑x.2 = g
-- Mathlib.Algebra.Homology.ShortComplex.LeftHomology
CategoryTheory.ShortComplex.leftHomologyMap_id : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  (S : CategoryTheory.ShortComplex C) [inst_2 : S.HasLeftHomology],
  CategoryTheory.ShortComplex.leftHomologyMap (CategoryTheory.CategoryStruct.id S) =
    CategoryTheory.CategoryStruct.id S.leftHomology
-- Mathlib.MeasureTheory.Group.Integral
/-- If some left-translate of a function negates it, then the integral of the function with
respect to a left-invariant measure is 0.  -/
MeasureTheory.integral_eq_zero_of_add_left_eq_neg : ∀ {G : Type u_4} {E : Type u_5} [inst : MeasurableSpace G] [inst_1 : NormedAddCommGroup E] [inst_2 : NormedSpace ℝ E]
  {μ : MeasureTheory.Measure G} {f : G → E} {g : G} [inst_3 : AddGroup G] [MeasurableAdd G] [μ.IsAddLeftInvariant],
  (∀ (x : G), f (g + x) = -f x) → ∫ (x : G), f x ∂μ = 0
-- Mathlib.Data.Rat.Defs
Rat.commMonoid : CommMonoid ℚ
-- Mathlib.CategoryTheory.Limits.Cones
CategoryTheory.Limits.Cocone.whiskering_map_hom : ∀ {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) {Y X : CategoryTheory.Limits.Cocone F} (f : Y ⟶ X),
  ((CategoryTheory.Limits.Cocone.whiskering E).map f).hom = f.hom
-- Mathlib.LinearAlgebra.TensorAlgebra.Basis
TensorAlgebra.equivFreeAlgebra_ι_apply : ∀ {κ : Type uκ} {R : Type uR} {M : Type uM} [inst : CommSemiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M]
  (b : Module.Basis κ R M) (i : κ), (TensorAlgebra.equivFreeAlgebra b) ((TensorAlgebra.ι R) (b i)) = FreeAlgebra.ι R i
-- Lean.Meta.DiscrTree.Basic
Lean.Meta.DiscrTree.instInhabitedTrie : {α : Type} → Inhabited (Lean.Meta.DiscrTree.Trie α)
-- Mathlib.CategoryTheory.Preadditive.Projective.Preserves
/-- A functor preserves projective objects if it maps projective objects to projective objects.  -/
CategoryTheory.Functor.PreservesProjectiveObjects : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    {D : Type u₂} → [inst_1 : CategoryTheory.Category.{v₂, u₂} D] → CategoryTheory.Functor C D → Prop
-- Mathlib.AlgebraicTopology.DoldKan.FunctorGamma
AlgebraicTopology.DoldKan.Γ₀_obj_obj : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Preadditive C]
  [inst_2 : CategoryTheory.Limits.HasFiniteCoproducts C] (X : ChainComplex C ℕ) (Δ : SimplexCategoryᵒᵖ),
  (AlgebraicTopology.DoldKan.Γ₀.obj X).obj Δ = AlgebraicTopology.DoldKan.Γ₀.Obj.obj₂ X Δ
-- Init.Conv
/-- Transforms `let` expressions into `have` expressions within the target expression when possible.
This is the conv mode version of the `let_to_have` tactic.
 -/
Lean.Parser.Tactic.Conv.letToHave : Lean.ParserDescr
-- Mathlib.Algebra.Homology.HomotopyCategory.KInjective
CochainComplex.IsKInjective.nonempty_homotopy_zero : ∀ {C : Type u_1} {inst : CategoryTheory.Category.{v_1, u_1} C} {inst_1 : CategoryTheory.Abelian C}
  {L : CochainComplex C ℤ} [self : L.IsKInjective] {K : CochainComplex C ℤ} (f : K ⟶ L),
  HomologicalComplex.Acyclic K → Nonempty (Homotopy f 0)
-- Mathlib.Dynamics.Ergodic.AddCircleAdd
AddCircle.ergodic_add_left : ∀ {p : ℝ} [inst : Fact (0 < p)] {a : AddCircle p}, Ergodic (fun x => a + x) MeasureTheory.volume ↔ addOrderOf a = 0
-- Mathlib.Algebra.Group.Submonoid.Units
Submonoid.mul_mem_units : ∀ {M : Type u_1} [inst : Monoid M] (S : Submonoid M) {x y : Mˣ}, x ∈ S.units → y ∈ S.units → x * y ∈ S.units
-- Init.Data.Array.Lemmas
Array.reverse_replicate : ∀ {α : Type u_1} {n : ℕ} {a : α}, (Array.replicate n a).reverse = Array.replicate n a
-- Mathlib.Algebra.Ring.Subsemiring.Basic
/-- The subsemiring generated by a set includes the set.  -/
Subsemiring.subset_closure : ∀ {R : Type u} [inst : NonAssocSemiring R] {s : Set R}, s ⊆ ↑(Subsemiring.closure s)
-- Init.Data.String.Basic
String.Slice.Pos.ofSliceFrom_le_ofSliceFrom_iff : ∀ {s : String.Slice} {p : s.Pos} {q r : (s.sliceFrom p).Pos},
  String.Slice.Pos.ofSliceFrom q ≤ String.Slice.Pos.ofSliceFrom r ↔ q ≤ r
-- Mathlib.Topology.Algebra.InfiniteSum.TsumUniformlyOn
HasSumUniformlyOn.of_norm_le_summable_eventually : ∀ {β : Type u_2} {F : Type u_3} [inst : NormedAddCommGroup F] [CompleteSpace F] {ι : Type u_4} {f : ι → β → F}
  {u : ι → ℝ},
  Summable u →
    ∀ {s : Set β},
      (∀ᶠ (n : ι) in Filter.cofinite, ∀ x ∈ s, ‖f n x‖ ≤ u n) → HasSumUniformlyOn f (fun x => ∑' (n : ι), f n x) s
-- Mathlib.Algebra.GroupWithZero.ProdHom
MonoidWithZeroHom.fst_inr_apply_of_ne_zero : ∀ {G₀ : Type u_1} {H₀ : Type u_2} [inst : GroupWithZero G₀] [inst_1 : GroupWithZero H₀]
  [inst_2 : DecidablePred fun x => x = 0] {x : H₀},
  x ≠ 0 → (MonoidWithZeroHom.fst G₀ H₀) ((MonoidWithZeroHom.inr G₀ H₀) x) = 1
-- Mathlib.Algebra.Order.Monovary
/-- **Alias** of the forward direction of `antivary_neg_right`. -/
Antivary.of_neg_right : ∀ {ι : Type u_1} {α : Type u_2} {β : Type u_3} [inst : PartialOrder α] [inst_1 : AddCommGroup β]
  [inst_2 : PartialOrder β] [IsOrderedAddMonoid β] {f : ι → α} {g : ι → β}, Antivary f (-g) → Monovary f g
-- Mathlib.CategoryTheory.DifferentialObject
/-- An isomorphism of differential objects can be constructed
from an isomorphism of the underlying objects that commutes with the differentials.  -/
CategoryTheory.DifferentialObject.mkIso : {S : Type u_1} →
  [inst : AddMonoidWithOne S] →
    {C : Type u} →
      [inst_1 : CategoryTheory.Category.{v, u} C] →
        [inst_2 : CategoryTheory.Limits.HasZeroMorphisms C] →
          [inst_3 : CategoryTheory.HasShift C S] →
            {X Y : CategoryTheory.DifferentialObject S C} →
              (f : X.obj ≅ Y.obj) →
                CategoryTheory.CategoryStruct.comp X.d ((CategoryTheory.shiftFunctor C 1).map f.hom) =
                    CategoryTheory.CategoryStruct.comp f.hom Y.d →
                  (X ≅ Y)
-- Mathlib.Analysis.SpecialFunctions.Trigonometric.Inverse
Real.arcsin_eq_iff_eq_sin : ∀ {x y : ℝ}, y ∈ Set.Ioo (-(Real.pi / 2)) (Real.pi / 2) → (Real.arcsin x = y ↔ x = Real.sin y)
-- Std.Data.HashSet.Lemmas
Std.HashSet.size_empty : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α}, ∅.size = 0
-- Init.Meta.Defs
Lean.instQuoteStringStrLitKind : Lean.Quote String Lean.strLitKind
-- Init.Data.Iterators.Lemmas.Combinators.FilterMap
Std.Iter.toList_mapM : ∀ {α β γ : Type w} [inst : Std.Iterator α Id β] {it : Std.Iter β} {m : Type w → Type w'} [inst_1 : Monad m]
  [inst_2 : MonadAttach m] [LawfulMonad m] [WeaklyLawfulMonadAttach m] [Std.Iterators.Finite α Id] {f : β → m γ},
  (Std.Iter.mapM f it).toList = List.mapM f it.toList