mathlib-initiative/mathlib-types huggingface dataset:
-- Lean.Meta.Tactic.Grind.Types
/-- Cached anchors (aka stable hash codes) for terms in the `grind` state.
 -/
Lean.Meta.Grind.State.anchors : Lean.Meta.Grind.State → Lean.PHashMap Lean.Meta.Sym.ExprPtr UInt64
-- Mathlib.MeasureTheory.Function.LpSpace.Basic
MeasureTheory.Lp.coeFn_zero : ∀ {α : Type u_1} (E : Type u_4) {m : MeasurableSpace α} (p : ENNReal) (μ : MeasureTheory.Measure α)
  [inst : NormedAddCommGroup E], ↑↑0 =ᵐ[μ] 0
-- Mathlib.Data.Set.Function
Set.BijOn.injOn : ∀ {α : Type u_1} {β : Type u_2} {s : Set α} {t : Set β} {f : α → β}, Set.BijOn f s t → Set.InjOn f s
-- Mathlib.Data.Finset.Defs
Finset.pairwise_subtype_iff_pairwise_finset : ∀ {α : Type u_1} {s : Finset α} (r : α → α → Prop), Pairwise (Function.onFun r fun x => ↑x) ↔ (↑s).Pairwise r
-- Mathlib.Algebra.Star.SelfAdjoint
star_comm_self' : ∀ {R : Type u_1} [inst : Mul R] [inst_1 : Star R] (x : R) [IsStarNormal x], star x * x = x * star x
-- Mathlib.Order.ConditionallyCompleteLattice.Basic
WithTop.isGLB_sInf : ∀ {α : Type u_1} [inst : ConditionallyCompleteLinearOrderBot α] (s : Set (WithTop α)), IsGLB s (sInf s)
-- Init.Data.Option.Lemmas
Option.le.eq_4 : ∀ {α : Type u_1} {β : Type u_2} (r : α → β → Prop) (x_2 : α) (y : β), Option.le r (some x_2) (some y) = r x_2 y
-- Mathlib.Topology.Algebra.Category.ProfiniteGrp.Basic
ProfiniteGrp.limit.eq_1 : ∀ {J : Type v} [inst : CategoryTheory.SmallCategory J] (F : CategoryTheory.Functor J ProfiniteGrp.{max v u}),
  ProfiniteGrp.limit F = ProfiniteGrp.of ↥(ProfiniteGrp.limitConePtAux F)
-- Std.Data.DTreeMap.Internal.Queries
Std.DTreeMap.Internal.Impl.mem_iff_contains : ∀ {α : Type u} {β : α → Type v} {x : Ord α} {t : Std.DTreeMap.Internal.Impl α β} {k : α},
  k ∈ t ↔ Std.DTreeMap.Internal.Impl.contains k t = true
-- Mathlib.Order.Hom.Basic
OrderIso.coe_refl : ∀ {α : Type u_2} [inst : LE α], ⇑(OrderIso.refl α) = id
-- Mathlib.Analysis.Convex.Uniform
exists_forall_closed_ball_dist_add_le_two_mul_sub : ∀ (E : Type u_1) [inst : SeminormedAddCommGroup E] [UniformConvexSpace E] {ε : ℝ} [NormedSpace ℝ E],
  0 < ε → ∀ (r : ℝ), ∃ δ, 0 < δ ∧ ∀ ⦃x : E⦄, ‖x‖ ≤ r → ∀ ⦃y : E⦄, ‖y‖ ≤ r → ε ≤ ‖x - y‖ → ‖x + y‖ ≤ 2 * r - δ
-- Mathlib.Analysis.Asymptotics.TVS
Asymptotics.IsBigOTVS.fst : ∀ {α : Type u_1} {𝕜 : Type u_3} {E : Type u_4} {F : Type u_5} {G : Type u_6} [inst : NontriviallyNormedField 𝕜]
  [inst_1 : AddCommGroup E] [inst_2 : TopologicalSpace E] [inst_3 : Module 𝕜 E] [inst_4 : AddCommGroup F]
  [inst_5 : TopologicalSpace F] [inst_6 : Module 𝕜 F] [inst_7 : AddCommGroup G] [inst_8 : TopologicalSpace G]
  [inst_9 : Module 𝕜 G] {l : Filter α} {f : α → E × F} {g : α → G}, f =O[𝕜; l] g → (fun x => (f x).1) =O[𝕜; l] g
