mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.MeasureTheory.Group.FundamentalDomain
MeasureTheory.IsAddFundamentalDomain.measure_zero_of_invariant : ∀ {G : Type u_1} {α : Type u_3} [inst : AddGroup G] [inst_1 : AddAction G α] [inst_2 : MeasurableSpace α] {s : Set α}
  {μ : MeasureTheory.Measure α} [MeasurableConstVAdd G α] [MeasureTheory.VAddInvariantMeasure G α μ] [Countable G],
  MeasureTheory.IsAddFundamentalDomain G s μ → ∀ (t : Set α), (∀ (g : G), g +ᵥ t = t) → μ (t ∩ s) = 0 → μ t = 0
-- Init.Data.List.Find
List.findSome?_isSome_iff : ∀ {α : Type u_1} {β : Type u_2} {f : α → Option β} {l : List α},
  (List.findSome? f l).isSome = true ↔ ∃ x ∈ l, (f x).isSome = true
-- Init.Data.Int.Order
Int.sign.eq_3 : ∀ (a : ℕ), (Int.negSucc a).sign = -1
-- Mathlib.Data.Set.Sigma
Sigma.mk.hcongr_4 : ∀ (α α' : Type u),
  α = α' →
    ∀ (β : α → Type v) (β' : α' → Type v),
      β ≍ β' →
        ∀ (fst : α) (fst' : α'), fst ≍ fst' → ∀ (snd : β fst) (snd' : β' fst'), snd ≍ snd' → ⟨fst, snd⟩ ≍ ⟨fst', snd'⟩
-- Mathlib.CategoryTheory.Monoidal.Cartesian.Grp
/-- If `G` is an additive group object, then `Hom(X, G)` has an additive group structure.  -/
CategoryTheory.Hom.addGroup : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    [inst_1 : CategoryTheory.CartesianMonoidalCategory C] → {G X : C} → [CategoryTheory.AddGrpObj G] → AddGroup (X ⟶ G)
-- Mathlib.Control.Traversable.Instances
Sum.comp_traverse : ∀ {σ : Type u} {F G : Type u → Type u} [inst : Applicative F] [inst_1 : Applicative G] [LawfulApplicative G]
  {α β γ : Type u} (f : β → F γ) (g : α → G β) (x : σ ⊕ α),
  Sum.traverse (Functor.Comp.mk ∘ (fun x => f <$> x) ∘ g) x = Functor.Comp.mk (Sum.traverse f <$> Sum.traverse g x)
-- Lean.Parser.Types
/-- Return character after position `pos`  -/
Lean.Parser.getNext : String → String.Pos.Raw → Char
-- Lean.Elab.Binders
Lean.Elab.Term.LetIdDeclView.mk.inj : ∀ {id : Lean.Syntax} {binders : Array Lean.Syntax} {type value id_1 : Lean.Syntax} {binders_1 : Array Lean.Syntax}
  {type_1 value_1 : Lean.Syntax},
  { id := id, binders := binders, type := type, value := value } =
      { id := id_1, binders := binders_1, type := type_1, value := value_1 } →
    id = id_1 ∧ binders = binders_1 ∧ type = type_1 ∧ value = value_1
-- Init.Data.Int.DivMod.Lemmas
Int.fmod_sub_cancel_left : ∀ {m n k : ℤ} (i : ℤ), (i - m).fmod n = (i - k).fmod n ↔ m.fmod n = k.fmod n
-- Mathlib.CategoryTheory.Limits.Shapes.Countable
CategoryTheory.Limits.IsCofiltered.sequentialFunctor_initial_aux : ∀ (J : Type u_2) [inst : Countable J] [inst_1 : Preorder J] [inst_2 : CategoryTheory.IsCofiltered J] (j : J),
  ∃ n, CategoryTheory.Limits.IsCofiltered.sequentialFunctor_obj J n ≤ j
