mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Analysis.BoxIntegral.Box.Basic
/-- Make a `WithBot (Box ι)` from a pair of corners `l u : ι → ℝ`. If `l i < u i` for all `i`,
then the result is `⟨l, u, _⟩ : Box ι`, otherwise it is `⊥`. In any case, the result interpreted
as a set in `ι → ℝ` is the set `{x : ι → ℝ | ∀ i, x i ∈ Ioc (l i) (u i)}`.  -/
BoxIntegral.Box.mk' : {ι : Type u_1} → (ι → ℝ) → (ι → ℝ) → WithBot (BoxIntegral.Box ι)
-- Mathlib.Data.Nat.MaxPowDiv
Nat.divMaxPow_one_left : ∀ (p : ℕ), Nat.divMaxPow 1 p = 1
-- Mathlib.GroupTheory.GroupAction.Defs
AddAction.instElemOrbit_1 : {G : Type u_1} →
  {α : Type u_2} →
    [inst : AddGroup G] → [inst_1 : AddAction G α] → (x : AddAction.orbitRel.Quotient G α) → AddAction G ↑x.orbit
-- Qq.Macro
Qq.Impl.ExprBackSubstResult.quoted.injEq : ∀ (e e_1 : Lean.Expr), (Qq.Impl.ExprBackSubstResult.quoted e = Qq.Impl.ExprBackSubstResult.quoted e_1) = (e = e_1)
-- Mathlib.CategoryTheory.Monoidal.Functor
CategoryTheory.Functor.LaxMonoidal.right_unitality : ∀ {C : Type u₁} {inst : CategoryTheory.Category.{v₁, u₁} C} {inst_1 : CategoryTheory.MonoidalCategory C} {D : Type u₂}
  {inst_2 : CategoryTheory.Category.{v₂, u₂} D} {inst_3 : CategoryTheory.MonoidalCategory D}
  (F : CategoryTheory.Functor C D) [self : F.LaxMonoidal] (X : C),
  (CategoryTheory.MonoidalCategoryStruct.rightUnitor (F.obj X)).hom =
    CategoryTheory.CategoryStruct.comp
      (CategoryTheory.MonoidalCategoryStruct.whiskerLeft (F.obj X) (CategoryTheory.Functor.LaxMonoidal.ε F))
      (CategoryTheory.CategoryStruct.comp
        (CategoryTheory.Functor.LaxMonoidal.μ F X (CategoryTheory.MonoidalCategoryStruct.tensorUnit C))
        (F.map (CategoryTheory.MonoidalCategoryStruct.rightUnitor X).hom))
-- Mathlib.CategoryTheory.Limits.Shapes.Multiequalizer
CategoryTheory.Limits.MulticospanIndex.mk.sizeOf_spec : ∀ {J : CategoryTheory.Limits.MulticospanShape} {C : Type u} [inst : CategoryTheory.Category.{v, u} C]
  [inst_1 : SizeOf C] (left : J.L → C) (right : J.R → C) (fst : (b : J.R) → left (J.fst b) ⟶ right b)
  (snd : (b : J.R) → left (J.snd b) ⟶ right b), sizeOf { left := left, right := right, fst := fst, snd := snd } = 1
-- Mathlib.AlgebraicTopology.SimplicialObject.DeltaZeroIter
CategoryTheory.SimplicialObject.δ₀Iter.eq_1 : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] (X : CategoryTheory.SimplicialObject C) {n m : ℕ} (i : ℕ)
  (hi : n + i = m), X.δ₀Iter i hi = X.map (SimplexCategory.δ₀Iter i hi).op
-- Mathlib.Analysis.Complex.UpperHalfPlane.Metric
UpperHalfPlane.dist_triangle : ∀ (a b c : UpperHalfPlane), dist a c ≤ dist a b + dist b c
-- Mathlib.Analysis.Meromorphic.LogDeriv
/-- The logarithmic derivative converts products into sums: away from a codiscrete subset of `U`, the
logarithmic derivative of a finite product of integer powers of meromorphic functions is the
corresponding weighted sum of logarithmic derivatives. This is the shape of statement used in the
differentiated Poisson–Jensen formula, where the exponents are given by a divisor.
 -/