-- Mathlib.Algebra.Group.Defs
npowRec_eq_npowBinRec : @npowRecAuto = @npowBinRecAuto
-- Mathlib.Algebra.Group.Pointwise.Set.Basic
Set.inv_subset_div_right : ∀ {α : Type u_2} [inst : DivisionMonoid α] {s t : Set α}, 1 ∈ s → t⁻¹ ⊆ s / t
-- Mathlib.Analysis.Real.Sqrt
/-- The natural floor of the real square root is the same as the natural square root.  -/
Real.nat_floor_real_sqrt_eq_nat_sqrt : ∀ {a : ℕ}, ⌊√↑a⌋₊ = a.sqrt
-- Mathlib.Data.Nat.MaxPowDiv
Nat.maxPowDvdDiv_zero_left : ∀ (n : ℕ), Nat.maxPowDvdDiv 0 n = (0, n)
-- Std.Time.Time.PlainTime
Std.Time.instTransOrdPlainTime : Std.TransOrd Std.Time.PlainTime
-- Mathlib.Data.List.Sublists
List.sublists_cons : ∀ {α : Type u} (a : α) (l : List α),
  (a :: l).sublists = do
    let x ← l.sublists
    [x, a :: x]
-- Init.Data.BitVec.Lemmas
BitVec.getMsbD_shiftLeftZeroExtend : ∀ {m i : ℕ} (x : BitVec m) (n : ℕ), (x.shiftLeftZeroExtend n).getMsbD i = x.getMsbD i
-- Lean.Meta.LazyDiscrTree
Lean.Meta.LazyDiscrTree.mk : {α : Type} →
  Array (Lean.Meta.LazyDiscrTree.Trie α) →
    Std.HashMap Lean.Meta.LazyDiscrTree.Key Lean.Meta.LazyDiscrTree.TrieIndex → Lean.Meta.LazyDiscrTree α
-- Mathlib.Combinatorics.Matroid.Circuit
/-- A cocircuit is a circuit of the dual matroid,
or equivalently the complement of a hyperplane.  -/
Matroid.IsCocircuit : {α : Type u_1} → Matroid α → Set α → Prop
-- Mathlib.MeasureTheory.Measure.ProbabilityMeasure
MeasureTheory.ProbabilityMeasure.apply_mono : ∀ {Ω : Type u_1} [inst : MeasurableSpace Ω] (μ : MeasureTheory.ProbabilityMeasure Ω) {s₁ s₂ : Set Ω},
  s₁ ⊆ s₂ → μ s₁ ≤ μ s₂
-- Lean.Meta.IndPredBelow
/-- Names of below declarations (corresponding to the motives)  -/
_private.Lean.Meta.IndPredBelow.0.Lean.Meta.IndPredBelow.Context.belowNames : Lean.Meta.IndPredBelow.Context✝ → Array Lean.Name
-- Mathlib.Topology.Constructible
IsRetrocompact.iInter : ∀ {ι : Sort u_1} {X : Type u_2} [inst : TopologicalSpace X] [T2Space X] [Finite ι] {f : ι → Set X},
  (∀ (i : ι), IsRetrocompact (f i)) → IsRetrocompact (⋂ i, f i)
-- Mathlib.CategoryTheory.Sites.Coherent.RegularSheaves
CategoryTheory.regularTopology.EqualizerCondition.bijective_mapToEqualizer_pullback' : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] {P : CategoryTheory.Functor Cᵒᵖ (Type u_4)},
  CategoryTheory.regularTopology.EqualizerCondition P →
    ∀ {X B : C} {π : X ⟶ B} [CategoryTheory.EffectiveEpi π] (c : CategoryTheory.Limits.PullbackCone π π)
      (hc : CategoryTheory.Limits.IsLimit c),
      Function.Bijective
        ⇑(CategoryTheory.ConcreteCategory.hom (CategoryTheory.regularTopology.mapToEqualizer P π c.fst c.snd ⋯))
-- Lean.Elab.Match
_private.Lean.Elab.Match.0.Lean.Elab.Term.ToDepElimPattern.normalize.processVar : Lean.Expr → Lean.Elab.Term.ToDepElimPattern.M Lean.Expr
-- Mathlib.Algebra.MonoidAlgebra.Module
MonoidAlgebra.supported_eq_span_single : ∀ (R : Type u_1) {M : Type u_3} [inst : Semiring R] (s : Set M),
  MonoidAlgebra.supported R R s = Submodule.span R ((fun m => MonoidAlgebra.single m 1) '' s)