-- Mathlib.CategoryTheory.GlueData
/-- Objects representing the intersections.  -/
CategoryTheory.GlueData'.V : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v, u₁} C] → (self : CategoryTheory.GlueData' C) → (i j : self.J) → i ≠ j → C
-- Mathlib.Algebra.Group.Subgroup.Lattice
AddSubgroup.disjoint_def : ∀ {G : Type u_1} [inst : AddGroup G] {H₁ H₂ : AddSubgroup G}, Disjoint H₁ H₂ ↔ ∀ {x : G}, x ∈ H₁ → x ∈ H₂ → x = 0
-- Mathlib.Algebra.GCDMonoid.Basic
gcd_one_left : ∀ {α : Type u_1} [inst : CommMonoidWithZero α] [inst_1 : NormalizedGCDMonoid α] (a : α), gcd 1 a = 1
-- Mathlib.Order.Lattice
/-- The supremum is an upper bound on the first argument  -/
SemilatticeSup.le_sup_left : ∀ {α : Type u} [self : SemilatticeSup α] (a b : α), a ≤ SemilatticeSup.sup a b
-- Mathlib.RingTheory.NonUnitalSubsemiring.Basic
NonUnitalSubsemiring.eq_top_iff' : ∀ {R : Type u} [inst : NonUnitalNonAssocSemiring R] (A : NonUnitalSubsemiring R), A = ⊤ ↔ ∀ (x : R), x ∈ A
-- Mathlib.Data.Real.Basic
_private.Mathlib.Data.Real.Basic.0.Real.add : ℝ → ℝ → ℝ
-- Mathlib.NumberTheory.Harmonic.ZetaAsymp
log_deriv_riemannZeta_eq_neg_inv_sub_add : ∀ᶠ (s : ℂ) in nhdsWithin 1 {1}ᶜ,
  deriv riemannZeta s / riemannZeta s = -(s - 1)⁻¹ + deriv riemannZeta₁ s / riemannZeta₁ s
-- Mathlib.RingTheory.PolynomialLaw.Basic
PolynomialLaw.instZero : {R : Type u} →
  [inst : CommSemiring R] →
    {M : Type u_1} →
      [inst_1 : AddCommMonoid M] →
        [inst_2 : Module R M] → {N : Type u_2} → [inst_3 : AddCommMonoid N] → [inst_4 : Module R N] → Zero (M →ₚₗ[R] N)
-- Mathlib.NumberTheory.Modular
_private.Mathlib.NumberTheory.Modular.0.ModularGroup.serreTheorem_im_eq : ∀ {g : Matrix.SpecialLinearGroup (Fin 2) ℤ} {z : UpperHalfPlane},
  z ∈ ModularGroup.fd → g • z ∈ ModularGroup.fd → (g • z).im = z.im
-- Mathlib.Order.Interval.Finset.Fin
Fin.finsetImage_castSucc_Ioi : ∀ {n : ℕ} (i : Fin n), Finset.image Fin.castSucc (Finset.Ioi i) = Finset.Ioo i.castSucc (Fin.last n)
-- Mathlib.Order.Lex
/-- `toColex` is the identity function to the `Colex` of a type.  -/
toColex : {α : Type u_1} → α ≃ Colex α
-- Mathlib.Tactic.Linter.TextBased.UnicodeLinter
/-- Prints a unicode character's codepoint in hexadecimal with prefix 'U+'.
E.g., 'a' is "U+0061".  -/
Mathlib.Linter.TextBased.UnicodeLinter.Char.printCodepointHex : Char → String
-- Mathlib.FieldTheory.IntermediateField.Basic
IntermediateField.inclusion_injective : ∀ {K : Type u_1} {L : Type u_2} [inst : Field K] [inst_1 : Field L] [inst_2 : Algebra K L] {E F : IntermediateField K L}
  (hEF : E ≤ F), Function.Injective ⇑(IntermediateField.inclusion hEF)
-- Mathlib.Topology.Algebra.MulAction
Filter.Tendsto.zero_vadd_const : ∀ {M : Type u_1} {X : Type u_2} {α : Type u_4} [inst : TopologicalSpace M] [inst_1 : TopologicalSpace X]
  [inst_2 : AddMonoid M] [inst_3 : AddAction M X] [ContinuousVAdd M X] {f : α → M} {l : Filter α},
  Filter.Tendsto f l (nhds 0) → ∀ (a : X), Filter.Tendsto (fun x => f x +ᵥ a) l (nhds a)
