mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.RingTheory.MvPowerSeries.Substitution
MvPowerSeries.subst_coe : ∀ {σ : Type u_1} {R : Type u_3} [inst : CommRing R] {τ : Type u_4} {S : Type u_5} [inst_1 : CommRing S]
  [inst_2 : Algebra R S] {a : σ → MvPowerSeries τ S} (p : MvPolynomial σ R),
  MvPowerSeries.subst a ↑p = (MvPolynomial.aeval a) p
-- Mathlib.Data.Nat.Squarefree
Nat.sum_divisors_filter_squarefree : ∀ {n : ℕ},
  n ≠ 0 →
    ∀ {α : Type u_1} [inst : AddCommMonoid α] {f : ℕ → α},
      ∑ d ∈ n.divisors with Squarefree d, f d =
        ∑ i ∈ (UniqueFactorizationMonoid.normalizedFactors n).toFinset.powerset, f i.val.prod
-- Std.Time.Format.Modifier
Std.Time.Text.noConfusionType : Sort v✝ → Std.Time.Text → Std.Time.Text → Sort v✝
-- Mathlib.GroupTheory.FreeGroup.Basic
FreeGroup.Red.to_append_iff : ∀ {α : Type u} {L L₁ L₂ : List (α × Bool)},
  FreeGroup.Red L (L₁ ++ L₂) ↔ ∃ L₃ L₄, L = L₃ ++ L₄ ∧ FreeGroup.Red L₃ L₁ ∧ FreeGroup.Red L₄ L₂
-- Init.Data.Int.Linear
Int.Internal.Linear.dvd_solve_elim : ∀ (ctx : Int.Internal.Linear.Context) (d₁ : ℤ) (p₁ : Int.Internal.Linear.Poly) (d₂ : ℤ) (p₂ : Int.Internal.Linear.Poly)
  (d : ℤ) (p : Int.Internal.Linear.Poly),
  Int.Internal.Linear.dvd_solve_elim_cert d₁ p₁ d₂ p₂ d p = true →
    d₁ ∣ Int.Internal.Linear.Poly.denote' ctx p₁ →
      d₂ ∣ Int.Internal.Linear.Poly.denote' ctx p₂ → d ∣ Int.Internal.Linear.Poly.denote' ctx p
-- Mathlib.CategoryTheory.Monoidal.Internal.Limits
/-- Implementation of `Mon.hasLimits`: a limiting cone over a functor `F : J ⥤ Mon C`.
 -/
CategoryTheory.Mon.limitCone : {J : Type w} →
  [inst : CategoryTheory.Category.{v_1, w} J] →
    {C : Type u} →
      [inst_1 : CategoryTheory.Category.{v, u} C] →
        [inst_2 : CategoryTheory.MonoidalCategory C] →
          (F : CategoryTheory.Functor J (CategoryTheory.Mon C)) →
            (c : CategoryTheory.Limits.Cone (F.comp (CategoryTheory.Mon.forget C))) →
              CategoryTheory.Limits.IsLimit c → CategoryTheory.Limits.Cone F
-- Mathlib.Algebra.Notation.Pi.Basic
Pi.mulSingle_eq_one_iff : ∀ {ι : Type u_1} {M : ι → Type u_6} [inst : (i : ι) → One (M i)] [inst_1 : DecidableEq ι] {i : ι} {x : M i},
  Pi.mulSingle i x = 1 ↔ x = 1
-- Mathlib.LinearAlgebra.BilinearForm.TensorProduct
/-- The base change of a symmetric bilinear form is symmetric.  -/
LinearMap.BilinForm.IsSymm.baseChange : ∀ {R : Type uR} (A : Type uA) {M₂ : Type uM₂} [inst : CommSemiring R] [inst_1 : CommSemiring A]
  [inst_2 : AddCommMonoid M₂] [inst_3 : Algebra R A] [inst_4 : Module R M₂] {B₂ : LinearMap.BilinForm R M₂},
  LinearMap.IsSymm B₂ → LinearMap.IsSymm (LinearMap.BilinForm.baseChange A B₂)
