mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.AlgebraicTopology.SimplicialSet.Degenerate
_private.Mathlib.AlgebraicTopology.SimplicialSet.Degenerate.0.SSet.unique_nonDegenerate.mono_g : ∀ {X : SSet} {n : ℕ} {x : X.obj (Opposite.op { len := n })} {m₁ m₂ : ℕ} {f₁ : { len := n } ⟶ { len := m₁ }}
  (hf₁ : CategoryTheory.SplitEpi f₁) {y₁ : ↑(X.nonDegenerate m₁)},
  x = (CategoryTheory.ConcreteCategory.hom (X.map f₁.op)) ↑y₁ →
    ∀ {f₂ : { len := n } ⟶ { len := m₂ }} {y₂ : X.obj (Opposite.op { len := m₂ })},
      x = (CategoryTheory.ConcreteCategory.hom (X.map f₂.op)) y₂ →
        CategoryTheory.Mono (SSet.unique_nonDegenerate.g✝ hf₁ f₂)
-- Mathlib.Algebra.MonoidAlgebra.Opposite
/-- The opposite of a monoid algebra is equivalent as a ring to the opposite monoid algebra over the
opposite ring.  -/
MonoidAlgebra.opRingEquiv : {R : Type u_1} →
  {M : Type u_2} → [inst : Semiring R] → [inst_1 : Mul M] → (MonoidAlgebra R M)ᵐᵒᵖ ≃+* MonoidAlgebra Rᵐᵒᵖ Mᵐᵒᵖ
-- Mathlib.MeasureTheory.Measure.TightNormed
/-- For a sequence of measures indexed by `ℕ`, the set of measures in the sequence is tight if and
only if the function `r : ℝ ↦ limsup (fun n ↦ μ n {x | r < ‖x‖}) atTop` tends to 0 at infinity.
Compared to `isTightMeasureSet_iff_tendsto_measure_norm_gt`, this lemma replaces a supremum over
all measures by a limsup. This is possible because the sequence is indexed by `ℕ`.  -/
MeasureTheory.isTightMeasureSet_range_iff_tendsto_limsup_measure_norm_gt : ∀ {E : Type u_1} {mE : MeasurableSpace E} [inst : NormedAddCommGroup E] [BorelSpace E] [ProperSpace E]
  {μ : ℕ → MeasureTheory.Measure E} [∀ (i : ℕ), MeasureTheory.IsFiniteMeasure (μ i)],
  MeasureTheory.IsTightMeasureSet (Set.range μ) ↔
    Filter.Tendsto (fun r => Filter.limsup (fun n => (μ n) {x | r < ‖x‖}) Filter.atTop) Filter.atTop (nhds 0)
-- Mathlib.Order.MinMax
MonotoneOn.map_min : ∀ {α : Type u} {β : Type v} [inst : LinearOrder α] [inst_1 : LinearOrder β] {f : α → β} {s : Set α} {a b : α},
  MonotoneOn f s → a ∈ s → b ∈ s → f (min a b) = min (f a) (f b)
-- Lean.Compiler.CSimpAttr
Lean.Compiler.CSimp.add : Lean.Name → Lean.AttributeKind → Lean.CoreM Unit
-- Mathlib.Algebra.Group.Pointwise.Set.Lattice
Set.smul_set_iUnion₂ : ∀ {α : Type u_2} {β : Type u_3} {ι : Sort u_5} {κ : ι → Sort u_6} [inst : SMul α β] (a : α) (s : (i : ι) → κ i → Set β),
  a • ⋃ i, ⋃ j, s i j = ⋃ i, ⋃ j, a • s i j
-- Mathlib.LinearAlgebra.Ray
/-- A nonnegative multiple of a vector is in the same ray as that vector.  -/
SameRay.sameRay_nonneg_smul_left : ∀ {R : Type u_1} [inst : CommSemiring R] [inst_1 : PartialOrder R] [inst_2 : IsStrictOrderedRing R] {M : Type u_2}
  [inst_3 : AddCommMonoid M] [inst_4 : Module R M] {S : Type u_5} [inst_5 : CommSemiring S] [inst_6 : PartialOrder S]
  [inst_7 : Algebra S R] [inst_8 : Module S M] [SMulPosMono S R] [IsScalarTower S R M] {a : S} (v : M),
  0 ≤ a → SameRay R (a • v) v
-- Std.Time.Time.Unit.Basic
/-- Converts a `Nanosecond.Offset` to a `Millisecond.Offset`.
 -/
