mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Algebra.BrauerGroup.Defs
CSA.mk.inj : ∀ {K : Type u} {inst : Field K} {toAlgCat : AlgCat K} {isCentral : Algebra.IsCentral K ↑toAlgCat}
  {isSimple : IsSimpleRing ↑toAlgCat} {fin_dim : FiniteDimensional K ↑toAlgCat} {toAlgCat_1 : AlgCat K}
  {isCentral_1 : Algebra.IsCentral K ↑toAlgCat_1} {isSimple_1 : IsSimpleRing ↑toAlgCat_1}
  {fin_dim_1 : FiniteDimensional K ↑toAlgCat_1},
  { toAlgCat := toAlgCat, isCentral := isCentral, isSimple := isSimple, fin_dim := fin_dim } =
      { toAlgCat := toAlgCat_1, isCentral := isCentral_1, isSimple := isSimple_1, fin_dim := fin_dim_1 } →
    toAlgCat = toAlgCat_1
-- Std.Tactic.BVDecide.Reflect
Std.Tactic.BVDecide.Reflect.BitVec.cond_true : ∀ {w : ℕ} (discr : Bool) (lhs rhs : BitVec w), (!discr || (bif discr then lhs else rhs) == lhs) = true
-- Mathlib.Topology.Algebra.GroupCompletion
instAddCompletion : {α : Type u_3} → [inst : UniformSpace α] → [Add α] → Add (UniformSpace.Completion α)
-- Mathlib.Tactic.ClickSuggestions.Util
/-- The range that should be replaced.
In tactic mode, this should be the range of the suggestion tactic.
In infoview mode, the start and end of the range should both be the cursor position.  -/
Mathlib.Tactic.ClickSuggestions.Context.cursorPos : Mathlib.Tactic.ClickSuggestions.Context → Lean.Lsp.Position
-- Mathlib.Analysis.Analytic.Composition
/-- If two formal multilinear series have positive radius of convergence, then the terms appearing
in the definition of their composition are also summable (when multiplied by a suitable positive
geometric term).  -/
FormalMultilinearSeries.comp_summable_nnreal : ∀ {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} {G : Type u_4} [inst : NontriviallyNormedField 𝕜]
  [inst_1 : NormedAddCommGroup E] [inst_2 : NormedSpace 𝕜 E] [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F]
  [inst_5 : NormedAddCommGroup G] [inst_6 : NormedSpace 𝕜 G] (q : FormalMultilinearSeries 𝕜 F G)
  (p : FormalMultilinearSeries 𝕜 E F),
  0 < q.radius → 0 < p.radius → ∃ r > 0, Summable fun i => ‖q.compAlongComposition p i.snd‖₊ * r ^ i.fst
-- Mathlib.Geometry.Euclidean.Sphere.Tangent
/-- The set of all maximal tangent spaces to the sphere `s` containing the point `p`.  -/
EuclideanGeometry.Sphere.tangentsFrom : {V : Type u_1} →
  {P : Type u_2} →
    [inst : NormedAddCommGroup V] →
      [inst_1 : InnerProductSpace ℝ V] →
        [inst_2 : MetricSpace P] →
          [inst_3 : NormedAddTorsor V P] → EuclideanGeometry.Sphere P → P → Set (AffineSubspace ℝ P)
-- Mathlib.MeasureTheory.Function.StronglyMeasurable.Basic
/-- Eta-expanded form of `MeasureTheory.StronglyMeasurable.const_smul` -/
MeasureTheory.StronglyMeasurable.fun_const_smul : ∀ {α : Type u_1} {β : Type u_2} {f : α → β} {mα : MeasurableSpace α} [inst : TopologicalSpace β] {𝕜 : Type u_5}
  [inst_1 : SMul 𝕜 β] [ContinuousConstSMul 𝕜 β],
  MeasureTheory.StronglyMeasurable f → ∀ (c : 𝕜), MeasureTheory.StronglyMeasurable fun i => c • f i
-- Mathlib.Topology.Homeomorph.Lemmas
Homeomorph.isPreconnected_image : ∀ {X : Type u_1} {Y : Type u_2} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y] {s : Set X} (h : X ≃ₜ Y),
  IsPreconnected (⇑h '' s) ↔ IsPreconnected s