-- Mathlib.Analysis.SpecialFunctions.Log.Summable
/-- The exponential of a convergent sum of complex logs is the corresponding infinite product.  -/
Complex.cexp_tsum_eq_tprod : ∀ {ι : Type u_1} {f : ι → ℂ},
  (∀ (i : ι), f i ≠ 0) →
    (Summable fun i => Complex.log (f i)) → Complex.exp (∑' (i : ι), Complex.log (f i)) = ∏' (i : ι), f i
-- Std.Data.DHashMap.RawLemmas
Std.DHashMap.Raw.getKey!_eq_of_contains : ∀ {α : Type u} {β : α → Type v} {m : Std.DHashMap.Raw α β} [inst : BEq α] [inst_1 : Hashable α] [LawfulBEq α]
  [inst_3 : Inhabited α], m.WF → ∀ {k : α}, m.contains k = true → m.getKey! k = k
-- Mathlib.Algebra.Order.Hom.Monoid
OrderMonoidHom.instInhabited.eq_1 : ∀ (α : Type u_2) [inst : Preorder α] [inst_1 : MulOneClass α],
  OrderMonoidHom.instInhabited α = { default := OrderMonoidHom.id α }
-- Mathlib.Algebra.Lie.Solvable
LieAlgebra.derivedSeries_lt_top_of_solvable : ∀ (R : Type u) (L : Type v) [inst : CommRing R] [inst_1 : LieRing L] [inst_2 : LieAlgebra R L] [LieAlgebra.IsSolvable L]
  [Nontrivial L], LieAlgebra.derivedSeries R L 1 < ⊤
-- Init.Data.List.ToArray
_private.Init.Data.List.ToArray.0.Array.eraseP.eq_1 : ∀ {α : Type u} (as : Array α) (p : α → Bool),
  as.eraseP p =
    match Array.findFinIdx? p as with
    | none => as
    | some i => as.eraseIdx ↑i ⋯
-- Mathlib.Tactic.Linarith.Frontend
/-- Insert a new value into the map at key `k`. This does a defeq check with all other keys
in the map.  -/
Mathlib.Tactic.Linarith.ExprMultiMap.insert : {α : Type} →
  Mathlib.Tactic.Linarith.ExprMultiMap α → Lean.Expr → α → Lean.MetaM (Mathlib.Tactic.Linarith.ExprMultiMap α)
-- Mathlib.Data.Fintype.Card
Fintype.card_of_bijective : ∀ {α : Type u_1} {β : Type u_2} [inst : Fintype α] [inst_1 : Fintype β] {f : α → β},
  Function.Bijective f → Fintype.card α = Fintype.card β
-- Lean.Elab.Quotation
/-- Match step that succeeds on `null` nodes of arity at least `numPrefix + numSuffix`, introducing discriminants
for the first `numPrefix` children, one `null` node for those in between, and for the `numSuffix` last children.
example: `([$x, $xs,*, $y]) is `slice 2 2`  -/
Lean.Elab.Term.Quotation.HeadCheck.slice : ℕ → ℕ → Lean.Elab.Term.Quotation.HeadCheck
-- Init.Prelude
/-- `` `hexnum `` is the node kind of hexadecimal numbers like `ea10`
without the `0x` prefix. Recall that `hexnum` is not a token and must be prefixed.
For hexadecimal number literals, you should use `num` instead.
Example: `syntax anchor := "#" noWs hexnum`.
  -/
Lean.hexnumKind : Lean.SyntaxNodeKind
-- Mathlib.CategoryTheory.Limits.Shapes.Pullback.IsPullback.Basic
CategoryTheory.IsPushout.of_iso : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {Z X Y P : C} {f : Z ⟶ X} {g : Z ⟶ Y} {inl : X ⟶ P}
  {inr : Y ⟶ P},
  CategoryTheory.IsPushout f g inl inr →
    ∀ {Z' X' Y' P' : C} {f' : Z' ⟶ X'} {g' : Z' ⟶ Y'} {inl' : X' ⟶ P'} {inr' : Y' ⟶ P'} (e₁ : Z ≅ Z') (e₂ : X ≅ X')
      (e₃ : Y ≅ Y') (e₄ : P ≅ P'),
      CategoryTheory.CategoryStruct.comp f e₂.hom = CategoryTheory.CategoryStruct.comp e₁.hom f' →
        CategoryTheory.CategoryStruct.comp g e₃.hom = CategoryTheory.CategoryStruct.comp e₁.hom g' →
          CategoryTheory.CategoryStruct.comp inl e₄.hom = CategoryTheory.CategoryStruct.comp e₂.hom inl' →
            CategoryTheory.CategoryStruct.comp inr e₄.hom = CategoryTheory.CategoryStruct.comp e₃.hom inr' →
              CategoryTheory.IsPushout f' g' inl' inr'
-- Mathlib.Data.Num.ZNum
PosNum.cast_to_znum : ∀ (n : PosNum), ↑n = ZNum.pos n
-- Mathlib.Order.Category.Semilat
SemilatSupCat.instConcreteCategorySupBotHomX : CategoryTheory.ConcreteCategory SemilatSupCat fun x1 x2 => SupBotHom x1.X x2.X
-- Mathlib.MeasureTheory.Measure.Typeclasses.SFinite
/-- If a set `t` is covered by a countable family of finite measure sets, then its measurable
superset `toMeasurable μ t` (which has the same measure as `t`) satisfies,
for any measurable set `s`, the equality `μ (toMeasurable μ t ∩ s) = μ (t ∩ s)`.  -/
MeasureTheory.Measure.measure_toMeasurable_inter_of_cover : ∀ {α : Type u_1} {m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} {s : Set α},
  MeasurableSet s →
    ∀ {t : Set α} {v : ℕ → Set α},
      t ⊆ ⋃ n, v n → (∀ (n : ℕ), μ (t ∩ v n) ≠ ⊤) → μ (MeasureTheory.toMeasurable μ t ∩ s) = μ (t ∩ s)
-- Mathlib.CategoryTheory.Localization.CalculusOfFractions
CategoryTheory.MorphismProperty.LeftFraction.Localization.Q_obj : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] (W : CategoryTheory.MorphismProperty C)
  [inst_1 : W.HasLeftCalculusOfFractions] (X : C),
  (CategoryTheory.MorphismProperty.LeftFraction.Localization.Q W).obj X = X