Std.Time.Millisecond.Offset.ofNanoseconds : Std.Time.Nanosecond.Offset → Std.Time.Millisecond.Offset
-- Mathlib.Analysis.ODE.Basic
IsIntegralCurve.isIntegralCurveAt : ∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] {γ : ℝ → E} {v : ℝ → E → E},
  IsIntegralCurve γ v → ∀ (t : ℝ), IsIntegralCurveAt γ v t
-- Batteries.Recycling.RBTree.Basic
/-- `O(log n)`. Returns the key-value pair `(a, b)` such that `a ≤ k` for all keys in the RBMap.  -/
RBTree.RBMap.min? : {α : Type u} → {β : Type v} → {cmp : α → α → Ordering} → RBTree.RBMap α β cmp → Option (α × β)
-- Mathlib.AlgebraicGeometry.EllipticCurve.Affine.Point
WeierstrassCurve.Affine.Point.instInhabited : {R : Type r} → [inst : CommRing R] → {W' : WeierstrassCurve.Affine R} → Inhabited W'.Point
-- Mathlib.Data.List.Cycle
Cycle.prev.congr_simp : ∀ {α : Type u_1} [inst : DecidableEq α] (s s_1 : Cycle α) (e_s : s = s_1) (_hs : s.Nodup) (x x_1 : α) (e_x : x = x_1)
  (_hx : x ∈ s), s.prev _hs x _hx = s_1.prev ⋯ x_1 ⋯
-- Mathlib.Data.Set.Image
Subtype.image_preimage_val : ∀ {α : Type u_1} (s t : Set α), Subtype.val '' Subtype.val ⁻¹' t = s ∩ t
-- Std.Data.DTreeMap.Internal.WF.Lemmas
Std.DTreeMap.Internal.Impl.findCell_of_eq : ∀ {α : Type u} {β : α → Type v} [inst : Ord α] [Std.TransOrd α] {k : α → Ordering} [Std.Internal.IsStrictCut compare k]
  {sz : ℕ} {k' : α} {v' : β k'} {l r : Std.DTreeMap.Internal.Impl α β} (hcmp : k k' = Ordering.eq),
  (Std.DTreeMap.Internal.Impl.inner sz k' v' l r).Ordered →
    Std.DTreeMap.Internal.List.findCell (Std.DTreeMap.Internal.Impl.inner sz k' v' l r).toListModel k =
      Std.DTreeMap.Internal.Cell.ofEq k' v' ⋯
-- Mathlib.Algebra.MonoidAlgebra.Defs
AddMonoidAlgebra.nonUnitalNonAssocSemiring.eq_1 : ∀ {R : Type u_1} {M : Type u_4} [inst : Semiring R] [inst_1 : Add M],
  AddMonoidAlgebra.nonUnitalNonAssocSemiring =
    { toAddCommMonoid := AddMonoidAlgebra.instAddCommMonoid, toMul := AddMonoidAlgebra.instMul, left_distrib := ⋯,
      right_distrib := ⋯, zero_mul := ⋯, mul_zero := ⋯ }
-- Mathlib.CategoryTheory.Action.Monoidal
Action.diagonalSuccIsoTensorDiagonal_hom_hom : ∀ (G : Type u) [inst : Monoid G] (n : ℕ),
  (Action.diagonalSuccIsoTensorDiagonal G n).hom.hom = (Fin.consEquiv fun a => G).symm.toIso.hom
-- Mathlib.CategoryTheory.Monoidal.Action.Opposites
CategoryTheory.MonoidalCategory.MonoidalRightAction.monoidalOppositeRightAction_actionAssocIso_mop_mop : ∀ (C : Type u_1) (D : Type u_2) [inst : CategoryTheory.Category.{v_1, u_1} C]
  [inst_1 : CategoryTheory.MonoidalCategory C] [inst_2 : CategoryTheory.Category.{v_2, u_2} D]
  [inst_3 : CategoryTheory.MonoidalCategory.MonoidalLeftAction C D] (c c' : C) (d : D),
  CategoryTheory.MonoidalCategory.MonoidalRightActionStruct.actionAssocIso d { unmop := c } { unmop := c' } =
    CategoryTheory.MonoidalCategory.MonoidalLeftActionStruct.actionAssocIso c' c d
-- Mathlib.Analysis.Normed.Group.Basic
/-- **Alias** of the forward direction of `norm_div_eq_zero_iff`. -/
eq_of_norm_div_eq_zero : ∀ {E : Type u_5} [inst : NormedGroup E] {a b : E}, ‖a / b‖ = 0 → a = b
-- Mathlib.Data.Seq.Computation
Computation.results_of_terminates : ∀ {α : Type u} (s : Computation α) [_T : s.Terminates], s.Results s.get s.length
-- Mathlib.Topology.Algebra.RestrictedProduct.TopologicalSpace
RestrictedProduct.topologicalSpace_eq_of_bot : ∀ {ι : Type u_1} {R : ι → Type u_2} {A : (i : ι) → Set (R i)} [inst : (i : ι) → TopologicalSpace (R i)],
  RestrictedProduct.topologicalSpace R A ⊥ = TopologicalSpace.induced DFunLike.coe inferInstance
-- Mathlib.SetTheory.Cardinal.Cofinality.Ordinal
Ordinal.cof_univ : Ordinal.univ.{u, v}.cof = Cardinal.univ.{u, v}
-- Mathlib.CategoryTheory.SmallObject.TransfiniteCompositionLifting
CategoryTheory.HasLiftingProperty.transfiniteComposition.hasLiftingProperty_ι_app_bot : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {J : Type w} [inst_1 : LinearOrder J] [inst_2 : OrderBot J]
  {F : CategoryTheory.Functor J C} {c : CategoryTheory.Limits.Cocone F} (hc : CategoryTheory.Limits.IsColimit c)
  {X Y : C} {p : X ⟶ Y} [F.IsWellOrderContinuous] [inst_4 : SuccOrder J] [WellFoundedLT J],
  (∀ (j : J), ¬IsMax j → CategoryTheory.HasLiftingProperty (F.map (CategoryTheory.homOfLE ⋯)) p) →
    CategoryTheory.HasLiftingProperty (c.ι.app ⊥) p
-- Mathlib.Tactic.Convert
Convert.CheapConfig.toConfig : Convert.CheapConfig → Congr!.Config
-- Init.Data.Float.Model.Float
/-- Construct a `Float.Model` from its bit representation. This operation canonicalizes
all `NaN` inputs into the canonical `NaN`.
 -/
Float.Model.ofBits : UInt64 → Float.Model
-- Mathlib.Algebra.Category.Grp.EpiMono
GrpCat.SurjectiveOfEpiAuxs.XWithInfinity.fromCoset.sizeOf_spec : ∀ {A B : GrpCat} {f : A ⟶ B} (a : ↑(Set.range fun x => x • ↑(GrpCat.Hom.hom f).range)),
  sizeOf (GrpCat.SurjectiveOfEpiAuxs.XWithInfinity.fromCoset a) = 1 + sizeOf a
-- Mathlib.CategoryTheory.Triangulated.TStructure.TruncLTGE
CategoryTheory.Triangulated.TStructure.isGE_truncGE_obj : ∀ {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) (X : C) (a b : ℤ),
  autoParam (b ≤ a) CategoryTheory.Triangulated.TStructure.isGE_truncGE_obj._auto_1 → t.IsGE ((t.truncGE a).obj X) b
-- Init.Prelude
/-- The bitvector with value `i mod 2^n`.


Conventions for notations in identifiers:

 * The recommended spelling of `0#n` in identifiers is `zero` (not `ofNat_zero`).

 * The recommended spelling of `1#n` in identifiers is `one` (not `ofNat_one`). -/
BitVec.ofNat : (n : ℕ) → ℕ → BitVec n
-- Mathlib.RingTheory.Artinian.Module
IsArtinianRing.isMaximal_of_isPrime : ∀ {R : Type u_2} [inst : CommRing R] (p : Ideal R) [p.IsPrime] [IsArtinianRing R], p.IsMaximal
-- Std.Data.DHashMap.Lemmas
Std.DHashMap.singleton_eq_insert : ∀ {α : Type u} {β : α → Type v} {x : BEq α} {x_1 : Hashable α} {p : (a : α) × β a}, {p} = ∅.insert p.fst p.snd
-- Std.Data.Iterators.Lemmas.Equivalence.Basic
Std.IterM.Equiv.symm : ∀ {m : Type w → Type w'} {α₁ α₂ β : Type w} [inst : Monad m] [inst_1 : LawfulMonad m] [inst_2 : Std.Iterator α₁ m β]
  [inst_3 : Std.Iterator α₂ m β] {ita : Std.IterM m β} {itb : Std.IterM m β}, ita.Equiv itb → itb.Equiv ita
-- Std.Data.DHashMap.Lemmas
Std.DHashMap.Const.get?_eq_some_iff : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} {β : Type v} {m : Std.DHashMap α fun x => β} [EquivBEq α]
  [LawfulHashable α] {k : α} {v : β},
  Std.DHashMap.Const.get? m k = some v ↔ ∃ (h : k ∈ m), Std.DHashMap.Const.get m k h = v
-- Lean.Meta.Sym.SymM
/-- Cache for type-level canonicalization (reductions applied).  -/
Lean.Meta.Sym.Canon.State.cacheInType : Lean.Meta.Sym.Canon.State → Std.HashMap Lean.Expr Lean.Expr
-- Mathlib.Order.Category.OmegaCompletePartialOrder
ωCPO.instHasLimits : CategoryTheory.Limits.HasLimits ωCPO
-- Mathlib.CategoryTheory.Monoidal.DayConvolution
CategoryTheory.MonoidalCategory.DayConvolution.whiskerLeft_comp_unit_app_assoc : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {V : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} V]
  [inst_2 : CategoryTheory.MonoidalCategory C] [inst_3 : CategoryTheory.MonoidalCategory V]
  (F G : CategoryTheory.Functor C V) [inst_4 : CategoryTheory.MonoidalCategory.DayConvolution F G] (x : C) {y y' : C}
  (g : y ⟶ y') {Z : V}
  (h :
    (CategoryTheory.MonoidalCategory.DayConvolution.convolution F G).obj
        ((CategoryTheory.MonoidalCategory.tensor C).obj (x, y')) ⟶
      Z),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerLeft (F.obj x) (G.map g))
      (CategoryTheory.CategoryStruct.comp ((CategoryTheory.MonoidalCategory.DayConvolution.unit F G).app (x, y')) h) =
    CategoryTheory.CategoryStruct.comp ((CategoryTheory.MonoidalCategory.DayConvolution.unit F G).app (x, y))
      (CategoryTheory.CategoryStruct.comp
        ((CategoryTheory.MonoidalCategory.DayConvolution.convolution F G).map
          (CategoryTheory.MonoidalCategoryStruct.whiskerLeft x g))
        h)
-- Mathlib.Algebra.Order.Interval.Set.SuccPred
Set.insert_Ico_right_eq_Ico_add_one_of_not_isMax : ∀ {α : Type u_2} [inst : LinearOrder α] [inst_1 : One α] [inst_2 : Add α] [SuccAddOrder α] {a b : α},
  a ≤ b → ¬IsMax b → insert b (Set.Ico a b) = Set.Ico a (b + 1)
-- Mathlib.Algebra.Polynomial.Degree.Domain
Polynomial.not_dvd_of_natDegree_lt : ∀ {R : Type u} [inst : Semiring R] [NoZeroDivisors R] {p q : Polynomial R}, q ≠ 0 → q.natDegree < p.natDegree → ¬p ∣ q
-- Mathlib.Topology.ContinuousMap.ContinuousMapZero
ContinuousMapZero.instNorm : {α : Type u_1} →
  {R : Type u_3} →
    [inst : TopologicalSpace α] →
      [CompactSpace α] → [inst_2 : Zero α] → [inst_3 : NormedAddCommGroup R] → Norm (ContinuousMapZero α R)
-- Mathlib.Algebra.Category.Grp.Basic
/-- Typecheck a `MonoidHom` as a morphism in `CommGrpCat`.  -/
CommGrpCat.ofHom : {X Y : Type u} → [inst : CommGroup X] → [inst_1 : CommGroup Y] → (X →* Y) → (CommGrpCat.of X ⟶ CommGrpCat.of Y)
-- Mathlib.Analysis.Distribution.DerivNotation
LineDeriv.tensorLineDerivTwo_canonicalCovariantTensor_eq_sum : ∀ {ι : Type u_1} {E : Type u_6} {V₁ : Type u_8} {V₂ : Type u_9} {V₃ : Type u_10} [inst : LineDeriv E V₁ V₂]
  [inst_1 : LineDeriv E V₂ V₃] [inst_2 : AddCommGroup V₁] [inst_3 : AddCommGroup V₂] [inst_4 : AddCommGroup V₃]
  [inst_5 : NormedAddCommGroup E] [inst_6 : InnerProductSpace ℝ E] [inst_7 : FiniteDimensional ℝ E]
  [inst_8 : Module ℝ V₂] [inst_9 : Module ℝ V₃] [inst_10 : LineDerivAdd E V₁ V₂] [inst_11 : LineDerivAdd E V₂ V₃]
  [inst_12 : LineDerivSMul ℝ E V₂ V₃] [inst_13 : LineDerivLeftSMul ℝ E V₁ V₂] [inst_14 : LineDerivLeftSMul ℝ E V₂ V₃]
  [inst_15 : Fintype ι] (v : OrthonormalBasis ι ℝ E) (f : V₁),
  (LineDeriv.tensorLineDerivTwo ℝ f) (InnerProductSpace.canonicalCovariantTensor E) =
    ∑ i, LineDeriv.lineDerivOp (v i) (LineDeriv.lineDerivOp (v i) f)
-- Std.Time.Date.Unit.Day
Std.Time.Day.instDecidableLtOrdinal : {x y : Std.Time.Day.Ordinal} → Decidable (x < y)
-- Init.Data.Slice.Operations
/-- Returns the number of elements with distinct indices in the given slice.

Example: `#[1, 1, 1][0...2].size = 2`.
 -/
Std.Slice.size : {γ : Type u_1} → Std.Slice γ → [Std.Slice.SliceSize γ] → ℕ
-- Mathlib.Topology.UniformSpace.Defs
/-- The uniformity agrees with the topology: the neighborhoods filter of each point `x`
is equal to `Filter.comap (Prod.mk x) (𝓤 α)`.  -/
UniformSpace.nhds_eq_comap_uniformity : ∀ {α : Type u} [self : UniformSpace α] (x : α), nhds x = Filter.comap (Prod.mk x) UniformSpace.uniformity
-- Mathlib.CategoryTheory.EquivalenceRelation
CategoryTheory.SymmetricRelation.symmetry₁ : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] {R X : C} {p₁ p₂ : R ⟶ X}
  (self : CategoryTheory.SymmetricRelation p₁ p₂), CategoryTheory.CategoryStruct.comp self.s p₁ = p₂
-- Mathlib.NumberTheory.NumberField.Ideal.Basic
Ideal.rootsOfUnityMapQuot_apply : ∀ {K : Type u_1} [inst : Field K] (I : Ideal (NumberField.RingOfIntegers K)) (n : ℕ)
  {x : (NumberField.RingOfIntegers K)ˣ} (hx : x ∈ rootsOfUnity n (NumberField.RingOfIntegers K)),
  ↑((I.rootsOfUnityMapQuot n) ⟨x, hx⟩) = (Ideal.Quotient.mk I) ↑x
-- Mathlib.MeasureTheory.Integral.CircleIntegral
/-- The function we actually integrate over `[0, 2π]` in the definition of `circleIntegral` is
integrable.  -/
CircleIntegrable.out : ∀ {E : Type u_1} [inst : NormedAddCommGroup E] {f : ℂ → E} {c : ℂ} {R : ℝ} [inst_1 : NormedSpace ℂ E],
  CircleIntegrable f c R →
    IntervalIntegrable (fun θ => deriv (circleMap c R) θ • f (circleMap c R θ)) MeasureTheory.volume 0 (2 * Real.pi)
-- Mathlib.Algebra.Category.Grp.Basic
CommGrpCat.forget₂_commMonCat_map_ofHom : ∀ {X Y : Type u} [inst : CommGroup X] [inst_1 : CommGroup Y] (f : X →* Y),
  (CategoryTheory.forget₂ CommGrpCat CommMonCat).map (CommGrpCat.ofHom f) = CommMonCat.ofHom f
-- Mathlib.NumberTheory.PellMatiyasevic
Pell.yz_succ_succ : ∀ {a : ℕ} (a1 : 1 < a) (n : ℕ), Pell.yz a1 (n + 2) = ↑(2 * a) * Pell.yz a1 (n + 1) - Pell.yz a1 n
-- Mathlib.Algebra.SkewPolynomial.Basic
SkewPolynomial.coeff_one : ∀ {R : Type u_1} [inst : Semiring R] [MulSemiringAction (Multiplicative ℕ) R] (n : ℕ),
  SkewPolynomial.coeff 1 n = if 0 = n then 1 else 0
-- Mathlib.Data.Finset.Sigma
Finset.sigmaLift.eq_1 : ∀ {ι : Type u_1} {α : ι → Type u_2} {β : ι → Type u_3} {γ : ι → Type u_4} [inst : DecidableEq ι]
  (f : ⦃i : ι⦄ → α i → β i → Finset (γ i)) (a : Sigma α) (b : Sigma β),
  Finset.sigmaLift f a b =
    if h : a.fst = b.fst then Finset.map (Function.Embedding.sigmaMk b.fst) (f (h ▸ a.snd) b.snd) else ∅
-- Mathlib.Topology.Compactification.OnePoint.Basic
OnePoint.isOpen_iff_of_notMem : ∀ {X : Type u_1} [inst : TopologicalSpace X] {s : Set (OnePoint X)},
  OnePoint.infty ∉ s → (IsOpen s ↔ IsOpen (OnePoint.some ⁻¹' s))
-- Mathlib.Data.Matrix.Basic
/-- A version of `Set.matrix` for `AddSubgroup`s.
Given an `AddSubgroup` `S`, `S.matrix` is the `AddSubgroup` of matrices `m`
all of whose entries `m i j` belong to `S`.  -/
AddSubgroup.matrix : {m : Type u_2} → {n : Type u_3} → {A : Type u_14} → [inst : AddGroup A] → AddSubgroup A → AddSubgroup (Matrix m n A)
-- Mathlib.LinearAlgebra.SesquilinearForm.Basic
/-- Strict **Cauchy-Schwarz** is equivalent to linear independence for positive definite forms.  -/
LinearMap.BilinForm.apply_mul_apply_lt_iff_linearIndependent : ∀ {R : Type u_1} {M : Type u_5} [inst : CommRing R] [inst_1 : LinearOrder R] [IsStrictOrderedRing R]
  [inst_3 : AddCommGroup M] [inst_4 : Module R M] (B : LinearMap.BilinForm R M) [Module.IsTorsionFree R M],
  (∀ (x : M), x ≠ 0 → 0 < (B x) x) → ∀ (x y : M), (B x) y * (B y) x < (B x) x * (B y) y ↔ LinearIndependent R ![x, y]
-- Mathlib.Order.Partition.Finpartition
Finpartition.part_nonempty : ∀ {α : Type u_1} [inst : DecidableEq α] {s : Finset α} (P : Finpartition s) {a : α}, (P.part a).Nonempty ↔ a ∈ s
-- Init.Data.UInt.Lemmas
UInt32.toFin_add : ∀ (a b : UInt32), (a + b).toFin = a.toFin + b.toFin
-- Lean.Data.Lsp.Internal
Lean.Lsp.instToJsonLeanIdentifier.toJson : Lean.Lsp.LeanIdentifier → Lean.Json
-- Mathlib.Order.Disjointed
/-- Note this lemma does not require `¬IsMax i`, unlike `disjointed_succ`.  -/
Monotone.disjointed_succ_sup : ∀ {α : Type u_1} {ι : Type u_2} [inst : GeneralizedBooleanAlgebra α] [inst_1 : LinearOrder ι]
  [inst_2 : LocallyFiniteOrderBot ι] [inst_3 : SuccOrder ι] {f : ι → α},
  Monotone f → ∀ (i : ι), disjointed f (Order.succ i) ⊔ f i = f (Order.succ i)
-- Mathlib.Combinatorics.SimpleGraph.Maps
SimpleGraph.Iso.map_mem_edgeSet_iff : ∀ {V : Type u_1} {W : Type u_2} {G : SimpleGraph V} {G' : SimpleGraph W} (f : G ≃g G') {e : Sym2 V},
  Sym2.map (⇑f) e ∈ G'.edgeSet ↔ e ∈ G.edgeSet
-- Init.Data.Order.PackageFactories
Std.LinearPreorderPackage.toPreorderPackage : {α : Type u} → [self : Std.LinearPreorderPackage α] → Std.PreorderPackage α
-- Mathlib.GroupTheory.Congruence.Defs
/-- Defining the quotient by an additive congruence relation of a type with
an addition.  -/
AddCon.Quotient : {M : Type u_1} → [inst : Add M] → AddCon M → Type u_1
-- Mathlib.RingTheory.PowerSeries.Inverse
/-- The inverse 1/f of a power series f defined over a field  -/
PowerSeries.inv : {k : Type u_2} → [Field k] → PowerSeries k → PowerSeries k
-- Mathlib.Order.Lex
Colex.exists : ∀ {α : Type u_1} {p : Colex α → Prop}, (∃ a, p a) ↔ ∃ a, p (toColex a)
-- Mathlib.Algebra.Group.Action.Defs
Commute.smul_right : ∀ {M : Type u_1} {α : Type u_5} [inst : SMul M α] [inst_1 : Mul α] [SMulCommClass M α α] [IsScalarTower M α α]
  {a b : α}, Commute a b → ∀ (r : M), Commute a (r • b)
-- Mathlib.Algebra.Ring.Equiv
RingEquiv.prodCongr_symm_apply : ∀ {R : Type u_7} {R' : Type u_8} {S : Type u_9} {S' : Type u_10} [inst : NonUnitalNonAssocSemiring R]
  [inst_1 : NonUnitalNonAssocSemiring R'] [inst_2 : NonUnitalNonAssocSemiring S] [inst_3 : NonUnitalNonAssocSemiring S']
  (f : R ≃+* R') (g : S ≃+* S') (a : R' × S'), (f.prodCongr g).symm a = Prod.map (⇑f.symm) (⇑g.symm) a
-- Mathlib.Topology.Algebra.Module.ContinuousLinearMap.Restrict
ContinuousLinearMap.subtypeL_comp_restrict : ∀ {R₁ : Type u_1} {R₂ : Type u_2} [inst : Semiring R₁] [inst_1 : Semiring R₂] {σ₁₂ : R₁ →+* R₂} {M₁ : Type u_4}
  {M₂ : Type u_5} [inst_2 : TopologicalSpace M₁] [inst_3 : AddCommMonoid M₁] [inst_4 : Module R₁ M₁]
  [inst_5 : TopologicalSpace M₂] [inst_6 : AddCommMonoid M₂] [inst_7 : Module R₂ M₂] {f : M₁ →SL[σ₁₂] M₂}
  {p : Submodule R₁ M₁} {q : Submodule R₂ M₂} (hf : ∀ x ∈ p, f x ∈ q), q.subtypeL ∘SL f.restrict hf = f.domRestrict p
-- Mathlib.Topology.ClusterPt
ClusterPt.of_inf_right : ∀ {X : Type u} [inst : TopologicalSpace X] {x : X} {f g : Filter X}, ClusterPt x (f ⊓ g) → ClusterPt x g
-- Lean.Data.Lsp.Internal
/-- Used in the `$/lean/ileanInfoUpdate` and `$/lean/ileanInfoFinal` watchdog <- worker notifications.
Contains the definitions and references of the file managed by a worker.
 -/
Lean.Lsp.LeanIleanInfoParams : Type
-- Mathlib.Order.BooleanSubalgebra
BooleanSubalgebra.map_top : ∀ {α : Type u_2} {β : Type u_3} [inst : BooleanAlgebra α] [inst_1 : BooleanAlgebra β] (f : BoundedLatticeHom α β),
  Function.Surjective ⇑f → BooleanSubalgebra.map f ⊤ = ⊤
-- Std.Time.Zoned.TimeZone
Std.Time.instReprTimeZone : Repr Std.Time.TimeZone
-- Mathlib.Data.Ordmap.Invariants
/-- Concatenate two nodes, performing a right rotation `(x y) z -> (x (y z))`
if balance is upset.  -/
Ordnode.rotateR : {α : Type u_1} → Ordnode α → α → Ordnode α → Ordnode α
-- Mathlib.MeasureTheory.Integral.FinMeasAdditive
MeasureTheory.DominatedFinMeasAdditive.neg : ∀ {α : Type u_1} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} {β : Type u_7} [inst : SeminormedAddCommGroup β]
  {T : Set α → β} {C : ℝ},
  MeasureTheory.DominatedFinMeasAdditive μ T C → MeasureTheory.DominatedFinMeasAdditive μ (-T) C
-- Mathlib.Data.Set.Function
Set.SurjOn.comap_nonempty : ∀ {α : Type u_1} {β : Type u_2} {s : Set α} {t : Set β} {f : α → β}, Set.SurjOn f s t → t.Nonempty → s.Nonempty
-- Mathlib.CategoryTheory.Bicategory.Product
/-- `Bicategory.uniformProd B C` is an additional instance specialised so both factors have the same
universe levels. This helps typeclass resolution.
 -/
CategoryTheory.Bicategory.uniformProd : (B : Type u₁) →
  [CategoryTheory.Bicategory B] → (C : Type u₁) → [CategoryTheory.Bicategory C] → CategoryTheory.Bicategory (B × C)
-- Mathlib.Algebra.Group.Defs
AddCancelMonoid.toAddRightCancelMonoid : {M : Type u} → [self : AddCancelMonoid M] → AddRightCancelMonoid M
-- Mathlib.CategoryTheory.Abelian.GrothendieckCategory.ColimCoyoneda
/-- If `X` is an object in a Grothendieck abelian category, then
the functor `coyoneda.obj (op X)` commutes with colimits corresponding
to diagrams of monomorphisms indexed by `κ`-filtered categories
for a big enough regular cardinal `κ`.  -/
CategoryTheory.IsGrothendieckAbelian.preservesColimit_coyoneda_obj_of_mono : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Abelian C]
  [CategoryTheory.IsGrothendieckAbelian.{w, v, u} C] {X : C} {J : Type w} [inst_3 : CategoryTheory.SmallCategory J]
  (Y : CategoryTheory.Functor J C) {κ : Cardinal.{w}} [hκ : Fact κ.IsRegular] [CategoryTheory.IsCardinalFiltered J κ],
  HasCardinalLT (CategoryTheory.Subobject X) κ →
    ∀ [∀ (j j' : J) (φ : j ⟶ j'), CategoryTheory.Mono (Y.map φ)],
      CategoryTheory.Limits.PreservesColimit Y (CategoryTheory.coyoneda.obj (Opposite.op X))
-- Mathlib.Combinatorics.Matroid.Map
Matroid.comap_loopyOn : ∀ {α : Type u_1} {β : Type u_2} (f : α → β) (E : Set β), (Matroid.loopyOn E).comap f = Matroid.loopyOn (f ⁻¹' E)
-- Mathlib.Algebra.Order.Ring.Synonym
ofLex_ofNat : ∀ {R : Type u_1} [inst : NatCast R] (n : ℕ) [inst_1 : n.AtLeastTwo], ofLex (OfNat.ofNat n) = OfNat.ofNat n
-- Mathlib.Topology.Order.Hom.Basic
ContinuousOrderHom.cancel_left : ∀ {α : Type u_2} {β : Type u_3} {γ : Type u_4} [inst : TopologicalSpace α] [inst_1 : Preorder α]
  [inst_2 : TopologicalSpace β] [inst_3 : Preorder β] [inst_4 : TopologicalSpace γ] [inst_5 : Preorder γ] {g : β →Co γ}
  {f₁ f₂ : α →Co β}, Function.Injective ⇑g → (g.comp f₁ = g.comp f₂ ↔ f₁ = f₂)
-- Std.Data.ExtTreeMap.Lemmas
Std.ExtTreeMap.size_map : ∀ {α : Type u} {β : Type v} {γ : Type w} {cmp : α → α → Ordering} {t : Std.ExtTreeMap α β cmp} [Std.TransCmp cmp]
  {f : α → β → γ}, (Std.ExtTreeMap.map f t).size = t.size
-- Mathlib.MeasureTheory.Function.AEEqFun
MeasureTheory.AEEqFun.quot_mk_eq_mk : ∀ {α : Type u_1} {β : Type u_2} [inst : MeasurableSpace α] {μ : MeasureTheory.Measure α} [inst_1 : TopologicalSpace β]
  (f : α → β) (hf : MeasureTheory.AEStronglyMeasurable f μ),
  Quot.mk ⇑(MeasureTheory.Measure.aeEqSetoid β μ) ⟨f, hf⟩ = MeasureTheory.AEEqFun.mk f hf
-- Mathlib.AlgebraicGeometry.GammaSpecAdjunction
AlgebraicGeometry.Spec.preimage_comp : ∀ {R S T : CommRingCat} (f : AlgebraicGeometry.Spec R ⟶ AlgebraicGeometry.Spec S)
  (g : AlgebraicGeometry.Spec S ⟶ AlgebraicGeometry.Spec T),
  AlgebraicGeometry.Spec.preimage (CategoryTheory.CategoryStruct.comp f g) =
    CategoryTheory.CategoryStruct.comp (AlgebraicGeometry.Spec.preimage g) (AlgebraicGeometry.Spec.preimage f)
-- Init.Data.String.Lemmas.FindPos
String.Slice.lt_posGT_iff : ∀ {s : String.Slice} {p : String.Pos.Raw} {h : p < s.rawEndPos} {q : s.Pos}, q < s.posGT p h ↔ q.offset ≤ p