-- Lean.Meta.Tactic.Grind.Arith.Cutsat.ToIntInfo
Lean.Meta.Grind.Arith.Cutsat.ToIntTermInfo.mk.sizeOf_spec : ∀ (eToInt α he : Lean.Expr), sizeOf { eToInt := eToInt, α := α, he := he } = 1 + sizeOf eToInt + sizeOf α + sizeOf he
-- Mathlib.Geometry.Euclidean.Circumcenter
/-- All n-simplices among cospherical points in an n-dimensional
subspace have the same circumsphere.  -/
EuclideanGeometry.exists_circumsphere_eq_of_cospherical_subset : ∀ {V : Type u_1} {P : Type u_2} [inst : NormedAddCommGroup V] [inst_1 : InnerProductSpace ℝ V] [inst_2 : MetricSpace P]
  [inst_3 : NormedAddTorsor V P] {s : AffineSubspace ℝ P} {ps : Set P},
  ps ⊆ ↑s →
    ∀ [Nonempty ↥s] {n : ℕ} [FiniteDimensional ℝ ↥s.direction],
      Module.finrank ℝ ↥s.direction = n →
        EuclideanGeometry.Cospherical ps →
          ∃ c, ∀ (sx : Affine.Simplex ℝ P n), Set.range sx.points ⊆ ps → sx.circumsphere = c
-- Mathlib.NumberTheory.PythagoreanTriples
sq_ne_two_fin_zmod_four : ∀ (z : ZMod 4), z * z ≠ 2
-- Mathlib.Probability.BorelCantelli
ProbabilityTheory.iIndepFun.indep_comap_natural_of_lt : ∀ {Ω : Type u_1} {m0 : MeasurableSpace Ω} {μ : MeasureTheory.Measure Ω} {ι : Type u_2} {β : Type u_3}
  [inst : LinearOrder ι] [mβ : MeasurableSpace β] [inst_1 : NormedAddCommGroup β] [inst_2 : BorelSpace β]
  {f : ι → Ω → β} {i j : ι} (hf : ∀ (i : ι), MeasureTheory.StronglyMeasurable (f i)),
  ProbabilityTheory.iIndepFun f μ →
    i < j → ProbabilityTheory.Indep (MeasurableSpace.comap (f j) mβ) (↑(MeasureTheory.Filtration.natural f hf) i) μ