MeromorphicOn.logDeriv_finprod_zpow_eventuallyEq : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {𝕜' : Type u_2} [inst_1 : NontriviallyNormedField 𝕜']
  [inst_2 : NormedAlgebra 𝕜 𝕜'] {U : Set 𝕜} {ι : Type u_3} {F : ι → 𝕜 → 𝕜'} {d : ι → ℤ},
  (Function.support d).Finite →
    (∀ (i : ι), MeromorphicOn (F i) U) →
      (∀ (i : ι), ∀ x ∈ U, meromorphicOrderAt (F i) x ≠ ⊤) →
        logDeriv (∏ᶠ (i : ι), F i ^ d i) =ᶠ[Filter.codiscreteWithin U] fun z => ∑ᶠ (i : ι), d i • logDeriv (F i) z
-- Mathlib.Algebra.Group.Subgroup.Defs
/-- `G` is closed under negation  -/
AddSubgroup.neg_mem' : ∀ {G : Type u_3} [inst : AddGroup G] (self : AddSubgroup G) {x : G}, x ∈ self.carrier → -x ∈ self.carrier
-- Mathlib.CategoryTheory.Yoneda
CategoryTheory.map_coyonedaEquiv : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {X Y : C} {F : CategoryTheory.Functor C (Type v₁)}
  (f : CategoryTheory.coyoneda.obj (Opposite.op X) ⟶ F) (g : X ⟶ Y),
  (CategoryTheory.ConcreteCategory.hom (F.map g)) (CategoryTheory.coyonedaEquiv f) =
    (CategoryTheory.ConcreteCategory.hom (f.app Y)) g
-- Mathlib.Order.SuccPred.Basic
WithBot.pred_coe : ∀ {α : Type u_1} [inst : PartialOrder α] [inst_1 : PredOrder α] [inst_2 : (a : α) → Decidable (Order.pred a = a)]
  [NoMinOrder α] {a : α}, Order.pred ↑a = ↑(Order.pred a)
-- Mathlib.Analysis.Convex.Cone.InnerDual
/-- Relative geometric interpretation of **Farkas' lemma**. Also stronger version of the
**Hahn-Banach separation theorem** for proper cones.  -/
ProperCone.relative_hyperplane_separation : ∀ {E : Type u_2} {F : Type u_3} [inst : NormedAddCommGroup E] [inst_1 : InnerProductSpace ℝ E]
  [inst_2 : CompleteSpace E] [inst_3 : NormedAddCommGroup F] [inst_4 : InnerProductSpace ℝ F] [inst_5 : CompleteSpace F]
  {C : ProperCone ℝ E} {f : E →L[ℝ] F} {b : F},
  b ∈ ProperCone.map f C ↔ ∀ (y : F), (ContinuousLinearMap.adjoint f) y ∈ ProperCone.innerDual ↑C → 0 ≤ inner ℝ b y
-- Mathlib.MeasureTheory.Integral.Average
MeasureTheory.average_const : ∀ {α : Type u_1} {E : Type u_2} {m0 : MeasurableSpace α} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E]
  [CompleteSpace E] (μ : MeasureTheory.Measure α) [MeasureTheory.IsFiniteMeasure μ] [h : NeZero μ] (c : E),
  ⨍ (_x : α), c ∂μ = c
-- Mathlib.SetTheory.Cardinal.Finite
Nat.card_ulift : ∀ (α : Type u_3), Nat.card (ULift.{u_4, u_3} α) = Nat.card α
-- Batteries.Data.UnionFind.Basic
/-- Link a union-find node to a root node.  -/
Batteries.UnionFind.link : (self : Batteries.UnionFind) → Fin self.size → (y : Fin self.size) → self.parent ↑y = ↑y → Batteries.UnionFind
-- Mathlib.CategoryTheory.Conj
CategoryTheory.Iso.self_symm_conj : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {X Y : C} (α : X ≅ Y) (f : CategoryTheory.End Y),
  α.conj (α.symm.conj f) = f