-- Init.Prelude
/-- The read-only context for the `MacroM` monad.  -/
Lean.Macro.Context : Type
-- Mathlib.Algebra.Star.SelfAdjoint
IsSelfAdjoint.add_star_self : ∀ {R : Type u_1} [inst : AddCommMonoid R] [inst_1 : StarAddMonoid R] (x : R), IsSelfAdjoint (x + star x)
-- Mathlib.Data.EReal.Basic
/-- **Alias** of the reverse direction of `EReal.coe_lt_coe_iff`. -/
EReal.coe_lt_coe : ∀ {x y : ℝ}, x < y → ↑x < ↑y
-- Std.Data.Iterators.Lemmas.Combinators.Monadic.TakeWhile
_private.Std.Data.Iterators.Lemmas.Combinators.Monadic.TakeWhile.0.Std.IterM.step_takeWhileWithPostcondition.match_1.splitter : {m : Type u_1 → Type u_2} →
  {β : Type u_1} →
    {P : β → Std.Iterators.PostconditionT m (ULift.{u_1, 0} Bool)} →
      (out : β) →
        (motive : Subtype (P out).Property → Sort u_3) →
          (__do_lift : Subtype (P out).Property) →
            ((h' : (P out).Property { down := true }) → motive ⟨{ down := true }, h'⟩) →
              ((h' : (P out).Property { down := false }) → motive ⟨{ down := false }, h'⟩) → motive __do_lift
-- Mathlib.FieldTheory.Finite.Polynomial
MvPolynomial.decidableRestrictDegree : (σ : Type u) → (m : ℕ) → DecidablePred fun x => x ∈ {n | ∀ (i : σ), n i ≤ m}
-- Mathlib.Algebra.Category.MonCat.Basic
AddCommMonCat.instCoeMonCat : Coe AddCommMonCat AddMonCat
-- Mathlib.MeasureTheory.Order.Group.Lattice
AEMeasurable.leOnePart : ∀ {α : Type u_1} {β : Type u_2} [inst : Lattice α] [inst_1 : Group α] [inst_2 : MeasurableSpace α]
  [inst_3 : MeasurableSpace β] {f : β → α} [MeasurableInv α] {μ : MeasureTheory.Measure β} [MeasurableSup α],
  AEMeasurable f μ → AEMeasurable (fun x => (f x)⁻ᵐ) μ
-- Mathlib.Data.Rel.Cover
SetRel.IsCover.mono_entourage : ∀ {X : Type u_1} {U V : SetRel X X} {s N : Set X}, U ⊆ V → U.IsCover s N → V.IsCover s N
-- Mathlib.Tactic.ComputeAsymptotics.Multiseries.Basis
Tactic.ComputeAsymptotics.WellFormedBasis.eq_1 : ∀ (basis : Tactic.ComputeAsymptotics.Basis),
  Tactic.ComputeAsymptotics.WellFormedBasis basis =
    (List.Pairwise (fun x y => (Real.log ∘ y) =o[Filter.atTop] (Real.log ∘ x)) basis ∧
      ∀ f ∈ basis, Filter.Tendsto f Filter.atTop Filter.atTop)
-- Mathlib.MeasureTheory.VectorMeasure.WithDensityVec
MeasureTheory.VectorMeasure.withDensity.eq_1 : ∀ {X : Type u_1} {E : Type u_2} {F : Type u_3} {G : Type u_4} {mX : MeasurableSpace X} [inst : NormedAddCommGroup E]
  [inst_1 : NormedSpace ℝ E] [inst_2 : NormedAddCommGroup F] [inst_3 : NormedSpace ℝ F] [inst_4 : NormedAddCommGroup G]
  [inst_5 : NormedSpace ℝ G] (μ : MeasureTheory.VectorMeasure X F) (f : X → E) (B : E →L[ℝ] F →L[ℝ] G),
  μ.withDensity f B =
    if h : μ.Integrable f then
      { measureOf' := fun s => ∫ᵛ (x : X) in s, f x ∂[B; μ], empty' := ⋯, not_measurable' := ⋯, m_iUnion' := ⋯ }
    else 0
-- Mathlib.RingTheory.PowerSeries.Basic
/-- The ring homomorphism taking a power series `f(X)` to `f(-X)`.  -/
PowerSeries.evalNegHom : {A : Type u_2} → [inst : CommRing A] → PowerSeries A →+* PowerSeries A
-- Mathlib.Algebra.Group.Indicator
Set.mulIndicator_self_mul_compl_apply : ∀ {α : Type u_1} {M : Type u_4} [inst : MulOneClass M] (s : Set α) (f : α → M) (a : α),
  s.mulIndicator f a * sᶜ.mulIndicator f a = f a
-- Init.PropLemmas
exists₅_congr : ∀ {α : Sort u_1} {β : α → Sort u_2} {γ : (a : α) → β a → Sort u_3} {δ : (a : α) → (b : β a) → γ a b → Sort u_4}
  {ε : (a : α) → (b : β a) → (c : γ a b) → δ a b c → Sort u_5}
  {p q : (a : α) → (b : β a) → (c : γ a b) → (d : δ a b c) → ε a b c d → Prop},
  (∀ (a : α) (b : β a) (c : γ a b) (d : δ a b c) (e : ε a b c d), p a b c d e ↔ q a b c d e) →
    ((∃ a b c d e, p a b c d e) ↔ ∃ a b c d e, q a b c d e)
-- Std.Data.DHashMap.RawLemmas
Std.DHashMap.Raw.isEmpty_iff_forall_not_mem : ∀ {α : Type u} {β : α → Type v} {m : Std.DHashMap.Raw α β} [inst : BEq α] [inst_1 : Hashable α] [EquivBEq α]
  [LawfulHashable α], m.WF → (m.isEmpty = true ↔ ∀ (a : α), a ∉ m)
-- Std.Sat.CNF.Relabel
Std.Sat.CNF.Clause.relabel_nil : ∀ {α : Type u_1} {β : Type u_2} (r : α → β), Std.Sat.CNF.Clause.relabel r [] = []
-- Mathlib.Algebra.Category.ModuleCat.Semi
SemimoduleCat.Hom.hom₂_apply : ∀ {R : Type u_1} [inst : CommSemiring R] {M N P : SemimoduleCat R} (f : M ⟶ SemimoduleCat.of R (N ⟶ P)) (x : ↑M),
  (SemimoduleCat.Hom.hom₂ f) x = (SemimoduleCat.ofHom ↑SemimoduleCat.homLinearEquiv).hom' (f.hom' x)
-- Mathlib.Topology.ContinuousMap.CompactlySupported
CompactlySupportedContinuousMap.finsetInf'_apply : ∀ {α : Type u_2} {β : Type u_3} [inst : TopologicalSpace α] [inst_1 : SemilatticeInf β] [inst_2 : Zero β]
  [inst_3 : TopologicalSpace β] [inst_4 : ContinuousInf β] {ι : Type u_5} {s : Finset ι} (H : s.Nonempty)
  (f : ι → CompactlySupportedContinuousMap α β) (a : α), (s.inf' H f) a = s.inf' H fun i => (f i) a
-- Mathlib.Topology.Algebra.Group.GroupTopology
AddGroupTopology.instInfSet.eq_1 : ∀ {α : Type u} [inst : AddGroup α],
  AddGroupTopology.instInfSet =
    {
      sInf := fun S =>
        { toTopologicalSpace := sInf (AddGroupTopology.toTopologicalSpace '' S), toIsTopologicalAddGroup := ⋯ } }
-- Mathlib.AlgebraicGeometry.Birational.Birational
AlgebraicGeometry.Scheme.PartialIso.restrictTarget_iso : ∀ {X Y : AlgebraicGeometry.Scheme} (f : X.PartialIso Y) (U : Y.Opens) (hU : Dense ↑U) (hU' : U ≤ f.target),
  (f.restrictTarget U hU hU').iso = (f.symm.restrictSource U hU hU').iso.symm
-- Std.Data.TreeMap.Raw.Lemmas
Std.TreeMap.Raw.ordCompare_maxKey!_modify_eq : ∀ {α : Type u} {β : Type v} [inst : Ord α] [Std.TransOrd α] {t : Std.TreeMap.Raw α β compare} [inst_2 : Inhabited α],
  t.WF → ∀ {k : α} {f : β → β}, compare (t.modify k f).maxKey! t.maxKey! = Ordering.eq
-- Init.Data.Int.DivMod.Bootstrap
_private.Init.Data.Int.DivMod.Bootstrap.0.Int.ediv.match_1.eq_1 : ∀ (motive : ℤ → ℤ → Sort u_1) (m n : ℕ) (h_1 : (m n : ℕ) → motive (Int.ofNat m) (Int.ofNat n))
  (h_2 : (m n : ℕ) → motive (Int.ofNat m) (Int.negSucc n)) (h_3 : (a : ℕ) → motive (Int.negSucc a) 0)
  (h_4 : (m n : ℕ) → motive (Int.negSucc m) (Int.ofNat n.succ))
  (h_5 : (m n : ℕ) → motive (Int.negSucc m) (Int.negSucc n)),
  (match Int.ofNat m, Int.ofNat n with
    | Int.ofNat m, Int.ofNat n => h_1 m n
    | Int.ofNat m, Int.negSucc n => h_2 m n
    | Int.negSucc a, 0 => h_3 a
    | Int.negSucc m, Int.ofNat n.succ => h_4 m n
    | Int.negSucc m, Int.negSucc n => h_5 m n) =
    h_1 m n
-- Lean.Data.Lsp.Capabilities
Lean.Lsp.LeanClientCapabilities : Type
-- Mathlib.Data.Set.Prod
Set.prod_eq_prod_iff_of_nonempty : ∀ {α : Type u_1} {β : Type u_2} {s s₁ : Set α} {t t₁ : Set β}, (s ×ˢ t).Nonempty → (s ×ˢ t = s₁ ×ˢ t₁ ↔ s = s₁ ∧ t = t₁)
-- Std.Data.DTreeMap.Internal.WF.Defs
Std.DTreeMap.Internal.Impl.WF.union : ∀ {α : Type u} {β : α → Type v} [inst : Ord α] {t₁ : Std.DTreeMap.Internal.Impl α β} {h₁ : t₁.WF}
  {t₂ : Std.DTreeMap.Internal.Impl α β} {h₂ : t₂.WF}, (t₁.union t₂ ⋯ ⋯).WF
-- Mathlib.FieldTheory.Separable
Polynomial.separable_def : ∀ {R : Type u} [inst : CommSemiring R] (f : Polynomial R), f.Separable ↔ IsCoprime f (Polynomial.derivative f)
-- Mathlib.Algebra.GradedMonoid
One.gOne : (ι : Type u_1) → {R : Type u_2} → [inst : Zero ι] → [One R] → GradedMonoid.GOne fun x => R
-- Mathlib.Algebra.Group.Subgroup.Map
MonoidHom.subgroupComap_surjective_of_surjective : ∀ {G : Type u_1} {G' : Type u_2} [inst : Group G] [inst_1 : Group G'] (f : G →* G') (H' : Subgroup G'),
  Function.Surjective ⇑f → Function.Surjective ⇑(f.subgroupComap H')
-- Mathlib.Algebra.MonoidAlgebra.Defs
AddMonoidAlgebra.zero.eq_1 : ∀ {R : Type u_1} {M : Type u_4} [inst : Semiring R] [inst_1 : Zero M],
  AddMonoidAlgebra.zero = { one := AddMonoidAlgebra.single 0 1 }
-- Lean.Attributes
/-- You can tag attributes with the 'local' or 'scoped' kind.
For example: `attribute [local myattr, scoped yourattr, theirattr]`.

This is used to indicate how an attribute should be scoped.
- local means that the attribute should only be applied in the current scope and forgotten once the current section, namespace, or file is closed.
- scoped means that the attribute should only be applied while the namespace is open.
- global means that the attribute should always be applied.

Note that the attribute handler (`AttributeImpl.add`) is responsible for interpreting the kind and
making sure that these kinds are respected.
 -/
Lean.AttributeKind : Type
-- Std.Data.DHashMap.Lemmas
Std.DHashMap.contains_of_isEmpty : ∀ {α : Type u} {β : α → Type v} {x : BEq α} {x_1 : Hashable α} {m : Std.DHashMap α β} [EquivBEq α] [LawfulHashable α]
  {a : α}, m.isEmpty = true → m.contains a = false
-- Mathlib.Order.CountableSupClosed
CountableSupClosed.isLUB_mem : ∀ {α : Type u_2} [inst : LE α] {s : Set α},
  CountableSupClosed s → ∀ t ⊆ s, t.Nonempty → t.Countable → ∀ (x : α), IsLUB t x → x ∈ s
-- Mathlib.Geometry.Euclidean.Angle.Oriented.Affine
/-- If the angle between three points is `-π / 2`, the first two points are not equal.  -/
EuclideanGeometry.left_ne_of_oangle_eq_neg_pi_div_two : ∀ {V : Type u_1} {P : Type u_2} [inst : NormedAddCommGroup V] [inst_1 : InnerProductSpace ℝ V] [inst_2 : MetricSpace P]
  [inst_3 : NormedAddTorsor V P] [hd2 : Fact (Module.finrank ℝ V = 2)] [inst_4 : Module.Oriented ℝ V (Fin 2)]
  {p₁ p₂ p₃ : P}, EuclideanGeometry.oangle p₁ p₂ p₃ = ↑(-Real.pi / 2) → p₁ ≠ p₂
-- Mathlib.CategoryTheory.Comma.Over.Basic
CategoryTheory.CostructuredArrow.ofCommaFstEquivalenceFunctor_obj_right : ∀ {T : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} T] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  {C : Type u₃} [inst_2 : CategoryTheory.Category.{v₃, u₃} C] (F : CategoryTheory.Functor C T)
  (G : CategoryTheory.Functor D T) (c : C) (X : CategoryTheory.CostructuredArrow (CategoryTheory.Comma.fst F G) c),
  ((CategoryTheory.CostructuredArrow.ofCommaFstEquivalenceFunctor F G c).obj X).right = X.left.right
-- Mathlib.Order.Bounded
Set.bounded_ge_of_bounded_gt : ∀ {α : Type u_1} {s : Set α} [inst : Preorder α],
  Set.Bounded (fun x1 x2 => x1 > x2) s → Set.Bounded (fun x1 x2 => x1 ≥ x2) s
-- Init.Data.String.Iterator
_private.Init.Data.String.Iterator.0.String.Pos.Raw.get?.match_1.splitter : (motive : String → String.Pos.Raw → Sort u_1) →
  (x : String) → (x_1 : String.Pos.Raw) → ((s : String) → (p : String.Pos.Raw) → motive s p) → motive x x_1
-- Mathlib.Order.Hom.WithTopBot
InfHom.withTop_toFun : ∀ {α : Type u_1} {β : Type u_2} [inst : SemilatticeInf α] [inst_1 : SemilatticeInf β] (f : InfHom α β) (a : WithTop α),
  f.withTop a = WithTop.map (⇑f) a
-- Mathlib.CategoryTheory.Localization.Resolution
CategoryTheory.LocalizerMorphism.RightResolution.mk.injEq : ∀ {C₁ : Type u_1} {C₂ : Type u_2} [inst : CategoryTheory.Category.{v_1, u_1} C₁]
  [inst_1 : CategoryTheory.Category.{v_2, u_2} C₂] {W₁ : CategoryTheory.MorphismProperty C₁}
  {W₂ : CategoryTheory.MorphismProperty C₂} {Φ : CategoryTheory.LocalizerMorphism W₁ W₂} {X₂ : C₂} {X₁ : C₁}
  (w : X₂ ⟶ Φ.functor.obj X₁) (hw : W₂ w) (X₁_1 : C₁) (w_1 : X₂ ⟶ Φ.functor.obj X₁_1) (hw_1 : W₂ w_1),
  ({ X₁ := X₁, w := w, hw := hw } = { X₁ := X₁_1, w := w_1, hw := hw_1 }) = (X₁ = X₁_1 ∧ w ≍ w_1)
-- Mathlib.NumberTheory.NumberField.Discriminant.Basic
/-- **Hermite-Minkowski Theorem**. A nontrivial number field has discriminant greater than `2`.  -/
NumberField.abs_discr_gt_two : ∀ {K : Type u_1} [inst : Field K] [inst_1 : NumberField K], 1 < Module.finrank ℚ K → 2 < |NumberField.discr K|
-- Mathlib.CategoryTheory.SmallRepresentatives
/-- Given `h : CoreSmallCategoryOfSet Ω C`, the equivalence of categories
`h.smallCategoryOfSet.obj ≌ C` is actually an isomorphism: it induces
a bijection on the type of arrows.  -/
CategoryTheory.CoreSmallCategoryOfSet.arrowEquiv : {Ω : Type w} →
  {C : Type u} →
    [inst : CategoryTheory.Category.{v, u} C] →
      (h : CategoryTheory.CoreSmallCategoryOfSet Ω C) →
        CategoryTheory.Arrow ↑h.smallCategoryOfSet.obj ≃ CategoryTheory.Arrow C
-- Lean.Meta.Tactic.LibrarySearch
/-- the backward direction of an `iff`  -/
Lean.Meta.LibrarySearch.DeclMod.mpr : Lean.Meta.LibrarySearch.DeclMod
-- Init.Data.UInt.Bitwise
UInt8.neg_one_and : ∀ {a : UInt8}, -1 &&& a = a
-- Mathlib.Order.SuccPred.Basic
Order.Icc_subset_Ioc_pred_left_of_not_isMin : ∀ {α : Type u_1} [inst : Preorder α] [inst_1 : PredOrder α] {a b : α}, ¬IsMin b → Set.Icc b a ⊆ Set.Ioc (Order.pred b) a
-- Mathlib.MeasureTheory.Measure.NullMeasurable
MeasureTheory.Measure.isComplete_iff : ∀ {α : Type u_2} {m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α},
  μ.IsComplete ↔ ∀ (s : Set α), μ s = 0 → MeasurableSet s
-- Mathlib.Algebra.Quaternion
Quaternion.finrank_eq_four : ∀ {R : Type u_3} [inst : CommRing R] [StrongRankCondition R], Module.finrank R (Quaternion R) = 4
-- Mathlib.LinearAlgebra.Span.Defs
/-- In a non-unital algebra, if `x` commutes with every element of a set `s`, then `x` commutes
with every element of `Submodule.span R s`.  -/
Commute.span_right : ∀ {R : Type u_8} {A : Type u_9} [inst : Semiring R] [inst_1 : NonUnitalNonAssocSemiring A] [inst_2 : Module R A]
  [IsScalarTower R A A] [SMulCommClass R A A] {s : Set A} {x : A},
  (∀ y ∈ s, Commute x y) → ∀ y ∈ Submodule.span R s, Commute x y
-- Mathlib.Analysis.Normed.Module.Ball.Action
instSMulCommClass_sphere_closedBall_ball : ∀ {𝕜 : Type u_1} {𝕜' : Type u_2} {E : Type u_3} [inst : NormedField 𝕜] [inst_1 : NormedField 𝕜']
  [inst_2 : SeminormedAddCommGroup E] [inst_3 : NormedSpace 𝕜 E] [inst_4 : NormedSpace 𝕜' E] {r : ℝ}
  [SMulCommClass 𝕜 𝕜' E], SMulCommClass ↑(Metric.sphere 0 1) ↑(Metric.closedBall 0 1) ↑(Metric.ball 0 r)
-- Mathlib.Topology.Algebra.Module.FiniteDimension
LinearEquiv.toLinearEquiv_toContinuousLinearEquiv_symm : ∀ {𝕜 : Type u} [hnorm : NontriviallyNormedField 𝕜] {E : Type v} [inst : AddCommGroup E] [inst_1 : Module 𝕜 E]
  [inst_2 : TopologicalSpace E] [inst_3 : IsTopologicalAddGroup E] [inst_4 : ContinuousSMul 𝕜 E] {F : Type w}
  [inst_5 : AddCommGroup F] [inst_6 : Module 𝕜 F] [inst_7 : TopologicalSpace F] [inst_8 : IsTopologicalAddGroup F]
  [inst_9 : ContinuousSMul 𝕜 F] [inst_10 : CompleteSpace 𝕜] [inst_11 : T2Space E] [inst_12 : T2Space F]
  [inst_13 : FiniteDimensional 𝕜 E] (e : E ≃ₗ[𝕜] F), ↑e.toContinuousLinearEquiv.symm = e.symm
-- Mathlib.Analysis.Calculus.BumpFunction.FiniteDimension
ExistsContDiffBumpBase.u_neg : ∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] [inst_2 : FiniteDimensional ℝ E] (x : E),
  ExistsContDiffBumpBase.u (-x) = ExistsContDiffBumpBase.u x
-- Mathlib.Analysis.Calculus.FDeriv.Symmetric
/-- If a function is analytic within a set at a point, then its second derivative is symmetric.  -/
ContDiffWithinAt.isSymmSndFDerivWithinAt_of_omega : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} {F : Type u_3} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F] {s : Set E} {f : E → F} {x : E},
  ContDiffWithinAt 𝕜 ⊤ f s x → UniqueDiffOn 𝕜 s → x ∈ s → IsSymmSndFDerivWithinAt 𝕜 f s x
-- Mathlib.CategoryTheory.Abelian.Injective.Extend
CategoryTheory.InjectiveResolution.cochainComplex_d : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Limits.HasZeroObject C]
  [inst_2 : CategoryTheory.Preadditive C] {X : C} (R : CategoryTheory.InjectiveResolution X) (n₁ n₂ : ℤ) (k₁ k₂ : ℕ)
  (h₁ : ↑k₁ = n₁) (h₂ : ↑k₂ = n₂),
  R.cochainComplex.d n₁ n₂ =
    CategoryTheory.CategoryStruct.comp (R.cochainComplexXIso n₁ k₁ h₁).hom
      (CategoryTheory.CategoryStruct.comp (R.cocomplex.d k₁ k₂) (R.cochainComplexXIso n₂ k₂ h₂).inv)
-- Mathlib.CategoryTheory.Iso
CategoryTheory.Iso.inv_comp_eq_id : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {X Y : C} (α : X ≅ Y) {f : X ⟶ Y},
  CategoryTheory.CategoryStruct.comp α.inv f = CategoryTheory.CategoryStruct.id Y ↔ f = α.hom
-- Mathlib.Analysis.Complex.Trigonometric
Complex.cosh_ofReal_re : ∀ (x : ℝ), (Complex.cosh ↑x).re = Real.cosh x
-- Mathlib.MeasureTheory.Integral.Bochner.Basic
MeasureTheory.L1.dist_eq_integral_dist : ∀ {α : Type u_1} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} {H : Type u_6} [inst : NormedAddCommGroup H]
  (f g : ↥(MeasureTheory.Lp H 1 μ)), dist f g = ∫ (a : α), dist (↑↑f a) (↑↑g a) ∂μ
-- Lean.Meta.Diagnostics
Lean.Meta.DiagSummary.mk.sizeOf_spec : ∀ (data : Array Lean.MessageData) (max : ℕ), sizeOf { data := data, max := max } = 1 + sizeOf data + sizeOf max
-- Lean.Data.Lsp.LanguageFeatures
Lean.Lsp.InlayHintLabelPart : Type
-- Mathlib.Data.WSeq.Relation
Stream'.WSeq.bind.eq_1 : ∀ {α : Type u} {β : Type v} (s : Stream'.WSeq α) (f : α → Stream'.WSeq β), s.bind f = (Stream'.WSeq.map f s).join
-- Mathlib.CategoryTheory.Limits.Shapes.Reflexive
/-- The pair `f g : A ⟶ B` is reflexive if there is a morphism `B ⟶ A` which is a section for both.
 -/