-- Mathlib.CategoryTheory.Limits.Over
/-- If `c` is a colimit cocone, then so is the cocone `c.toOver` with cocone point `𝟙 c.pt`.  -/
CategoryTheory.Over.isColimitToOver : {J : Type w} →
  [inst : CategoryTheory.Category.{w', w} J] →
    {C : Type u} →
      [inst_1 : CategoryTheory.Category.{v, u} C] →
        {F : CategoryTheory.Functor J C} →
          {c : CategoryTheory.Limits.Cocone F} →
            CategoryTheory.Limits.IsColimit c → CategoryTheory.Limits.IsColimit c.toOver
-- Mathlib.Algebra.Homology.Embedding.ExtendHomology
HomologicalComplex.extend.rightHomologyData_ι : ∀ {ι : Type u_1} {ι' : Type u_2} {c : ComplexShape ι} {c' : ComplexShape ι'} {C : Type u_3}
  [inst : CategoryTheory.Category.{v_1, u_3} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  [inst_2 : CategoryTheory.Limits.HasZeroObject C] (K : HomologicalComplex C c) (e : c.Embedding c') {i j k : ι}
  {i' j' k' : ι'} (hj' : e.f j = j') (hi : c.prev j = i) (hi' : c'.prev j' = i') (hk : c.next j = k)
  (hk' : c'.next j' = k') (h : (K.sc' i j k).RightHomologyData),
  (HomologicalComplex.extend.rightHomologyData K e hj' hi hi' hk hk' h).ι = h.ι
-- Mathlib.Data.List.Sym
_private.Mathlib.Data.List.Sym.0.List.sym.match_1.eq_3 : ∀ {α : Type u_1} (motive : ℕ → List α → Sort u_2) (n : ℕ) (x : α) (xs : List α) (h_1 : (x : List α) → motive 0 x)
  (h_2 : (x : ℕ) → motive x []) (h_3 : (n : ℕ) → (x : α) → (xs : List α) → motive n.succ (x :: xs)),
  (match n.succ, x :: xs with
    | 0, x => h_1 x
    | x, [] => h_2 x
    | n.succ, x :: xs => h_3 n x xs) =
    h_3 n x xs
-- Lean.Meta.Basic
Lean.Meta.isDefEqStuckExceptionId : Lean.InternalExceptionId
-- Mathlib.RingTheory.Coprime.Basic
IsCoprime.of_mul_right_left : ∀ {R : Type u} [inst : CommSemiring R] {x y z : R}, IsCoprime x (y * z) → IsCoprime x y
-- Mathlib.LinearAlgebra.DirectSum.TensorProduct
TensorProduct.directSum_lof_tmul_lof : ∀ (R : Type u) [inst : CommSemiring R] (S : Type u_1) [inst_1 : Semiring S] [inst_2 : Algebra R S] {ι₁ : Type v₁}
  {ι₂ : Type v₂} [inst_3 : DecidableEq ι₁] [inst_4 : DecidableEq ι₂] {M₁ : ι₁ → Type w₁} {M₂ : ι₂ → Type w₂}
  [inst_5 : (i₁ : ι₁) → AddCommMonoid (M₁ i₁)] [inst_6 : (i₂ : ι₂) → AddCommMonoid (M₂ i₂)]
  [inst_7 : (i₁ : ι₁) → Module R (M₁ i₁)] [inst_8 : (i₂ : ι₂) → Module R (M₂ i₂)]
  [inst_9 : (i₁ : ι₁) → Module S (M₁ i₁)] [inst_10 : ∀ (i₁ : ι₁), IsScalarTower R S (M₁ i₁)] (i₁ : ι₁) (m₁ : M₁ i₁)
  (i₂ : ι₂) (m₂ : M₂ i₂),
  (TensorProduct.directSum R S M₁ M₂) ((DirectSum.lof S ι₁ M₁ i₁) m₁ ⊗ₜ[R] (DirectSum.lof R ι₂ M₂ i₂) m₂) =
    (DirectSum.lof S (ι₁ × ι₂) (fun i => TensorProduct R (M₁ i.1) (M₂ i.2)) (i₁, i₂)) (m₁ ⊗ₜ[R] m₂)
-- Init.Data.Vector.Lemmas
Vector.contains_iff_exists_mem_beq : ∀ {α : Type u_1} {n : ℕ} [inst : BEq α] {xs : Vector α n} {a : α}, xs.contains a = true ↔ ∃ a' ∈ xs, (a == a') = true
-- Mathlib.Order.WithBot
WithBot.unbotD.eq_1 : ∀ {α : Type u_1} (d : α) (x : WithBot α), WithBot.unbotD d x = WithBot.recBotCoe d id x
-- Std.Data.DTreeMap.Raw.Lemmas
Std.DTreeMap.Raw.Const.toList_map : ∀ {α : Type u} {cmp : α → α → Ordering} {β : Type v} {γ : Type w} {t : Std.DTreeMap.Raw α (fun x => β) cmp}
  {f : α → β → γ},
  Std.DTreeMap.Raw.Const.toList (Std.DTreeMap.Raw.map f t) =
    List.map (fun p => (p.1, f p.1 p.2)) (Std.DTreeMap.Raw.Const.toList t)
-- Init.Data.List.MinMaxIdx
List.maxIdxOn?_cons_eq_some_maxIdxOn : ∀ {β : Type u_1} {α : Type u_2} [inst : LE β] [inst_1 : DecidableLE β] {f : α → β} {x : α} {xs : List α},
  List.maxIdxOn? f (x :: xs) = some (List.maxIdxOn f (x :: xs) ⋯)
-- Lean.PrettyPrinter.Delaborator.Builtins
Lean.PrettyPrinter.Delaborator.delabNameMkNum : Lean.PrettyPrinter.Delaborator.Delab
-- Mathlib.RingTheory.Nilpotent.GeometricallyReduced
Algebra.IsGeometricallyReduced.of_injective : ∀ {k : Type u_1} {A : Type u_2} [inst : Field k] [inst_1 : Ring A] [inst_2 : Algebra k A] {B : Type u_3}
  [inst_3 : Ring B] [inst_4 : Algebra k B] (f : A →ₐ[k] B),
  Function.Injective ⇑f → ∀ [Algebra.IsGeometricallyReduced k B], Algebra.IsGeometricallyReduced k A
-- Init.Data.Repr
instReprSubtype : {α : Type u_1} → {p : α → Prop} → [Repr α] → Repr (Subtype p)
-- Mathlib.LinearAlgebra.Ray
/-- If two vectors are on the same ray then they remain so after applying a linear map.  -/
SameRay.map : ∀ {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] {N : Type u_3} [inst_5 : AddCommMonoid N] [inst_6 : Module R N]
  {x y : M} (f : M →ₗ[R] N), SameRay R x y → SameRay R (f x) (f y)
-- Init.Data.UInt.Lemmas
UInt8.ofBitVec_uSizeToBitVec : ∀ (n : USize), { toBitVec := BitVec.setWidth 8 n.toBitVec } = n.toUInt8
-- Mathlib.Algebra.Order.Group.Unbundled.Basic
neg_le_sub_iff_le_add' : ∀ {α : Type u} [inst : AddCommGroup α] [inst_1 : LE α] [AddLeftMono α] {a b c : α}, -a ≤ b - c ↔ c ≤ a + b
-- Mathlib.LinearAlgebra.Matrix.Hermitian
Matrix.IsHermitian.fromBlocks₁₁ : ∀ {α : Type u_1} {m : Type u_3} {n : Type u_4} [inst : CommRing α] [inst_1 : StarRing α] [inst_2 : Fintype m]
  [inst_3 : DecidableEq m] {A : Matrix m m α} (B : Matrix m n α) (D : Matrix n n α),
  A.IsHermitian → ((Matrix.fromBlocks A B B.conjTranspose D).IsHermitian ↔ (D - B.conjTranspose * A⁻¹ * B).IsHermitian)
-- Mathlib.Combinatorics.Matroid.Minor.Contract
Matroid.IsBasis.contract_isBasis_of_disjoint_indep : ∀ {α : Type u_1} {M : Matroid α} {I J X : Set α},
  M.IsBasis I X → Disjoint J X → M.Indep (I ∪ J) → (M.contract J).IsBasis I X
-- Mathlib.Data.Num.Lemmas
Num.bit1_succ : ∀ (n : Num), n.bit1.succ = n.succ.bit0
-- Std.Http.Data.Body.Stream
_private.Std.Http.Data.Body.Stream.0.Std.Http.Body.Stream.collapseForSend : Std.Http.Body.Stream → Std.Http.Chunk → Bool → BaseIO (Except IO.Error (Option Std.Http.Chunk))
-- Mathlib.Order.Defs.Unbundled
rel_congr_right : ∀ {α : Sort u_1} {r : α → α → Prop} [Std.Symm r] [IsTrans α r] {a b c : α}, r b c → (r a b ↔ r a c)
-- Mathlib.Algebra.Group.Subsemigroup.Operations
AddSubsemigroup.map_id : ∀ {M : Type u_1} [inst : Add M] (S : AddSubsemigroup M), AddSubsemigroup.map (AddHom.id M) S = S
-- Lean.Parser.Basic
Lean.Parser.peekTokenAux : Lean.Parser.ParserContext →
  Lean.Parser.ParserState → Lean.Parser.ParserState × Except Lean.Parser.ParserState Lean.Syntax
-- Lean.Elab.Do.Legacy
Lean.Elab.Term.Do.ToTerm.Kind.nestedPR : Lean.Elab.Term.Do.ToTerm.Kind
-- Mathlib.RingTheory.Coalgebra.Hom
CoalgHomClass.toSemilinearMapClass : ∀ {F : Type u_1} {R : outParam (Type u_2)} {A : outParam (Type u_3)} {B : outParam (Type u_4)} {inst : CommSemiring R}
  {inst_1 : AddCommMonoid A} {inst_2 : Module R A} {inst_3 : AddCommMonoid B} {inst_4 : Module R B}
  {inst_5 : CoalgebraStruct R A} {inst_6 : CoalgebraStruct R B} {inst_7 : FunLike F A B} [self : CoalgHomClass F R A B],
  SemilinearMapClass F (RingHom.id R) A B
-- Mathlib.RingTheory.Valuation.ValuativeRel.Basic
ValuativeRel.uniformizer_ne_zero : ∀ {R : Type u_1} [inst : Semiring R] [inst_1 : ValuativeRel R] [inst_2 : ValuativeRel.IsDiscrete R]
  [ValuativeRel.IsNontrivial R], ValuativeRel.uniformizer R ≠ 0
-- Lean.ErrorExplanation
Lean.ErrorExplanation.mk.inj : ∀ {doc : String} {metadata : Lean.ErrorExplanation.Metadata} {declLoc? : Option Lean.DeclarationLocation}
  {doc_1 : String} {metadata_1 : Lean.ErrorExplanation.Metadata} {declLoc?_1 : Option Lean.DeclarationLocation},
  { doc := doc, metadata := metadata, declLoc? := declLoc? } =
      { doc := doc_1, metadata := metadata_1, declLoc? := declLoc?_1 } →
    doc = doc_1 ∧ metadata = metadata_1 ∧ declLoc? = declLoc?_1
-- Mathlib.Computability.RecursiveIn
ComputableIn.recursiveIn : ∀ {α : Type u_1} {σ : Type u_4} [inst : Primcodable α] [inst_1 : Primcodable σ] {f : α → σ} {O : Set (ℕ →. ℕ)},
  ComputableIn O f → RecursiveIn O fun a => Part.some (f a)
-- Mathlib.Order.Minimal
not_maximal_subset_iff : ∀ {α : Type u_2} {P : Set α → Prop} {s : Set α}, P s → (¬Maximal P s ↔ ∃ t, s ⊂ t ∧ P t)
-- Mathlib.Data.Int.Bitwise
/-- `xor` computes the bitwise `xor` of two natural numbers  -/
Int.xor : ℤ → ℤ → ℤ
-- Mathlib.Data.Finset.Sum
Finset.toRight_disjSum : ∀ {α : Type u_1} {β : Type u_2} {s : Finset α} {t : Finset β}, (s.disjSum t).toRight = t
-- Mathlib.RingTheory.PowerBasis
PowerBasis.natDegree_minpoly : ∀ {S : Type u_2} [inst : Ring S] {A : Type u_4} [inst_1 : CommRing A] [inst_2 : Algebra A S] [Nontrivial A]
  (pb : PowerBasis A S), (minpoly A pb.gen).natDegree = pb.dim
-- Lean.ResolveName
/-- Registers a new reserved name predicate.
 -/
Lean.registerReservedNamePredicate : (Lean.Environment → Lean.Name → Bool) → IO Unit
-- Mathlib.Data.Nat.Digits.Defs
/-- Any number m is less than (b+2)^(number of digits in the base b + 2 representation of m)  -/
Nat.lt_base_pow_length_digits' : ∀ {b m : ℕ}, m < (b + 2) ^ ((b + 2).digits m).length
-- Mathlib.Combinatorics.Enumerative.DoubleCounting
Finset.bipartiteAbove.eq_1 : ∀ {α : Type u_2} {β : Type u_3} (r : α → β → Prop) (t : Finset β) (a : α) [inst : DecidablePred (r a)],
  Finset.bipartiteAbove r t a = {b ∈ t | r a b}
-- Mathlib.NumberTheory.Padics.PadicNumbers
padicNormE.image' : ∀ {p : ℕ} [inst : Fact (Nat.Prime p)] {q : ℚ_[p]}, q ≠ 0 → ∃ n, padicNormE q = ↑p ^ (-n)
-- Mathlib.RepresentationTheory.Homological.GroupCohomology.LongExactSequence
/-- Exactness of `Hⁱ(G, X₂) ⟶ Hⁱ(G, X₃) ⟶ Hʲ(G, X₁)`.  -/
groupCohomology.mapShortComplex₃_exact : ∀ {k G : Type u} [inst : CommRing k] [inst_1 : Group G] {X : CategoryTheory.ShortComplex (Rep.{u, u, u} k G)}
  (hX : X.ShortExact) {i j : ℕ} (hij : i + 1 = j), (groupCohomology.mapShortComplex₃ hX hij).Exact
-- Mathlib.Order.SuccPred.Tree
SubRootedTree.mem_iff : ∀ {t : RootedTree} {r : SubRootedTree t} {v : ↑t}, v ∈ r ↔ r.root ≤ v
-- Init.Data.String.Basic
String.ofList_toList : ∀ {s : String}, String.ofList s.toList = s
-- Init.Data.BitVec.Bitblast
BitVec.uppcRec.eq_2 : ∀ {w : ℕ} (x : BitVec w) (i : ℕ) (hs_2 : i + 1 < w), x.uppcRec i.succ hs_2 = (x[w - 1 - i] || x.uppcRec i ⋯)
-- Std.Tactic.BVDecide.Bitblast.BoolExpr.Basic
Std.Tactic.BVDecide.BoolExpr.not.injEq : ∀ {α : Type} (a a_1 : Std.Tactic.BVDecide.BoolExpr α), (a.not = a_1.not) = (a = a_1)
-- Mathlib.AlgebraicTopology.SimplicialSet.Basic
/-- The ulift functor `SSet.Truncated.{u} ⥤ SSet.Truncated.{max u v}` on truncated
simplicial sets.  -/
SSet.Truncated.uliftFunctor : (k : ℕ) → CategoryTheory.Functor (SSet.Truncated k) (SSet.Truncated k)
-- Init.Omega.Coeffs
/-- Shim for `List.map`.  -/
Lean.Omega.Coeffs.map : (ℤ → ℤ) → Lean.Omega.Coeffs → Lean.Omega.Coeffs
-- Mathlib.RingTheory.IsAdjoinRoot
/-- If `S` is `R`-isomorphic to `R[X]/(f)`, then `S` is given by adjoining a root of `f`.  -/
IsAdjoinRoot.ofAdjoinRootEquiv : {R : Type u} →
  {S : Type v} →
    [inst : CommRing R] →
      [inst_1 : Ring S] → {f : Polynomial R} → [inst_2 : Algebra R S] → (AdjoinRoot f ≃ₐ[R] S) → IsAdjoinRoot S f
-- Mathlib.Topology.EMetricSpace.BoundedVariation
BoundedVariationOn.rightLim : ∀ {α : Type u_1} [inst : LinearOrder α] {E : Type u_2} [inst_1 : PseudoEMetricSpace E] [inst_2 : TopologicalSpace α]
  [OrderTopology α] {f : α → E}, BoundedVariationOn f Set.univ → BoundedVariationOn (Function.rightLim f) Set.univ
-- Mathlib.LinearAlgebra.Projection
Submodule.projectionOnto.congr_simp : ∀ {R : Type u_1} [inst : Ring R] {E : Type u_2} [inst_1 : AddCommGroup E] [inst_2 : Module R E]
  (p q q_1 : Submodule R E) (e_q : q = q_1) (h : IsCompl p q), p.projectionOnto q h = p.projectionOnto q_1 ⋯
-- Mathlib.Algebra.Order.GroupWithZero.Canonical
LinearOrderedCommMonoidWithZero.toIsMulTorsionFree : ∀ {α : Type u_1} [inst : LinearOrderedCommMonoidWithZero α], IsMulTorsionFree α
-- Mathlib.Algebra.Homology.TotalComplex
HomologicalComplex₂.totalAux.d₁_eq' : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Preadditive C] {I₁ : Type u_2}
  {I₂ : Type u_3} {I₁₂ : Type u_4} {c₁ : ComplexShape I₁} {c₂ : ComplexShape I₂} (K : HomologicalComplex₂ C c₁ c₂)
  (c₁₂ : ComplexShape I₁₂) [inst_2 : TotalComplexShape c₁ c₂ c₁₂] [inst_3 : DecidableEq I₁₂] [inst_4 : K.HasTotal c₁₂]
  {i₁ i₁' : I₁},
  c₁.Rel i₁ i₁' →
    ∀ (i₂ : I₂) (i₁₂ : I₁₂),
      K.d₁ c₁₂ i₁ i₂ i₁₂ =
        c₁.ε₁ c₂ c₁₂ (i₁, i₂) •
          CategoryTheory.CategoryStruct.comp ((K.d i₁ i₁').f i₂)
            (K.toGradedObject.ιMapObjOrZero (c₁.π c₂ c₁₂) (i₁', i₂) i₁₂)
-- Mathlib.CategoryTheory.Comma.Over.Basic
/-- The induced cone on `Over X` on the lifted functor.  -/
CategoryTheory.Over.liftCone : {T : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} T] →
    {J : Type u_1} →
      [inst_1 : CategoryTheory.Category.{v_1, u_1} J] →
        (D : CategoryTheory.Functor J T) →
          {X : T} →
            (s : D ⟶ (CategoryTheory.Functor.const J).obj X) →
              (c : CategoryTheory.Limits.Cone D) →
                (p : c.pt ⟶ X) →
                  (∀ (j : J), CategoryTheory.CategoryStruct.comp (c.π.app j) (s.app j) = p) →
                    CategoryTheory.Limits.Cone (CategoryTheory.Over.lift D s)
-- Mathlib.Algebra.Algebra.Subalgebra.Unitization
NonUnitalSubsemiring.unitization.eq_1 : ∀ {R : Type u_1} {S : Type u_2} [inst : Semiring R] [inst_1 : SetLike S R] [hSR : NonUnitalSubsemiringClass S R]
  (s : S), NonUnitalSubsemiring.unitization s = NonUnitalSubalgebra.unitization s
-- Lean.ResolveName
/-- Global reference containing all reserved name predicates.  -/
Lean.reservedNamePredicatesRef : IO.Ref (Array (Lean.Environment → Lean.Name → Bool))
-- Mathlib.LinearAlgebra.RootSystem.CartanMatrix
RootPairing.Base.cartanMatrixIn.eq_1 : ∀ {ι : Type u_1} {R : Type u_2} {M : Type u_3} {N : Type u_4} [inst : CommRing R] [inst_1 : AddCommGroup M]
  [inst_2 : Module R M] [inst_3 : AddCommGroup N] [inst_4 : Module R N] (S : Type u_5) [inst_5 : CommRing S]
  [inst_6 : Algebra S R] {P : RootPairing ι R M N} [inst_7 : P.IsValuedIn S] (b : P.Base),
  RootPairing.Base.cartanMatrixIn S b = Matrix.of fun i j => P.pairingIn S ↑i ↑j
-- Mathlib.CategoryTheory.Sites.Point.Monoidal
CategoryTheory.GrothendieckTopology.Point.toPresheafFiber_δ_assoc : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {J : CategoryTheory.GrothendieckTopology C} (Φ : J.Point)
  {A : Type u'} [inst_1 : CategoryTheory.Category.{v', u'} A] [inst_2 : CategoryTheory.MonoidalCategory A]
  [inst_3 : CategoryTheory.Limits.HasColimitsOfSize.{w, w, v', u'} A] (X : C) (x : Φ.fiber.obj X)
  (G₁ G₂ : CategoryTheory.Functor Cᵒᵖ A) {Z : A}
  (h : CategoryTheory.MonoidalCategoryStruct.tensorObj (Φ.presheafFiber.obj G₁) (Φ.presheafFiber.obj G₂) ⟶ Z),
  CategoryTheory.CategoryStruct.comp (Φ.toPresheafFiber X x (CategoryTheory.MonoidalCategoryStruct.tensorObj G₁ G₂))
      (CategoryTheory.CategoryStruct.comp (CategoryTheory.Functor.OplaxMonoidal.δ Φ.presheafFiber G₁ G₂) h) =
    CategoryTheory.CategoryStruct.comp
      (CategoryTheory.MonoidalCategoryStruct.tensorHom (Φ.toPresheafFiber X x G₁) (Φ.toPresheafFiber X x G₂)) h
-- Mathlib.Algebra.Group.Action.TypeTags
Multiplicative.smulCommClass : ∀ {α : Type u_2} {β : Type u_3} {γ : Type u_4} [inst : VAdd α γ] [inst_1 : VAdd β γ] [VAddCommClass α β γ],
  SMulCommClass (Multiplicative α) (Multiplicative β) γ
-- Mathlib.CategoryTheory.Monoidal.Multifunctor
/-- The bifunctor `F (- ⊗ -)`.  -/
CategoryTheory.MonoidalCategory.curriedTensorPost : {C : Type u_1} →
  [inst : CategoryTheory.Category.{v_1, u_1} C] →
    [CategoryTheory.MonoidalCategory C] →
      {D : Type u_2} →
        [inst_2 : CategoryTheory.Category.{v_2, u_2} D] →
          CategoryTheory.Functor C D → CategoryTheory.Functor C (CategoryTheory.Functor C D)
-- Std.Data.DTreeMap.Raw.Slice
Std.DTreeMap.Raw.toList_ric : ∀ {α : Type u} {β : α → Type v} (cmp : autoParam (α → α → Ordering) Std.DTreeMap.Raw.toList_ric._auto_1)
  [Std.TransCmp cmp] {t : Std.DTreeMap.Raw α β cmp},
  t.WF →
    ∀ {bound : α},
      Std.Slice.toList (Std.Ric.Sliceable.mkSlice t *...=bound) = List.filter (fun e => (cmp e.fst bound).isLE) t.toList
-- Mathlib.Data.Holor
Holor.instAddCommMonoid : {α : Type} → {ds : List ℕ} → [AddCommMonoid α] → AddCommMonoid (Holor α ds)
-- Mathlib.Data.ENNReal.Operations
ENNReal.sub_lt_of_lt_add : ∀ {a b c : ENNReal}, c ≤ a → a < b + c → a - c < b
-- Mathlib.CategoryTheory.Monoidal.Grp
CategoryTheory.Functor.FullyFaithful.grpObj_inv : ∀ {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} [inst_4 : F.Monoidal] (hF : F.FullyFaithful) (X : C)
  [inst_5 : CategoryTheory.GrpObj (F.obj X)], CategoryTheory.GrpObj.inv = hF.preimage CategoryTheory.GrpObj.inv
-- Mathlib.RepresentationTheory.FinGroupCharZero
/-- If `G` is finite and its order is nonzero in the field `k`, then every object of
`Rep k G` is projective.
 -/
Rep.instProjective : ∀ {k : Type u} [inst : Field k] {G : Type u} [Finite G] [inst_2 : Group G] [NeZero ↑(Nat.card G)]
  (V : Rep.{u, u, u} k G), CategoryTheory.Projective V
-- Mathlib.Data.NNReal.Defs
/-- Nonnegative real numbers, denoted as `ℝ≥0` within the NNReal namespace  -/
NNReal.«termℝ≥0» : Lean.ParserDescr
-- Mathlib.Analysis.SpecialFunctions.Trigonometric.Inverse
Real.zero_eq_arcsin_iff : ∀ {x : ℝ}, 0 = Real.arcsin x ↔ x = 0
-- Mathlib.SetTheory.Cardinal.Cofinality.Ordinal
Ordinal.cof_iSup : ∀ {γ : Type u} [inst : LinearOrder γ] [NoMaxOrder γ] {f : γ → Ordinal.{u}}, StrictMono f → (⨆ i, f i).cof = Order.cof γ
-- Mathlib.Probability.Process.Adapted
MeasureTheory.StronglyAdapted.sub : ∀ {Ω : Type u_1} {ι : Type u_2} {m : MeasurableSpace Ω} [inst : Preorder ι] {f : MeasureTheory.Filtration ι m}
  {β : ι → Type u_3} [inst_1 : (i : ι) → TopologicalSpace (β i)] {u v : (i : ι) → Ω → β i}
  [inst_2 : (i : ι) → Sub (β i)] [∀ (i : ι), ContinuousSub (β i)],
  MeasureTheory.StronglyAdapted f u → MeasureTheory.StronglyAdapted f v → MeasureTheory.StronglyAdapted f (u - v)
-- Mathlib.Algebra.TrivSqZeroExt.Basic
TrivSqZeroExt.inr_sum : ∀ (R : Type u) {M : Type v} {ι : Type u_3} [inst : AddCommMonoid R] [inst_1 : AddCommMonoid M] (s : Finset ι)
  (f : ι → M), TrivSqZeroExt.inr (∑ i ∈ s, f i) = ∑ i ∈ s, TrivSqZeroExt.inr (f i)
-- Mathlib.CategoryTheory.Discrete.Basic
CategoryTheory.piEquivalenceFunctorDiscrete_counitIso : ∀ (J : Type u₂) (C : Type u₁) [inst : CategoryTheory.Category.{v₁, u₁} C],
  (CategoryTheory.piEquivalenceFunctorDiscrete J C).counitIso =
    CategoryTheory.NatIso.ofComponents
      (fun F =>
        CategoryTheory.NatIso.ofComponents
          (fun x =>
            CategoryTheory.Iso.refl
              ((({ obj := fun F j => F.obj { as := j }, map := fun {X Y} f j => f.app { as := j }, map_id := ⋯,
                            map_comp := ⋯ }.comp
                        { obj := fun F => CategoryTheory.Discrete.functor F,
                          map := fun {X Y} f => CategoryTheory.Discrete.natTrans fun j => f j.as, map_id := ⋯,
                          map_comp := ⋯ }).obj
                    F).obj
                x))
          ⋯)
      ⋯
-- Mathlib.Algebra.Field.Subfield.Basic
Subfield.coe_sInf : ∀ {K : Type u} [inst : DivisionRing K] (S : Set (Subfield K)), ↑(sInf S) = ⋂ s ∈ S, ↑s
-- Mathlib.LinearAlgebra.Trace
LinearMap.traceAux_eq : ∀ (R : Type u) [inst : CommSemiring R] {M : Type v} [inst_1 : AddCommMonoid M] [inst_2 : Module R M] {ι : Type w}
  [inst_3 : DecidableEq ι] [inst_4 : Fintype ι] {κ : Type u_1} [inst_5 : DecidableEq κ] [inst_6 : Fintype κ]
  (b : Module.Basis ι R M) (c : Module.Basis κ R M), LinearMap.traceAux R b = LinearMap.traceAux R c
-- Mathlib.Algebra.Module.LocalizedModule.Basic
IsLocalizedModule.fromLocalizedModule.bij : ∀ {R : Type u_1} [inst : CommSemiring R] (S : Submonoid R) {M : Type u_2} {M' : Type u_3} [inst_1 : AddCommMonoid M]
  [inst_2 : AddCommMonoid M'] [inst_3 : Module R M] [inst_4 : Module R M'] (f : M →ₗ[R] M')
  [inst_5 : IsLocalizedModule S f], Function.Bijective ⇑(IsLocalizedModule.fromLocalizedModule S f)
-- Mathlib.Topology.Homeomorph.Lemmas
IsHomeomorph.isInducing : ∀ {X : Type u_1} {Y : Type u_2} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y] {f : X → Y},
  IsHomeomorph f → Topology.IsInducing f