-- Aesop.Forward.Match.Types
/-- Premises that appear in slots which are as yet unassigned in this match
(i.e., in slots with index greater than `level`). This is a property of the
rule, but we include it here because it's used to check whether two matches
are equivalent.  -/
Aesop.Match.forwardDeps : Aesop.Match → Array Aesop.PremiseIndex
-- Mathlib.LinearAlgebra.Basis.Defs
Module.subsingletonEquiv.congr_simp : ∀ (R : Type u_4) (M : Type u_5) (ι : Type u_6) [inst : Semiring R] [inst_1 : Subsingleton R] [inst_2 : AddCommMonoid M]
  [inst_3 : Module R M], Module.subsingletonEquiv R M ι = Module.subsingletonEquiv R M ι
-- Lean.Data.Iterators.Producers.PersistentHashMap
Lean.PersistentHashMap.instIteratorLoop : {α : Type u_1} →
  {β : Type u_2} → {n : Type u_3 → Type u_4} → [Monad n] → Std.IteratorLoop (Lean.PersistentHashMap.Zipper α β) Id n
-- Mathlib.CategoryTheory.Triangulated.TriangleShift
CategoryTheory.Pretriangulated.Triangle.shiftFunctorZero_hom_app_hom₃ : ∀ (C : Type u) [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Preadditive C]
  [inst_2 : CategoryTheory.HasShift C ℤ] (X : CategoryTheory.Pretriangulated.Triangle C),
  ((CategoryTheory.Pretriangulated.Triangle.shiftFunctorZero C).hom.app X).hom₃ =
    (CategoryTheory.shiftFunctorZero C ℤ).hom.app X.obj₃
-- Mathlib.Algebra.Homology.HomotopyCategory.HomComplex
/-- The differential on a cochain complex, as a cochain of degree `1`.  -/
CochainComplex.HomComplex.Cochain.diff : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    [inst_1 : CategoryTheory.Preadditive C] → (K : CochainComplex C ℤ) → CochainComplex.HomComplex.Cochain K K 1
-- Mathlib.NumberTheory.NumberField.Cyclotomic.Ideal
/-- Write `n = p ^ (k + 1) * m` where the prime `p` does not divide `m`, then the ramification index
of `p` in `ℚ(ζₙ)` is `p ^ k * (p - 1)`.
 -/
IsCyclotomicExtension.Rat.ramificationIdxIn_eq : ∀ (n : ℕ) {m p k : ℕ} [hp : Fact (Nat.Prime p)] (K : Type u_1) [inst : Field K] [inst_1 : NumberField K]
  [IsCyclotomicExtension {n} ℚ K],
  n = p ^ (k + 1) * m → ¬p ∣ m → (Ideal.span {↑p}).ramificationIdxIn (NumberField.RingOfIntegers K) = p ^ k * (p - 1)
-- Std.Data.Internal.List.Associative
_private.Std.Data.Internal.List.Associative.0.Std.Internal.List.Option.map_dmap : ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} (x : Option α) (f : (a : α) → x = some a → β) (g : β → γ),
  Option.map g (Std.Internal.List.Option.dmap✝ x f) = Std.Internal.List.Option.dmap✝ x fun a h => g (f a h)
-- Lean.Meta.Tactic.Simp.Types
Lean.Meta.Simp.Methods.toMethodsRef : Lean.Meta.Simp.Methods → Lean.Meta.Simp.MethodsRef
-- Mathlib.Algebra.Polynomial.Degree.Operations
Polynomial.degree_mul_C_of_isUnit : ∀ {R : Type u} {a : R} [inst : Semiring R], IsUnit a → ∀ (p : Polynomial R), (p * Polynomial.C a).degree = p.degree
-- Init.Grind.Ring.CommSolver
Lean.Grind.CommRing.Mon.beq' : Lean.Grind.CommRing.Mon → Lean.Grind.CommRing.Mon → Bool
-- Mathlib.Algebra.ContinuedFractions.Translations
GenContFract.terminatedAt_iff_s_none : ∀ {α : Type u_1} {g : GenContFract α} {n : ℕ}, g.TerminatedAt n ↔ g.s.get? n = none
-- Mathlib.Algebra.Polynomial.BigOperators
Polynomial.natDegree_multiset_prod_of_monic : ∀ {R : Type u} [inst : CommSemiring R] (t : Multiset (Polynomial R)),
  (∀ f ∈ t, f.Monic) → t.prod.natDegree = (Multiset.map Polynomial.natDegree t).sum