-- Init.Data.SInt.Lemmas
Int8.lt_irrefl : ∀ {a : Int8}, ¬a < a
-- Lean.Server.FileWorker.InlayHints
Lean.Server.FileWorker.applyEditToHint? : Lean.Name → Lean.Elab.InlayHintInfo → Lean.Syntax.Range → String → Option Lean.Elab.InlayHintInfo
-- Mathlib.Algebra.Algebra.NonUnitalSubalgebra
NonUnitalSubalgebra.instSMulMemClass : ∀ {R : Type u} {A : Type v} [inst : CommSemiring R] [inst_1 : NonUnitalNonAssocSemiring A] [inst_2 : Module R A],
  SMulMemClass (NonUnitalSubalgebra R A) R A
-- Mathlib.Data.Set.MulAntidiagonal
Set.MulAntidiagonal.eq_of_fst_le_fst_of_snd_le_snd : ∀ {α : Type u_1} [inst : CommMonoid α] [inst_1 : PartialOrder α] [IsCancelMul α] [MulLeftMono α] [MulRightStrictMono α]
  (s t : Set α) (a : α) {x y : ↑(s.mulAntidiagonal t a)}, (↑x).1 ≤ (↑y).1 → (↑x).2 ≤ (↑y).2 → x = y
-- Init.Data.Rat.Lemmas
Rat.mkRat_eq_div : ∀ (a : ℤ) (b : ℕ), mkRat a b = ↑a / ↑b
-- Mathlib.Analysis.Complex.RiemannMapping
/-- Proof of the Riemann Mapping Theorem, step 1.

If `U` is an open simply connected subset of `ℂ` that is not the whole `ℂ`,
then there exists a function `f : ℂ → ℂ` such that

- `f` is injective;
- the image `f '' U` isn't dense in `ℂ`;
- `f` is complex differentiable on `U` with nonzero derivative.

E.g., one can choose `a ∉ U`, then take `f z` to be the square root of `z - a`.
 -/
_private.Mathlib.Analysis.Complex.RiemannMapping.0.Complex.exists_injective_not_dense_image_deriv_ne_zero : ∀ {U : Set ℂ},
  IsOpen U → IsSimplyConnected U → U ≠ Set.univ → ∃ f, Function.Injective f ∧ ¬Dense (f '' U) ∧ ∀ z ∈ U, deriv f z ≠ 0
-- Mathlib.Algebra.Group.Pointwise.Set.Basic
Set.instAddRightMono : ∀ {α : Type u_2} [inst : Add α], AddRightMono (Set α)
-- Mathlib.Combinatorics.SimpleGraph.Maps
SimpleGraph.map_adj_apply : ∀ {V : Type u_1} {W : Type u_2} {G : SimpleGraph V} {f : V ↪ W} {a b : V},
  (SimpleGraph.map (⇑f) G).Adj (f a) (f b) ↔ G.Adj a b
-- Mathlib.GroupTheory.Torsion
/-- **Alias** of `not_isMulTorsion_iff`.

---