CategoryTheory.IsReflexivePair : {C : Type u} → [inst : CategoryTheory.Category.{v, u} C] → {A B : C} → (A ⟶ B) → (A ⟶ B) → Prop
-- Mathlib.CategoryTheory.Types.Basic
TypeCat.Fun.ext_iff : ∀ {X : Type u_1} {Y : Type u_2} {x y : TypeCat.Fun X Y}, x = y ↔ x.toFun = y.toFun
-- Mathlib.Order.Basic
forall_le_imp_ne_iff_lt : ∀ {α : Type u_2} [inst : LinearOrder α] {a b : α}, (∀ c ≤ a, c ≠ b) ↔ a < b
-- Std.Data.DTreeMap.Raw.Lemmas
Std.DTreeMap.Raw.getKey?_minKeyD : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t : Std.DTreeMap.Raw α β cmp} [Std.TransCmp cmp],
  t.WF → t.isEmpty = false → ∀ {fallback : α}, t.getKey? (t.minKeyD fallback) = some (t.minKeyD fallback)
-- Lean.Meta.Sym.ReplaceS
_private.Lean.Meta.Sym.ReplaceS.0.Lean.Meta.Sym.visit.match_1.splitter : (motive : Lean.Expr → Sort u_1) →
  (e : Lean.Expr) →
    ((a : Lean.Literal) → motive (Lean.Expr.lit a)) →
      ((mvarId : Lean.MVarId) → motive (Lean.Expr.mvar mvarId)) →
        ((deBruijnIndex : ℕ) → motive (Lean.Expr.bvar deBruijnIndex)) →
          ((fvarId : Lean.FVarId) → motive (Lean.Expr.fvar fvarId)) →
            ((declName : Lean.Name) → (us : List Lean.Level) → motive (Lean.Expr.const declName us)) →
              ((u : Lean.Level) → motive (Lean.Expr.sort u)) →
                ((f a : Lean.Expr) → motive (f.app a)) →
                  ((data : Lean.MData) → (a : Lean.Expr) → motive (Lean.Expr.mdata data a)) →
                    ((typeName : Lean.Name) → (idx : ℕ) → (a : Lean.Expr) → motive (Lean.Expr.proj typeName idx a)) →
                      ((binderName : Lean.Name) →
                          (d b : Lean.Expr) →
                            (binderInfo : Lean.BinderInfo) → motive (Lean.Expr.forallE binderName d b binderInfo)) →
                        ((binderName : Lean.Name) →
                            (d b : Lean.Expr) →
                              (binderInfo : Lean.BinderInfo) → motive (Lean.Expr.lam binderName d b binderInfo)) →
                          ((declName : Lean.Name) →
                              (t v b : Lean.Expr) → (nondep : Bool) → motive (Lean.Expr.letE declName t v b nondep)) →
                            motive e