-- Mathlib.Algebra.Polynomial.Splits
Polynomial.splits_mul_iff_right : ∀ {R : Type u_1} [inst : CommRing R] {f g : Polynomial R} [IsDomain R], f ≠ 0 → f.Splits → ((f * g).Splits ↔ g.Splits)
-- Mathlib.GroupTheory.Rank
/-- The minimum number of generators of a group.  -/
Group.rank : (G : Type u_1) → [inst : Group G] → [h : Group.FG G] → ℕ
-- Mathlib.Analysis.InnerProductSpace.StandardSubspace
/-- The imaginary unit as an invertible element.  -/
Complex.UnitI : ℂˣ
-- Mathlib.Algebra.Group.Action.Pointwise.Finset
Finset.mem_neg_vadd_finset_iff : ∀ {α : Type u_2} {β : Type u_3} [inst : DecidableEq β] [inst_1 : AddGroup α] [inst_2 : AddAction α β] {s : Finset β}
  {a : α} {b : β}, b ∈ -a +ᵥ s ↔ a +ᵥ b ∈ s
-- Mathlib.CategoryTheory.Bicategory.Basic
CategoryTheory.Bicategory.rightUnitor_comp_inv : ∀ {B : Type u} [inst : CategoryTheory.Bicategory B] {a b c : B} (f : a ⟶ b) (g : b ⟶ c),
  (CategoryTheory.Bicategory.rightUnitor (CategoryTheory.CategoryStruct.comp f g)).inv =
    CategoryTheory.CategoryStruct.comp
      (CategoryTheory.Bicategory.whiskerLeft f (CategoryTheory.Bicategory.rightUnitor g).inv)
      (CategoryTheory.Bicategory.associator f g (CategoryTheory.CategoryStruct.id c)).inv
-- Init.Data.SInt.Bitwise
ISize.toBitVec_or : ∀ (a b : ISize), (a ||| b).toBitVec = a.toBitVec ||| b.toBitVec
-- Mathlib.Tactic.CategoryTheory.Coherence.Normalize
Mathlib.Tactic.BicategoryLike.HorizontalComp.cons.sizeOf_spec : ∀ (e : Mathlib.Tactic.BicategoryLike.Mor₂) (η : Mathlib.Tactic.BicategoryLike.WhiskerRight)
  (ηs : Mathlib.Tactic.BicategoryLike.HorizontalComp),
  sizeOf (Mathlib.Tactic.BicategoryLike.HorizontalComp.cons e η ηs) = 1 + sizeOf e + sizeOf η + sizeOf ηs
-- Init.Data.Int.Order
Int.sign_one : Int.sign 1 = 1
-- Std.Data.DTreeMap.Raw.Basic
Std.DTreeMap.Raw.instInhabited : {α : Type u} → {β : α → Type v} → {cmp : α → α → Ordering} → Inhabited (Std.DTreeMap.Raw α β cmp)
-- Mathlib.Data.Finsupp.WellFounded
Finsupp.Lex.wellFounded : ∀ {α : Type u_1} {N : Type u_2} [inst : Zero N] {r : α → α → Prop} {s : N → N → Prop},
  (∀ ⦃n : N⦄, ¬s n 0) → WellFounded s → WellFounded (rᶜ ⊓ fun x1 x2 => x1 ≠ x2) → WellFounded (Finsupp.Lex r s)