-- Mathlib.RepresentationTheory.Equiv
Representation.diagonalOneEquivLeftRegular_apply_single : ∀ {k : Type u} [inst : Semiring k] {G : Type v} [inst_1 : Monoid G] (f : Fin 1 → G) (r : k),
  (Representation.diagonalOneEquivLeftRegular k G) (MonoidAlgebra.single f r) = MonoidAlgebra.single (f 0) r
-- Mathlib.RingTheory.UniqueFactorizationDomain.Basic
UniqueFactorizationMonoid.factors_pos : ∀ {α : Type u_1} [inst : CommMonoidWithZero α] [inst_1 : UniqueFactorizationMonoid α] {x : α},
  x ≠ 0 → (0 < UniqueFactorizationMonoid.factors x ↔ ¬IsUnit x)
-- Mathlib.CategoryTheory.Sites.DenseSubsite.Basic
CategoryTheory.Functor.IsCoverDense.Types.naturality_assoc : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] {D : Type u_2}
  [inst_1 : CategoryTheory.Category.{v_2, u_2} D] {K : CategoryTheory.GrothendieckTopology D}
  {G : CategoryTheory.Functor C D} {ℱ : CategoryTheory.Functor Dᵒᵖ (Type v)} {ℱ' : CategoryTheory.Sheaf K (Type v)}
  (α : G.op.comp ℱ ⟶ G.op.comp ℱ'.obj) [G.IsLocallyFull K] {X Y : C} (i : G.obj X ⟶ G.obj Y) {Z : Type v}
  (h : ℱ'.obj.obj (Opposite.op (G.obj X)) ⟶ Z),
  CategoryTheory.CategoryStruct.comp (α.app (Opposite.op Y)) (CategoryTheory.CategoryStruct.comp (ℱ'.obj.map i.op) h) =
    CategoryTheory.CategoryStruct.comp (ℱ.map i.op) (CategoryTheory.CategoryStruct.comp (α.app (Opposite.op X)) h)
-- Init.Data.Iterators.Consumers.Monadic.Loop
Std.IteratorLoop.wellFounded_of_finite : ∀ {m : Type w → Type w'} {α β : Type w} {γ : Type x} [inst : Std.Iterator α m β] [Std.Iterators.Finite α m]
  {P : β → γ → ForInStep γ → Prop}, Std.IteratorLoop.WellFounded α m P
-- Mathlib.RingTheory.RingHom.Unramified
RingHom.FormallyUnramified.eq_1 : ∀ {R : Type u_1} {S : Type u_2} [inst : CommRing R] [inst_1 : CommRing S] (f : R →+* S),
  f.FormallyUnramified = Algebra.FormallyUnramified R S
-- Init.Data.Iterators.Combinators.Monadic.ULift
/-- Transforms an `m`-monadic iterator with values in `β` into an `n`-monadic iterator with
values in `ULift β`. Requires a `MonadLift m (ULiftT n)` instance.

**Marble diagram:**

```
it            ---a    ----b    ---c    --d    ---⊥
it.uLift n    ---.up a----.up b---.up c--.up d---⊥
```

**Termination properties:**

* `Finite`: only if the original iterator is finite
* `Productive`: only if the original iterator is productive
 -/
Std.IterM.uLift : {α β : Type u} →
  {m : Type u → Type u'} →
    Std.IterM m β →
      (n : Type (max u v) → Type v') → [lift : MonadLiftT m (Std.Iterators.ULiftT n)] → Std.IterM n (ULift.{v, u} β)
-- Std.Data.ExtDTreeMap.Lemmas
Std.ExtDTreeMap.insertIfNew_ne_empty : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t : Std.ExtDTreeMap α β cmp} [inst : Std.TransCmp cmp] {k : α}
  {v : β k}, t.insertIfNew k v ≠ ∅
-- Mathlib.AlgebraicGeometry.OpenImmersion
AlgebraicGeometry.IsOpenImmersion.comp_lift_assoc : ∀ {X Y Z : AlgebraicGeometry.Scheme} (f : X ⟶ Z) (g : Y ⟶ Z) [H : AlgebraicGeometry.IsOpenImmersion f]
  {Y' : AlgebraicGeometry.Scheme} (g' : Y' ⟶ Y) (H_1 : Set.range ⇑g ⊆ Set.range ⇑f) {Z_1 : AlgebraicGeometry.Scheme}
  (h : X ⟶ Z_1),
  CategoryTheory.CategoryStruct.comp g'
      (CategoryTheory.CategoryStruct.comp (AlgebraicGeometry.IsOpenImmersion.lift f g H_1) h) =
    CategoryTheory.CategoryStruct.comp
      (AlgebraicGeometry.IsOpenImmersion.lift f (CategoryTheory.CategoryStruct.comp g' g) ⋯) h
-- Mathlib.CategoryTheory.Limits.Preserves.Finite
CategoryTheory.Limits.instReflectsColimitsOfShapeDiscreteOfReflectsFiniteCoproductsOfFinite : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  (F : CategoryTheory.Functor C D) [CategoryTheory.Limits.ReflectsFiniteCoproducts F] (J : Type u) [Finite J],
  CategoryTheory.Limits.ReflectsColimitsOfShape (CategoryTheory.Discrete J) F
-- Mathlib.MeasureTheory.SetSemiring
MeasureTheory.IsSetSemiring.sdiff_mem_supClosure : ∀ {α : Type u_1} {C : Set (Set α)} {s t : Set α}, MeasureTheory.IsSetSemiring C → s ∈ C → t ∈ C → s \ t ∈ supClosure C
-- Mathlib.Order.SuccPred.Limit
Order.not_isPredPrelimit_pred_of_not_isMin : ∀ {α : Type u_1} {a : α} [inst : Preorder α] [inst_1 : PredOrder α], ¬IsMin a → ¬Order.IsPredPrelimit (Order.pred a)
-- Init.Data.Iterators.Lemmas.Combinators.ULift
_private.Init.Data.Iterators.Lemmas.Combinators.ULift.0.Std.Iter.step_uLift.match_1.eq_1 : ∀ {α β : Type u_1} [inst : Std.Iterator α Id β] {it : Std.Iter β} (motive : it.Step → Sort u_2) (it' : Std.Iter β)
  (out : β) (h : it.IsPlausibleStep (Std.IterStep.yield it' out))
  (h_1 :
    (it' : Std.Iter β) →
      (out : β) → (h : it.IsPlausibleStep (Std.IterStep.yield it' out)) → motive ⟨Std.IterStep.yield it' out, h⟩)
  (h_2 : (it' : Std.Iter β) → (h : it.IsPlausibleStep (Std.IterStep.skip it')) → motive ⟨Std.IterStep.skip it', h⟩)
  (h_3 : (h : it.IsPlausibleStep Std.IterStep.done) → motive ⟨Std.IterStep.done, h⟩),
  (match ⟨Std.IterStep.yield it' out, h⟩ with
    | ⟨Std.IterStep.yield it' out, h⟩ => h_1 it' out h
    | ⟨Std.IterStep.skip it', h⟩ => h_2 it' h
    | ⟨Std.IterStep.done, h⟩ => h_3 h) =
    h_1 it' out h
-- Mathlib.Order.ConditionallyCompleteLattice.Basic
WithBot.sInf_singleton_bot : ∀ {α : Type u_1} [inst : LE α] [inst_1 : InfSet α], sInf {⊥} = ⊥
-- Mathlib.CategoryTheory.Presentable.Limits
CategoryTheory.Functor.Accessible.Limits.isColimitMapCocone.surjective : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {K : Type u'} [inst_1 : CategoryTheory.Category.{v', u'} K]
  {F : CategoryTheory.Functor K (CategoryTheory.Functor C (Type w'))} (c : CategoryTheory.Limits.Cone F)
  (hc : (Y : C) → CategoryTheory.Limits.IsLimit (((CategoryTheory.evaluation C (Type w')).obj Y).mapCone c))
  (κ : Cardinal.{w}) [inst_2 : Fact κ.IsRegular],
  HasCardinalLT (CategoryTheory.Arrow K) κ →
    ∀ {J : Type w} [inst_3 : CategoryTheory.SmallCategory J] [CategoryTheory.IsCardinalFiltered J κ]
      {X : CategoryTheory.Functor J C} (cX : CategoryTheory.Limits.Cocone X)
      (hF : (k : K) → CategoryTheory.Limits.IsColimit ((F.obj k).mapCocone cX)) (x : c.pt.obj cX.pt),
      ∃ j x', x = (CategoryTheory.ConcreteCategory.hom ((c.pt.mapCocone cX).ι.app j)) x'
-- Std.Sat.AIG.RelabelNat
_private.Std.Sat.AIG.RelabelNat.0.Std.Sat.AIG.relabelNat'.match_1.eq_2 : ∀ (motive : Option ℕ → Sort u_1) (h_1 : (var : ℕ) → motive (some var)) (h_2 : Unit → motive none),
  (match none with
    | some var => h_1 var
    | none => h_2 ()) =
    h_2 ()
-- Mathlib.CategoryTheory.Adjunction.FullyFaithful
CategoryTheory.Adjunction.isIso_unit_app_of_iso : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  {L : CategoryTheory.Functor C D} {R : CategoryTheory.Functor D C} (h : L ⊣ R) [R.Faithful] [R.Full] {X : D} {Y : C}
  (e : Y ≅ R.obj X), CategoryTheory.IsIso (h.unit.app Y)
-- Mathlib.CategoryTheory.Limits.Constructions.EventuallyConstant
/-- Auxiliary definition for `IsEventuallyConstantTo.cone`.  -/
CategoryTheory.Functor.IsEventuallyConstantTo.coneπApp : {J : Type u_1} →
  {C : Type u_2} →
    [inst : CategoryTheory.Category.{v_1, u_1} J] →
      [inst_1 : CategoryTheory.Category.{v_2, u_2} C] →
        {F : CategoryTheory.Functor J C} →
          {i₀ : J} → F.IsEventuallyConstantTo i₀ → [CategoryTheory.IsCofiltered J] → (j : J) → F.obj i₀ ⟶ F.obj j
-- Mathlib.GroupTheory.SemidirectProduct
SemidirectProduct.right_inr : ∀ {N : Type u_1} {G : Type u_2} [inst : Group N] [inst_1 : Group G] {φ : G →* MulAut N} (g : G),
  (SemidirectProduct.inr g).right = g
-- Init.Grind.Ring.CommSolver
Lean.Grind.CommRing.Expr.num.injEq : ∀ (k k_1 : ℤ), (Lean.Grind.CommRing.Expr.num k = Lean.Grind.CommRing.Expr.num k_1) = (k = k_1)
-- Mathlib.Algebra.MvPolynomial.Eval
MvPolynomial.eval₂_mul : ∀ {R : Type u} {S₁ : Type v} {σ : Type u_1} [inst : CommSemiring R] [inst_1 : CommSemiring S₁] {q : MvPolynomial σ R}
  (f : R →+* S₁) (g : σ → S₁) {p : MvPolynomial σ R},
  MvPolynomial.eval₂ f g (p * q) = MvPolynomial.eval₂ f g p * MvPolynomial.eval₂ f g q
-- Mathlib.Topology.Algebra.Module.ContinuousLinearMap.Restrict
Submodule.coe_subtypeL : ∀ {R : Type u_1} [inst : Semiring R] {M : Type u_2} [inst_1 : TopologicalSpace M] [inst_2 : AddCommMonoid M]
  [inst_3 : Module R M] (p : Submodule R M), ⇑p.subtypeL = ⇑p.subtype
-- Mathlib.Topology.Algebra.Group.OpenMapping
/-- Consider a sigma-compact additive group acting continuously and transitively on a
Baire space. Then the orbit map is open. This is a version of the open mapping theorem, valid
notably for the action of a sigma-compact locally compact group on a locally compact space.  -/
isOpenMap_vadd_of_sigmaCompact : ∀ {G : Type u_1} {X : Type u_2} [inst : TopologicalSpace G] [inst_1 : TopologicalSpace X] [inst_2 : AddGroup G]
  [IsTopologicalAddGroup G] [inst_4 : AddAction G X] [SigmaCompactSpace G] [BaireSpace X] [T2Space X]
  [ContinuousVAdd G X] [AddAction.IsPretransitive G X] (x : X), IsOpenMap fun g => g +ᵥ x
-- Mathlib.CategoryTheory.Monoidal.Free.Basic
CategoryTheory.FreeMonoidalCategory.mk_ρ_hom : ∀ {C : Type u} {X : CategoryTheory.FreeMonoidalCategory C},
  ⟦CategoryTheory.FreeMonoidalCategory.Hom.ρ_hom X⟧ = (CategoryTheory.MonoidalCategoryStruct.rightUnitor X).hom
-- Mathlib.Topology.NhdsSet
nhdsSet_iInter_le : ∀ {X : Type u_2} [inst : TopologicalSpace X] {ι : Sort u_4} (s : ι → Set X), nhdsSet (⋂ i, s i) ≤ ⨅ i, nhdsSet (s i)
-- Mathlib.CategoryTheory.Limits.Shapes.WideEqualizers
/-- A category `HasWideCoequalizers` if it has all colimits of shape `WalkingParallelFamily J`, i.e.
if it has a wide coequalizer for every family of parallel morphisms.  -/
CategoryTheory.Limits.HasWideCoequalizers : (C : Type u) → [CategoryTheory.Category.{v, u} C] → Prop
-- Mathlib.RingTheory.Ideal.Quotient.Operations
/-- The homomorphism from `R/(⋂ i, f i)` to `∏ i, (R / f i)` featured in the Chinese
Remainder Theorem. It is bijective if the ideals `f i` are coprime.  -/
Ideal.quotientInfToPiQuotient : {R : Type u} →
  [inst : Ring R] →
    {ι : Type u_1} → (I : ι → Ideal R) → [inst_1 : ∀ (i : ι), (I i).IsTwoSided] → R ⧸ ⨅ i, I i →+* (i : ι) → R ⧸ I i
-- Mathlib.AlgebraicTopology.SimplicialSet.AnodyneExtensions.UnionProd
/-- A weak rank function for `pairingCore k n`.  -/
SSet.prodStdSimplex.weakRankFunction : {m : ℕ} → (k : Fin (m + 1)) → (n : ℕ) → (SSet.prodStdSimplex.pairingCore k n).WeakRankFunction ℕ
-- Mathlib.Order.Shrink
orderIsoShrink_apply : ∀ {α : Type u_1} [inst : Small.{u, u_1} α] [inst_1 : Preorder α] (a : α), (orderIsoShrink α) a = (equivShrink α) a
-- Init.Data.SInt.Bitwise
Int16.toInt32_xor : ∀ (a b : Int16), (a ^^^ b).toInt32 = a.toInt32 ^^^ b.toInt32
-- Mathlib.Algebra.Category.CommBialgCat
CommBialgCat.isoMk_hom : ∀ {R : Type u} [inst : CommRing R] {X Y : Type v} {x : CommRing X} {x_1 : CommRing Y} {x_2 : Bialgebra R X}
  {x_3 : Bialgebra R Y} (e : X ≃ₐc[R] Y), (CommBialgCat.isoMk e).hom = CommBialgCat.ofHom ↑e
-- Mathlib.NumberTheory.NumberField.Completion.FinitePlace
/-- The embedding of a field inside its `adicCompletion` with respect to `v`.  -/
NumberField.FinitePlace.embedding : {K : Type u_1} →
  [inst : Field K] →
    {R : Type u_2} →
      [inst_1 : CommRing R] →
        [inst_2 : Algebra R K] →
          [inst_3 : IsDedekindDomain R] →
            [inst_4 : IsFractionRing R K] →
              (v : IsDedekindDomain.HeightOneSpectrum R) → K →+* IsDedekindDomain.HeightOneSpectrum.adicCompletion K v
-- Init.Data.Int.Order
Int.le_of_lt_add_one : ∀ {a b : ℤ}, a < b + 1 → a ≤ b
-- Std.Data.ExtDTreeMap.Basic
/-- Tries to retrieve the key-value pair with the smallest key in the tree map, returning `fallback` if
the tree map is empty.
 -/
Std.ExtDTreeMap.minEntryD : {α : Type u} →
  {β : α → Type v} →
    {cmp : α → α → Ordering} → [Std.TransCmp cmp] → Std.ExtDTreeMap α β cmp → (a : α) × β a → (a : α) × β a
-- Mathlib.SetTheory.Cardinal.Basic
Cardinal.small_Ioc : ∀ (a b : Cardinal.{u}), Small.{u, u + 1} ↑(Set.Ioc a b)
-- Mathlib.LinearAlgebra.Matrix.NonsingularInverse
Matrix.inv_inj : ∀ {n : Type u'} {α : Type v} [inst : Fintype n] [inst_1 : DecidableEq n] [inst_2 : CommRing α] {A B : Matrix n n α},
  A⁻¹ = B⁻¹ → IsUnit A.det → A = B
-- Mathlib.RepresentationTheory.Homological.GroupHomology.LowDegree
/-- The 2-cycles of the complex of inhomogeneous chains of `A` are isomorphic to
`cycles₂ A`, which is a simpler type.  -/
groupHomology.isoCycles₂ : {k G : Type u} →
  [inst : CommRing k] →
    [inst_1 : Group G] → (A : Rep.{u, u, u} k G) → groupHomology.cycles A 2 ≅ ModuleCat.of k ↥(groupHomology.cycles₂ A)
-- Mathlib.Order.Interval.Set.LinearOrder
Set.Ici_sdiff_Ioi : ∀ {α : Type u_1} [inst : LinearOrder α] {a b : α}, Set.Ici a \ Set.Ioi b = Set.Icc a b
-- Mathlib.NumberTheory.RamificationInertia.Basic
Ideal.Quotient.algebraMap_quotient_pow_ramificationIdx : ∀ {R : Type u} [inst : CommRing R] {S : Type v} [inst_1 : CommRing S] [inst_2 : Algebra R S] (p : Ideal R) (P : Ideal S)
  (x : R),
  (algebraMap (R ⧸ p) (S ⧸ P ^ p.ramificationIdx' P)) ((Ideal.Quotient.mk p) x) =
    (Ideal.Quotient.mk (P ^ p.ramificationIdx' P)) ((algebraMap R S) x)
-- Lean.Syntax
Lean.Syntax.isAntiquot : Lean.Syntax → Bool
-- Mathlib.Data.Multiset.Lattice
/-- Infimum of a multiset: `inf {a, b, c} = a ⊓ b ⊓ c`  -/
Multiset.inf : {α : Type u_1} → [inst : SemilatticeInf α] → [OrderTop α] → Multiset α → α
-- Mathlib.Topology.ContinuousOn
antitone_continuousOn : ∀ {α : Type u_1} {β : Type u_2} [inst : TopologicalSpace α] [inst_1 : TopologicalSpace β] {f : α → β},
  Antitone (ContinuousOn f)
-- Mathlib.Topology.Algebra.Module.ModuleTopology
/-- The product of the module topologies for two modules over a topological ring
is the module topology.  -/
IsModuleTopology.instProd : ∀ {R : Type u_1} [inst : TopologicalSpace R] [inst_1 : Semiring R] {M : Type u_2} [inst_2 : AddCommMonoid M]
  [inst_3 : Module R M] [inst_4 : TopologicalSpace M] [IsModuleTopology R M] {N : Type u_3} [inst_6 : AddCommMonoid N]
  [inst_7 : Module R N] [inst_8 : TopologicalSpace N] [IsModuleTopology R N], IsModuleTopology R (M × N)
-- Mathlib.Analysis.Fourier.FiniteAbelian.PontryaginDuality
AddChar.expect_apply_eq_zero_iff_ne_zero : ∀ {α : Type u_1} [inst : AddCommGroup α] {a : α} [inst_1 : Finite α], (Finset.univ.expect fun ψ => ψ a) = 0 ↔ a ≠ 0