A monoid is not a torsion monoid if it has an element of infinite order.  -/
Monoid.not_isTorsion_iff : ∀ (G : Type u_1) [inst : Monoid G], ¬IsMulTorsion G ↔ ∃ g, ¬IsOfFinOrder g
-- Batteries.Data.PairingHeap
/-- `O(n)`. The number of elements in the heap.  -/
Batteries.PairingHeapImp.Heap.size : {α : Type u_1} → Batteries.PairingHeapImp.Heap α → ℕ
-- Std.Data.Iterators.Lemmas.Equivalence.Basic
Std.instIteratorα : {m : Type u_1 → Type u_2} → {β : Type u_1} → (bit : Std.BundledIterM m β) → Std.Iterator bit.α m β
-- Mathlib.Order.Atoms
isStronglyAtomic_dual_iff_is_stronglyCoatomic : ∀ {α : Type u_4} [inst : Preorder α], IsStronglyAtomic αᵒᵈ ↔ IsStronglyCoatomic α
-- Mathlib.Algebra.Group.Units.Basic
mul_ne_one' : ∀ {α : Type u} [inst : CancelMonoid α] [Subsingleton αˣ] {a b : α}, a * b ≠ 1 ↔ a ≠ 1 ∨ b ≠ 1
-- Mathlib.Topology.Algebra.Module.Equiv
ContinuousSemilinearEquivClass.toSemilinearEquivClass : ∀ {F : Type u_1} {R : outParam (Type u_2)} {S : outParam (Type u_3)} {inst : Semiring R} {inst_1 : Semiring S}
  {σ : outParam (R →+* S)} {σ' : outParam (S →+* R)} {inst_2 : RingHomInvPair σ σ'} {inst_3 : RingHomInvPair σ' σ}
  {M : outParam (Type u_4)} {inst_4 : TopologicalSpace M} {inst_5 : AddCommMonoid M} {M₂ : outParam (Type u_5)}
  {inst_6 : TopologicalSpace M₂} {inst_7 : AddCommMonoid M₂} {inst_8 : Module R M} {inst_9 : Module S M₂}
  {inst_10 : EquivLike F M M₂} [self : ContinuousSemilinearEquivClass F σ M M₂], SemilinearEquivClass F σ M M₂
-- Std.Http.Protocol.H1.Parser
_private.Std.Http.Protocol.H1.Parser.0.Std.Http.Protocol.H1.parseChunkExt : Std.Http.Protocol.H1.Config →
  Std.Internal.Parsec.ByteArray.Parser (Std.Http.Chunk.ExtensionName × Option Std.Http.Chunk.ExtensionValue)
-- Mathlib.AlgebraicGeometry.EllipticCurve.Weierstrass
/-- The notation `\textf` for `WeierstrassCurve.baseChange W A`.  -/
WeierstrassCurve.«term_⁄_» : Lean.TrailingParserDescr
-- Mathlib.RingTheory.Ideal.Operations
Ideal.instIdemCommSemiring : {R : Type u} → [inst : CommSemiring R] → IdemCommSemiring (Ideal R)
-- Init.Data.Sum.Lemmas
Sum.exists : ∀ {α : Type u_1} {β : Type u_2} {p : α ⊕ β → Prop}, (∃ x, p x) ↔ (∃ a, p (Sum.inl a)) ∨ ∃ b, p (Sum.inr b)
-- Init.Data.SInt.Basic
/-- Converts 16-bit signed integers to 8-bit signed integers by truncating their bitvector
representation.

This function is overridden at runtime with an efficient implementation.
 -/
Int16.toInt8 : Int16 → Int8
-- Std.Data.DTreeMap.Raw.Basic
/-- Tries to retrieve the key-value pair with the largest key that is less than the given key,
panicking if no such pair exists.
 -/
Std.DTreeMap.Raw.Const.getEntryLT! : {α : Type u} →
  {cmp : α → α → Ordering} → {β : Type v} → [Inhabited (α × β)] → Std.DTreeMap.Raw α (fun x => β) cmp → α → α × β
-- Mathlib.Data.List.Induction
/-- Induction principle from the right for lists: if a property holds for the empty list, and
for `l ++ [a]` if it holds for `l`, then it holds for all lists. The principle is given for
a `Sort`-valued predicate, i.e., it can also be used to construct data.  -/
List.reverseRec : {α : Type u_1} →
  {motive : List α → Sort u_2} →
    motive [] → ((l : List α) → (a : α) → motive l → motive (l ++ [a])) → (l : List α) → motive l
-- Init.Data.Slice.List.Basic
instSliceableListSliceNat_2 : {α : Type u} → Std.Rci.Sliceable (ListSlice α) ℕ (ListSlice α)
-- Mathlib.Order.Antichain
/-- **Alias** of `antisymm`. -/
IsAntichain.isAntisymm : ∀ {α : Sort u_1} {r : α → α → Prop} {a b : α} [Std.Antisymm r], r a b → r b a → a = b
-- Mathlib.Analysis.Calculus.ContDiff.Defs
/-- For `n : ℕ∞`, a function is `C^n` iff it admits `ftaylorSeries 𝕜 f`
as a Taylor series up to order `n`.  -/
contDiff_iff_ftaylorSeries : ∀ {𝕜 : Type u} [inst : NontriviallyNormedField 𝕜] {E : Type uE} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {F : Type uF} [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F] {f : E → F}
  {n : ℕ∞}, ContDiff 𝕜 (↑n) f ↔ HasFTaylorSeriesUpTo (↑n) f (ftaylorSeries 𝕜 f)
-- Mathlib.Algebra.Polynomial.Module.AEval
Module.AEval.of_symm_smul : ∀ {R : Type u_1} {A : Type u_3} {M : Type u_2} [inst : CommSemiring R] [inst_1 : Semiring A] (a : A)
  [inst_2 : Algebra R A] [inst_3 : AddCommMonoid M] [inst_4 : Module A M] [inst_5 : Module R M]
  [inst_6 : IsScalarTower R A M] (f : Polynomial R) (m : Module.AEval R M a),
  (Module.AEval.of R M a).symm (f • m) = (Polynomial.aeval a) f • (Module.AEval.of R M a).symm m
-- Lean.Meta.Instances
Lean.Meta.checkNonClassInstance : Lean.Expr → Lean.MetaM Unit
-- Mathlib.LinearAlgebra.CliffordAlgebra.Grading
/-- To show a property is true on the even or odd part, it suffices to show it is true on the
scalars or vectors (respectively), closed under addition, and under left-multiplication by a pair
of vectors.  -/
CliffordAlgebra.evenOdd_induction : ∀ {R : Type u_1} {M : Type u_2} [inst : CommRing R] [inst_1 : AddCommGroup M] [inst_2 : Module R M]
  (Q : QuadraticForm R M) (n : ZMod 2) {motive : (x : CliffordAlgebra Q) → x ∈ CliffordAlgebra.evenOdd Q n → Prop},
  (∀ (v : CliffordAlgebra Q) (h : v ∈ (CliffordAlgebra.ι Q).range ^ n.val), motive v ⋯) →
    (∀ (x y : CliffordAlgebra Q) (hx : x ∈ CliffordAlgebra.evenOdd Q n) (hy : y ∈ CliffordAlgebra.evenOdd Q n),
        motive x hx → motive y hy → motive (x + y) ⋯) →
      (∀ (m₁ m₂ : M) (x : CliffordAlgebra Q) (hx : x ∈ CliffordAlgebra.evenOdd Q n),
          motive x hx → motive ((CliffordAlgebra.ι Q) m₁ * (CliffordAlgebra.ι Q) m₂ * x) ⋯) →
        ∀ (x : CliffordAlgebra Q) (hx : x ∈ CliffordAlgebra.evenOdd Q n), motive x hx
-- Mathlib.Algebra.Ring.Subring.Defs
SubringClass.subtype_injective : ∀ {R : Type u} {S : Type v} [inst : NonAssocRing R] [inst_1 : SetLike S R] [hSR : SubringClass S R] (s : S),
  Function.Injective ⇑(SubringClass.subtype s)
-- Mathlib.Algebra.Divisibility.Units
IsRelPrime.mul_dvd_of_right_isPrimal : ∀ {α : Type u_1} [inst : CommMonoid α] {x y z : α}, IsRelPrime x y → x ∣ z → y ∣ z → IsPrimal y → x * y ∣ z
-- Mathlib.Analysis.BoxIntegral.Partition.Basic
BoxIntegral.Prepartition.notMem_bot : ∀ {ι : Type u_1} {I J : BoxIntegral.Box ι}, J ∉ ⊥
-- Lean.Widget.TaggedText
Lean.Widget.TaggedText.append.sizeOf_spec : ∀ {α : Type u} [inst : SizeOf α] (a : Array (Lean.Widget.TaggedText α)),
  sizeOf (Lean.Widget.TaggedText.append a) = 1 + sizeOf a
-- Mathlib.Algebra.Polynomial.Splits
Polynomial.Splits.nextCoeff_eq_neg_sum_roots_mul_leadingCoeff : ∀ {R : Type u_1} [inst : CommRing R] {f : Polynomial R} [inst_1 : IsDomain R],
  f.Splits → f.nextCoeff = -f.leadingCoeff * f.roots.sum
-- Mathlib.Analysis.Calculus.Deriv.Add
derivWithin_add_const : ∀ {𝕜 : Type u} [inst : NontriviallyNormedField 𝕜] {F : Type v} [inst_1 : NormedAddCommGroup F]
  [inst_2 : NormedSpace 𝕜 F] {f : 𝕜 → F} {x : 𝕜} {s : Set 𝕜} (c : F),
  derivWithin (fun y => f y + c) s x = derivWithin f s x
-- Mathlib.Tactic.CategoryTheory.Coherence.Datatypes
/-- Extracts a lean expression from an `Obj` term. Return `none` in the monoidal
category context.  -/
Mathlib.Tactic.BicategoryLike.Obj.e? : Mathlib.Tactic.BicategoryLike.Obj → Option Lean.Expr
-- Mathlib.MeasureTheory.Category.MeasCat
TopCat.hasForgetToMeasCat : CategoryTheory.HasForget₂ TopCat MeasCat
-- Mathlib.FieldTheory.IntermediateField.Adjoin.Defs
IntermediateField.coe_bot : ∀ {F : Type u_1} [inst : Field F] {E : Type u_2} [inst_1 : Field E] [inst_2 : Algebra F E],
  ↑⊥ = Set.range ⇑(algebraMap F E)
-- Lean.Parser.Types
Lean.Parser.ParserCacheEntry.mk : Lean.Syntax → ℕ → String.Pos.Raw → Option Lean.Parser.Error → Lean.Parser.ParserCacheEntry
-- Mathlib.MeasureTheory.Integral.Prod
MeasureTheory.integral_continuousLinearMap_prod' : ∀ {E : Type u_5} {F : Type u_6} {G : Type u_7} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E]
  {mE : MeasurableSpace E} [inst_2 : NormedAddCommGroup F] [inst_3 : NormedSpace ℝ F] {mF : MeasurableSpace F}
  [inst_4 : NormedAddCommGroup G] [inst_5 : NormedSpace ℝ G] {μ : MeasureTheory.Measure E}
  [MeasureTheory.IsProbabilityMeasure μ] {ν : MeasureTheory.Measure F} [MeasureTheory.IsProbabilityMeasure ν]
  {L : E × F →L[ℝ] G} [CompleteSpace G],
  MeasureTheory.Integrable (⇑(L ∘SL ContinuousLinearMap.inl ℝ E F)) μ →
    MeasureTheory.Integrable (⇑(L ∘SL ContinuousLinearMap.inr ℝ E F)) ν →
      ∫ (p : E × F), L p ∂μ.prod ν =
        ∫ (x : E), (L ∘SL ContinuousLinearMap.inl ℝ E F) x ∂μ + ∫ (y : F), (L ∘SL ContinuousLinearMap.inr ℝ E F) y ∂ν
-- Mathlib.Data.Finite.Sum
Finite.sum_right : ∀ {β : Type u_2} (α : Type u_3) [Finite (α ⊕ β)], Finite β
-- Mathlib.CategoryTheory.Join.Opposites
CategoryTheory.Join.InclRightCompRightOpOpEquivFunctor_hom_app : ∀ (C : Type u₁) (D : Type u₂) [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  (X : D),
  (CategoryTheory.Join.InclRightCompRightOpOpEquivFunctor C D).hom.app X =
    CategoryTheory.CategoryStruct.id (Opposite.op (CategoryTheory.Join.left (Opposite.op X)))
-- Mathlib.Analysis.Complex.Circle
Circle.coe_inv_eq_conj : ∀ (z : Circle), ↑z⁻¹ = (starRingEnd ℂ) ↑z
-- Mathlib.CategoryTheory.Limits.Types.Products
/-- The terminal object in `Type u` is `PUnit`.  -/
CategoryTheory.Limits.Types.isTerminalPUnit : CategoryTheory.Limits.IsTerminal PUnit.{u + 1}
-- Mathlib.Data.Set.Lattice
Set.iUnion_plift_down : ∀ {α : Type u_1} {ι : Sort u_5} (f : ι → Set α), ⋃ i, f i.down = ⋃ i, f i
-- Init.Data.String.Lemmas.Pattern.TakeDrop.Basic
String.Slice.Pattern.Model.Pos.skipWhile_eq_self_iff : ∀ {ρ : Type} {pat : ρ} [inst : String.Slice.Pattern.Model.PatternModel pat]
  [String.Slice.Pattern.Model.StrictPatternModel pat] [inst_2 : String.Slice.Pattern.ForwardPattern pat]
  [String.Slice.Pattern.Model.LawfulForwardPatternModel pat] {s : String.Slice} {pos : s.Pos},
  pos.skipWhile pat = pos ↔ ¬String.Slice.Pattern.Model.MatchesAt pat pos
-- Mathlib.Analysis.Asymptotics.Defs
/-- **Alias** of the reverse direction of `Asymptotics.isBigOWith_norm_norm`. -/
Asymptotics.IsBigOWith.norm_norm : ∀ {α : Type u_1} {E' : Type u_6} {F' : Type u_7} [inst : SeminormedAddCommGroup E'] [inst_1 : SeminormedAddCommGroup F']
  {c : ℝ} {f' : α → E'} {g' : α → F'} {l : Filter α},
  Asymptotics.IsBigOWith c l f' g' → Asymptotics.IsBigOWith c l (fun x => ‖f' x‖) fun x => ‖g' x‖
-- Mathlib.Algebra.Category.Grp.Basic
CommGrpCat.coe_comp : ∀ {X Y Z : CommGrpCat} {f : X ⟶ Y} {g : Y ⟶ Z},
  ⇑(CategoryTheory.ConcreteCategory.hom (CategoryTheory.CategoryStruct.comp f g)) =
    ⇑(CategoryTheory.ConcreteCategory.hom g) ∘ ⇑(CategoryTheory.ConcreteCategory.hom f)
-- Mathlib.CategoryTheory.GlueData
CategoryTheory.GlueData'.mk.sizeOf_spec : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v, u₁} C] [inst_1 : SizeOf C] (J : Type v) (U : J → C)
  (V : (i j : J) → i ≠ j → C) (f : (i j : J) → (h : i ≠ j) → V i j h ⟶ U i)
  (f_mono :
    autoParam (∀ (i j : J) (h : i ≠ j), CategoryTheory.Mono (f i j h)) CategoryTheory.GlueData'.f_mono._autoParam)
  (f_hasPullback :
    autoParam (∀ (i j k : J) (hij : i ≠ j) (hik : i ≠ k), CategoryTheory.Limits.HasPullback (f i j hij) (f i k hik))
      CategoryTheory.GlueData'.f_hasPullback._autoParam)
  (t : (i j : J) → (h : i ≠ j) → V i j h ⟶ V j i ⋯)
  (t' :
    (i j k : J) →
      (hij : i ≠ j) →
        (hik : i ≠ k) →
          (hjk : j ≠ k) →
            CategoryTheory.Limits.pullback (f i j hij) (f i k hik) ⟶
              CategoryTheory.Limits.pullback (f j k hjk) (f j i ⋯))
  (t_fac :
    ∀ (i j k : J) (hij : i ≠ j) (hik : i ≠ k) (hjk : j ≠ k),
      CategoryTheory.CategoryStruct.comp (t' i j k hij hik hjk)
          (CategoryTheory.Limits.pullback.snd (f j k hjk) (f j i ⋯)) =
        CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pullback.fst (f i j hij) (f i k hik)) (t i j hij))
  (t_inv :
    ∀ (i j : J) (hij : i ≠ j),
      CategoryTheory.CategoryStruct.comp (t i j hij) (t j i ⋯) = CategoryTheory.CategoryStruct.id (V i j hij))
  (cocycle :
    ∀ (i j k : J) (hij : i ≠ j) (hik : i ≠ k) (hjk : j ≠ k),
      CategoryTheory.CategoryStruct.comp (t' i j k hij hik hjk)
          (CategoryTheory.CategoryStruct.comp (t' j k i hjk ⋯ ⋯) (t' k i j ⋯ ⋯ hij)) =
        CategoryTheory.CategoryStruct.id (CategoryTheory.Limits.pullback (f i j hij) (f i k hik))),
  sizeOf
      { J := J, U := U, V := V, f := f, f_mono := f_mono, f_hasPullback := f_hasPullback, t := t, t' := t',
        t_fac := t_fac, t_inv := t_inv, cocycle := cocycle } =
    1 + sizeOf J
-- Mathlib.Topology.Connected.TotallyDisconnected
/-- The lift to `connectedComponents α` of a continuous map from `α` to a totally disconnected space
 -/
Continuous.connectedComponentsLift : {α : Type u} →
  {β : Type v} →
    [inst : TopologicalSpace α] →
      [inst_1 : TopologicalSpace β] →
        [TotallyDisconnectedSpace β] → {f : α → β} → Continuous f → ConnectedComponents α → β
-- Mathlib.Order.BooleanAlgebra.Set
Set.subset_sdiff : ∀ {α : Type u_1} {s t u : Set α}, s ⊆ t \ u ↔ s ⊆ t ∧ Disjoint s u
-- Mathlib.Algebra.Group.Shrink
Shrink.instPow : {M : Type u_1} → {α : Type u_2} → [inst : Small.{v, u_2} α] → [Pow α M] → Pow (Shrink.{v, u_2} α) M
-- Std.Sat.AIG.RelabelNat
/-- The translation `HashMap`
 -/
Std.Sat.AIG.RelabelNat.State.map : {α : Type} →
  [inst : DecidableEq α] →
    [inst_1 : Hashable α] →
      {decls : Array (Std.Sat.AIG.Decl α)} → {idx : ℕ} → Std.Sat.AIG.RelabelNat.State α decls idx → Std.HashMap α ℕ
-- Mathlib.RingTheory.AdicCompletion.Algebra
AdicCompletion.surjective_evalₐ : ∀ {R : Type u_1} [inst : CommRing R] (I : Ideal R) (n : ℕ), Function.Surjective ⇑(AdicCompletion.evalₐ I n)
-- Std.Sat.AIG.LawfulOperator
Std.Sat.AIG.ExtendingRefVecEntry : {α : Type} → [inst : Hashable α] → [inst_1 : DecidableEq α] → Std.Sat.AIG α → ℕ → Type
-- Aesop.Tree.Data
Aesop.GoalState.toEmoji : Aesop.GoalState → String
-- Mathlib.Data.Nat.PrimeFin
Nat.Coprime.primeFactors_mul : ∀ {a b : ℕ}, a.Coprime b → (a * b).primeFactors = a.primeFactors ∪ b.primeFactors
-- Mathlib.CategoryTheory.Adjunction.Basic
CategoryTheory.Adjunction.comp_unit_app : ∀ {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 C} {H : CategoryTheory.Functor D E} {I : CategoryTheory.Functor E D} (adj₁ : F ⊣ G)
  (adj₂ : H ⊣ I) (X : C),
  (adj₁.comp adj₂).unit.app X = CategoryTheory.CategoryStruct.comp (adj₁.unit.app X) (G.map (adj₂.unit.app (F.obj X)))
-- Mathlib.Geometry.Manifold.MFDeriv.Atlas
hasMFDerivWithinAt_extChartAt : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {H : Type u_3} [inst_3 : TopologicalSpace H] {I : ModelWithCorners 𝕜 E H} {M : Type u_4}
  [inst_4 : TopologicalSpace M] [inst_5 : ChartedSpace H M] [IsManifold I 1 M] {s : Set M} {x y : M},
  y ∈ (chartAt H x).source → HasMFDerivAt[s] (↑(extChartAt I x)) y (mfderiv% ↑(chartAt H x) y)
-- Std.Data.TreeSet.Lemmas
Std.TreeSet.get_max!_eq_max : ∀ {α : Type u} {cmp : α → α → Ordering} {t : Std.TreeSet α cmp} [inst : Std.TransCmp cmp] [inst_1 : Inhabited α]
  {hc : t.max! ∈ t}, t.get t.max! hc = t.max ⋯
-- Mathlib.MeasureTheory.Integral.Bochner.L1
MeasureTheory.L1.nnnorm_Integral_le_one : ∀ {α : Type u_1} {E : Type u_2} [inst : NormedAddCommGroup E] {m : MeasurableSpace α} {μ : MeasureTheory.Measure α}
  [inst_1 : NormedSpace ℝ E] [inst_2 : CompleteSpace E], ‖MeasureTheory.L1.integralCLM‖₊ ≤ 1
-- Mathlib.Algebra.Polynomial.Reverse
/-- `reflect N f` is the polynomial such that `(reflect N f).coeff i = f.coeff (revAt N i)`.
In other words, the terms with exponent `[0, ..., N]` now have exponent `[N, ..., 0]`.

In practice, `reflect` is only used when `N` is at least as large as the degree of `f`.

Eventually, it will be used with `N` exactly equal to the degree of `f`.  -/
Polynomial.reflect : {R : Type u_1} → [inst : Semiring R] → ℕ → Polynomial R → Polynomial R
-- Std.Data.DTreeMap.Internal.WF.Lemmas
Std.DTreeMap.Internal.Impl.WF.constAlter! : ∀ {α : Type u} {x : Ord α} {β : Type v} {t : Std.DTreeMap.Internal.Impl α fun x => β} {a : α} {f : Option β → Option β},
  t.WF → (Std.DTreeMap.Internal.Impl.Const.alter! a f t).WF
-- Init.Data.SInt.Bitwise
Int16.shiftRight_zero : ∀ {a : Int16}, a >>> 0 = a
-- Mathlib.Data.PNat.Basic
PNat.add_coe : ∀ (m n : ℕ+), ↑(m + n) = ↑m + ↑n
-- Mathlib.Analysis.Complex.UnitDisc.Basic
Complex.UnitClosedDisc.re_star : ∀ (z : Complex.UnitClosedDisc), (star z).re = z.re
-- Mathlib.GroupTheory.Congruence.Defs
AddCon.hasSub.eq_1 : ∀ {M : Type u_1} [inst : AddGroup M] (c : AddCon M), c.hasSub = { sub := Quotient.map₂ (fun x1 x2 => x1 - x2) ⋯ }
-- Std.Http.Data.Chunk
Std.Http.Chunk.mk.inj : ∀ {data : ByteArray} {extensions : Array (Std.Http.Chunk.ExtensionName × Option Std.Http.Chunk.ExtensionValue)}
  {data_1 : ByteArray} {extensions_1 : Array (Std.Http.Chunk.ExtensionName × Option Std.Http.Chunk.ExtensionValue)},
  { data := data, extensions := extensions } = { data := data_1, extensions := extensions_1 } →
    data = data_1 ∧ extensions = extensions_1
-- Mathlib.CategoryTheory.Monoidal.Action.Basic
CategoryTheory.MonoidalCategory.MonoidalRightAction.actionHomRight_inv_hom_assoc : ∀ {C : Type u_1} {D : Type u_2} [inst : CategoryTheory.Category.{v_1, u_1} C]
  [inst_1 : CategoryTheory.Category.{v_2, u_2} D] [inst_2 : CategoryTheory.MonoidalCategory C]
  [inst_3 : CategoryTheory.MonoidalCategory.MonoidalRightAction C D] (x : D) {y z : C} (f : y ≅ z) {Z : D}
  (h : CategoryTheory.MonoidalCategory.MonoidalRightActionStruct.actionObj x z ⟶ Z),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.MonoidalRightActionStruct.actionHomRight x f.inv)
      (CategoryTheory.CategoryStruct.comp
        (CategoryTheory.MonoidalCategory.MonoidalRightActionStruct.actionHomRight x f.hom) h) =
    h
-- Mathlib.Algebra.Lie.Ideal
LieIdeal.map_comap_le : ∀ {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] {f : L →ₗ⁅R⁆ L'} {J : LieIdeal R L'},
  LieIdeal.map f (LieIdeal.comap f J) ≤ J
-- Mathlib.NumberTheory.NumberField.CanonicalEmbedding.PolarCoord
NumberField.mixedEmbedding.polarCoordReal_target : ∀ (K : Type u_1) [inst : Field K] [inst_1 : NumberField K],
  (NumberField.mixedEmbedding.polarCoordReal K).target =
    Set.univ ×ˢ Set.univ.pi fun i => Set.Ioi 0 ×ˢ Set.Ioo (-Real.pi) Real.pi
-- Mathlib.CategoryTheory.Triangulated.TStructure.TruncLTGE
CategoryTheory.Triangulated.TStructure.triangleLTLTGELT_distinguished : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Preadditive C]
  [inst_2 : CategoryTheory.Limits.HasZeroObject C] [inst_3 : CategoryTheory.HasShift C ℤ]
  [inst_4 : ∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive] [inst_5 : CategoryTheory.Pretriangulated C]
  (t : CategoryTheory.Triangulated.TStructure C) [CategoryTheory.IsTriangulated C] (a b : ℤ) (h : a ≤ b) (X : C),
  (t.triangleLTLTGELT a b h).obj X ∈ CategoryTheory.Pretriangulated.distinguishedTriangles