-- Mathlib.Data.ENNReal.Operations
ENNReal.add_lt_add_iff_right : ∀ {a b c : ENNReal}, a ≠ ⊤ → (b + a < c + a ↔ b < c)
-- Mathlib.Topology.VectorBundle.Basic
/-- A coordinate change function between two trivializations, as a continuous linear equivalence.
Defined to be the identity when `b` does not lie in the base set of both trivializations.  -/
Bundle.Trivialization.coordChangeL : (R : Type u_1) →
  {B : Type u_2} →
    {F : Type u_3} →
      {E : B → Type u_4} →
        [inst : Semiring R] →
          [inst_1 : TopologicalSpace F] →
            [inst_2 : TopologicalSpace B] →
              [inst_3 : TopologicalSpace (Bundle.TotalSpace F E)] →
                [inst_4 : AddCommMonoid F] →
                  [inst_5 : Module R F] →
                    [inst_6 : (x : B) → AddCommMonoid (E x)] →
                      [inst_7 : (x : B) → Module R (E x)] →
                        (e e' : Bundle.Trivialization F Bundle.TotalSpace.proj) →
                          [Bundle.Trivialization.IsLinear R e] → [Bundle.Trivialization.IsLinear R e'] → B → F ≃L[R] F
-- Std.Data.ExtDTreeMap.Lemmas
Std.ExtDTreeMap.maxKeyD_le : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t : Std.ExtDTreeMap α β cmp} [inst : Std.TransCmp cmp],
  t ≠ ∅ → ∀ {k fallback : α}, (cmp (t.maxKeyD fallback) k).isLE = true ↔ ∀ k' ∈ t, (cmp k' k).isLE = true
-- Mathlib.Data.Set.SymmDiff
Set.subset_symmDiff_union_symmDiff_left : ∀ {α : Type u} {s t u : Set α}, Disjoint s t → u ⊆ symmDiff s u ∪ symmDiff t u
-- Mathlib.Algebra.Homology.Embedding.Extend
HomologicalComplex.extend.d_eq : ∀ {ι : Type u_1} {c : ComplexShape ι} {C : Type u_3} [inst : CategoryTheory.Category.{v_1, u_3} C]
  [inst_1 : CategoryTheory.Limits.HasZeroObject C] [inst_2 : CategoryTheory.Limits.HasZeroMorphisms C]
  (K : HomologicalComplex C c) {i j : Option ι} {a b : ι} (hi : i = some a) (hj : j = some b),
  HomologicalComplex.extend.d K i j =
    CategoryTheory.CategoryStruct.comp (HomologicalComplex.extend.XIso K hi).hom
      (CategoryTheory.CategoryStruct.comp (K.d a b) (HomologicalComplex.extend.XIso K hj).inv)
-- Init.Data.String.Lemmas.Pattern.TakeDrop.Basic
String.Slice.takeEndWhile_takeEndWhile : ∀ {ρ : Type} {pat : ρ} [inst : String.Slice.Pattern.Model.PatternModel pat]
  [inst_1 : String.Slice.Pattern.BackwardPattern pat] [String.Slice.Pattern.Model.LawfulBackwardPatternModel pat]
  {s : String.Slice}, (s.takeEndWhile pat).takeEndWhile pat = s.takeEndWhile pat
-- Lean.Parser.Basic
Lean.Parser.LeadingIdentBehavior.noConfusionType : Sort v✝ → Lean.Parser.LeadingIdentBehavior → Lean.Parser.LeadingIdentBehavior → Sort v✝
-- Mathlib.Topology.UniformSpace.CompactConvergence
/-- In a weakly locally compact space,
convergence in the compact-open topology is the same as locally uniform convergence.

The right-to-left implication holds in any topological space,
see `ContinuousMap.tendsto_of_tendstoLocallyUniformly`.  -/
ContinuousMap.tendsto_iff_tendstoLocallyUniformly : ∀ {α : Type u₁} {β : Type u₂} [inst : TopologicalSpace α] [inst_1 : UniformSpace β] {f : C(α, β)} {ι : Type u₃}
  {p : Filter ι} {F : ι → C(α, β)} [WeaklyLocallyCompactSpace α],
  Filter.Tendsto F p (nhds f) ↔ TendstoLocallyUniformly (fun i a => (F i) a) (⇑f) p
-- Mathlib.Combinatorics.Quiver.Covering
Prefunctor.IsCovering.symmetrify : ∀ {U : Type u_1} [inst : Quiver U] {V : Type u_2} [inst_1 : Quiver V] (φ : U ⥤q V),
  φ.IsCovering → φ.symmetrify.IsCovering
-- Mathlib.Analysis.Normed.Operator.Compact.FredholmAlternative
/-- If `T` is a compact operator on a Banach space, then the nonzero eigenvalues of `T` are exactly
the nonzero points in the spectrum of `T`. This is a consequence of the Fredholm alternative for
compact operators.  -/
IsCompactOperator.hasEigenvalue_iff_mem_spectrum : ∀ {𝕜 : Type u_1} {X : Type u_2} [inst : NontriviallyNormedField 𝕜] [inst_1 : NormedAddCommGroup X]
  [inst_2 : NormedSpace 𝕜 X] {T : X →L[𝕜] X} {μ : 𝕜} [CompleteSpace X],
  IsCompactOperator ⇑T → μ ≠ 0 → (Module.End.HasEigenvalue (↑T) μ ↔ μ ∈ spectrum 𝕜 T)
-- Mathlib.Topology.Separation.CompletelyRegular
CompletelyRegularSpace.mk : ∀ {X : Type u} [inst : TopologicalSpace X],
  (∀ (x : X) (K : Set X), IsClosed K → x ∉ K → ∃ f, Continuous f ∧ f x = 0 ∧ Set.EqOn f 1 K) → CompletelyRegularSpace X
-- Init.Data.BitVec.Bitblast
/-- The value of `(carry i x y false)` can be computed by truncating `x` and `y`
to `len` bits where `len ≥ i`.  -/
BitVec.carry_extractLsb'_eq_carry : ∀ {w i len : ℕ},
  i < len →
    ∀ {x y : BitVec w} {b : Bool},
      BitVec.carry i (BitVec.extractLsb' 0 len x) (BitVec.extractLsb' 0 len y) b = BitVec.carry i x y b
-- Mathlib.RingTheory.PowerSeries.WeierstrassPreparation
/-- The remainder `r` in Weierstrass division, denoted by `f %ʷ g`. Note that when the image of
`g` in the residue field is zero, this is defined to be zero.  -/
PowerSeries.«term_%ʷ_» : Lean.TrailingParserDescr
-- Mathlib.Topology.Category.TopCommRingCat
TopCommRingCat.isCommRing : (self : TopCommRingCat) → CommRing self.α
-- Mathlib.Topology.MetricSpace.Dilation
/-- `Dilation.ratio` as a monoid homomorphism from `α →ᵈ α` to `ℝ≥0`.  -/
Dilation.ratioHom : {α : Type u_1} → [inst : PseudoEMetricSpace α] → (α →ᵈ α) →* NNReal
-- Mathlib.NumberTheory.Real.Irrational
irrational_ratCast_add_iff : ∀ {q : ℚ} {x : ℝ}, Irrational (↑q + x) ↔ Irrational x
-- Mathlib.MeasureTheory.Group.Prod
/-- The map `(x, y) ↦ (x, x + y)` as a `MeasurableEquiv`.  -/
MeasurableEquiv.shearAddRight : (G : Type u_1) →
  [inst : MeasurableSpace G] → [inst_1 : AddGroup G] → [MeasurableAdd₂ G] → [MeasurableNeg G] → G × G ≃ᵐ G × G
-- Mathlib.Algebra.Lie.Abelian
lie_abelian_iff_equiv_lie_abelian : ∀ {R : Type u} {L₁ : Type v} {L₂ : Type w} [inst : CommRing R] [inst_1 : LieRing L₁] [inst_2 : LieRing L₂]
  [inst_3 : LieAlgebra R L₁] [inst_4 : LieAlgebra R L₂] (e : L₁ ≃ₗ⁅R⁆ L₂), IsLieAbelian L₁ ↔ IsLieAbelian L₂
-- Mathlib.Algebra.Group.Submonoid.Operations
Submonoid.map.congr_simp : ∀ {M : Type u_1} {N : Type u_2} [inst : MulOneClass M] [inst_1 : MulOneClass N] {F : Type u_4} [inst_2 : FunLike F M N]
  [mc : MonoidHomClass F M N] (f f_1 : F),
  f = f_1 → ∀ (S S_1 : Submonoid M), S = S_1 → Submonoid.map f S = Submonoid.map f_1 S_1
-- Mathlib.CategoryTheory.Limits.Shapes.ZeroMorphisms
CategoryTheory.Limits.idZeroEquivIsoZero_apply_hom : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Limits.HasZeroObject C]
  [inst_2 : CategoryTheory.Limits.HasZeroMorphisms C] (X : C) (h : CategoryTheory.CategoryStruct.id X = 0),
  ((CategoryTheory.Limits.idZeroEquivIsoZero X) h).hom = 0
-- Mathlib.Analysis.Calculus.TangentCone.Basic
UniqueDiffWithinAt.inter' : ∀ {𝕜 : Type u_1} {E : Type u_2} [inst : AddCommGroup E] [inst_1 : Semiring 𝕜] [inst_2 : Module 𝕜 E]
  [inst_3 : TopologicalSpace E] [ContinuousAdd E] {s t : Set E} {x : E},
  UniqueDiffWithinAt 𝕜 s x → t ∈ nhdsWithin x s → UniqueDiffWithinAt 𝕜 (s ∩ t) x
-- Mathlib.Algebra.Polynomial.Monic
Polynomial.Monic.pow : ∀ {R : Type u} [inst : Semiring R] {p : Polynomial R}, p.Monic → ∀ (n : ℕ), (p ^ n).Monic
-- Mathlib.Algebra.Homology.Linear
HomologicalComplex.units_smul_f_apply : ∀ {R : Type u_1} [inst : Semiring R] {C : Type u_2} [inst_1 : CategoryTheory.Category.{v_1, u_2} C]
  [inst_2 : CategoryTheory.Preadditive C] [inst_3 : CategoryTheory.Linear R C] {ι : Type u_4} {c : ComplexShape ι}
  {X Y : HomologicalComplex C c} (r : Rˣ) (f : X ⟶ Y) (n : ι), (r • f).f n = r • f.f n
-- Mathlib.CategoryTheory.Limits.Shapes.Images
/-- Data exhibiting that a given factorisation through a mono is initial.  -/
CategoryTheory.Limits.IsImage.lift : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    {X Y : C} →
      {f : X ⟶ Y} →
        {F : CategoryTheory.Limits.MonoFactorisation f} →
          CategoryTheory.Limits.IsImage F → (F' : CategoryTheory.Limits.MonoFactorisation f) → F.I ⟶ F'.I
-- Mathlib.Order.Shrink
instPreorderShrink : {α : Type u_1} → [inst : Small.{u, u_1} α] → [Preorder α] → Preorder (Shrink.{u, u_1} α)
-- Mathlib.CategoryTheory.Limits.WeakLimits.WeakPullbacks
/-- The second projection of the weak pullback of `f` and `g`.  -/
CategoryTheory.Limits.weakPullback.snd : {C : Type u_1} →
  [inst : CategoryTheory.Category.{v_1, u_1} C] →
    {X Y Z : C} →
      (f : X ⟶ Z) →
        (g : Y ⟶ Z) → [inst_1 : CategoryTheory.Limits.HasWeakPullback f g] → CategoryTheory.Limits.weakPullback f g ⟶ Y
-- Mathlib.NumberTheory.ModularForms.QExpansion
UpperHalfPlane.cuspFunction.eq_1 : ∀ (h : ℝ) (f : UpperHalfPlane → ℂ),
  UpperHalfPlane.cuspFunction h f = Function.Periodic.cuspFunction h (f ∘ ↑UpperHalfPlane.ofComplex)
-- Mathlib.Data.Multiset.MapFold
Multiset.exists_multiset_eq_map_quot_mk : ∀ {α : Type u_1} {r : α → α → Prop} (s : Multiset (Quot r)), ∃ t, s = Multiset.map (Quot.mk r) t
-- Mathlib.CategoryTheory.Monoidal.Grp
/-- An adjunction of monoidal functors lifts to an adjunction of their lifts
to additive group objects.  -/
CategoryTheory.Adjunction.mapAddGrp : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    [inst_1 : CategoryTheory.CartesianMonoidalCategory C] →
      {D : Type u₂} →
        [inst_2 : CategoryTheory.Category.{v₂, u₂} D] →
          [inst_3 : CategoryTheory.CartesianMonoidalCategory D] →
            {F : CategoryTheory.Functor C D} →
              {G : CategoryTheory.Functor D C} →
                (F ⊣ G) → [inst_4 : F.Monoidal] → [inst_5 : G.Monoidal] → F.mapAddGrp ⊣ G.mapAddGrp
-- Mathlib.RingTheory.FractionalIdeal.Operations
FractionalIdeal.coeIdeal_inj : ∀ {R : Type u_1} [inst : CommRing R] {K : Type u_3} [inst_1 : Field K] [inst_2 : Algebra R K] [IsFractionRing R K]
  {I J : Ideal R}, ↑I = ↑J ↔ I = J
-- Mathlib.CategoryTheory.Limits.Cones
/-- The categories of cones over `F` and `G` are equivalent if `F` and `G` are naturally isomorphic
(possibly after changing the indexing category by an equivalence).
 -/
CategoryTheory.Limits.Cone.equivalenceOfReindexing : {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} →
              {G : CategoryTheory.Functor K C} →
                (e : K ≌ J) → (e.functor.comp F ≅ G) → (CategoryTheory.Limits.Cone F ≌ CategoryTheory.Limits.Cone G)
-- Std.Time.Format.Modifier
/-- `OffsetO` represents localized offset text formats based on the number of pattern letters.
 -/
Std.Time.OffsetO : Type
-- Lean.Hygiene
Lean.Unhygienic.Context.mk.inj : ∀ {ref : Lean.Syntax} {scope : Lean.MacroScope} {ref_1 : Lean.Syntax} {scope_1 : Lean.MacroScope},
  { ref := ref, scope := scope } = { ref := ref_1, scope := scope_1 } → ref = ref_1 ∧ scope = scope_1
-- Std.Data.DHashMap.Lemmas
Std.DHashMap.insert_eq_insert : ∀ {α : Type u} {β : α → Type v} {x : BEq α} {x_1 : Hashable α} {m : Std.DHashMap α β} {p : (a : α) × β a},
  insert p m = m.insert p.fst p.snd
-- Std.Data.DHashMap.Lemmas
Std.DHashMap.Equiv.symm : ∀ {α : Type u} {β : α → Type v} {x : BEq α} {x_1 : Hashable α} {m₁ m₂ : Std.DHashMap α β}, m₁.Equiv m₂ → m₂.Equiv m₁
-- Init.Data.UInt.Lemmas
UInt8.toFin_inj : ∀ {a b : UInt8}, a.toFin = b.toFin ↔ a = b
-- Mathlib.CategoryTheory.Preadditive.Biproducts
CategoryTheory.Limits.biprod.lift_desc_assoc : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Preadditive C] {X Y : C}
  [inst_2 : CategoryTheory.Limits.HasBinaryBiproduct X Y] {T U : C} {f : T ⟶ X} {g : T ⟶ Y} {h : X ⟶ U} {i : Y ⟶ U}
  {Z : C} (h_1 : U ⟶ Z),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.biprod.lift f g)
      (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.biprod.desc h i) h_1) =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.CategoryStruct.comp f h + CategoryTheory.CategoryStruct.comp g i)
      h_1
-- Mathlib.RepresentationTheory.Irreducible
Representation.IsIrreducible.finrank_intertwiningMap_self : ∀ {G : Type u_1} {k : Type u_2} {V : Type u_3} [inst : Monoid G] [inst_1 : Field k] [inst_2 : AddCommGroup V]
  [inst_3 : Module k V] (ρ : Representation k G V) [ρ.IsIrreducible] [FiniteDimensional k V] [IsAlgClosed k],
  Module.finrank k (ρ.IntertwiningMap ρ) = 1
-- Mathlib.Data.Set.Card
Set.encard_exchange' : ∀ {α : Type u_1} {s : Set α} {a b : α}, a ∉ s → b ∈ s → (insert a s \ {b}).encard = s.encard