mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Topology.Algebra.Module.ContinuousLinearMap.PiProd
ContinuousLinearMap.fst_prod_snd : ∀ {R : Type u_1} [inst : Semiring R] {M₁ : Type u_2} [inst_1 : TopologicalSpace M₁] [inst_2 : AddCommMonoid M₁]
  [inst_3 : Module R M₁] {M₂ : Type u_3} [inst_4 : TopologicalSpace M₂] [inst_5 : AddCommMonoid M₂]
  [inst_6 : Module R M₂],
  (ContinuousLinearMap.fst R M₁ M₂).prod (ContinuousLinearMap.snd R M₁ M₂) = ContinuousLinearMap.id R (M₁ × M₂)
-- Std.Data.DTreeMap.Internal.Model
Std.DTreeMap.Internal.Impl.entryAtIdx?_eq_some_entryAtIdx : ∀ {α : Type u} {β : α → Type v} {t : Std.DTreeMap.Internal.Impl α β} (htb : t.Balanced) {i : ℕ} (h : i < t.size),
  t.entryAtIdx? i = some (t.entryAtIdx htb i h)
-- Mathlib.Data.Fin.VecNotation
/-- Simplify `Fin.snoc` to `vecCons` in this case.  -/
Matrix.Fin.snoc_vecEmpty : ∀ {α : Type u_1} (x : α), Fin.snoc ![] x = ![x]
-- Lean.Parser.Term.Basic
Lean.Parser.Term.structInstFieldBinder.parenthesizer : Lean.PrettyPrinter.Parenthesizer
-- Mathlib.Algebra.Category.ModuleCat.Limits
/-- The `Cocone` on `directLimitDiagram` corresponding to
the unbundled `directLimit` of modules.

In `directLimitIsColimit` we show that it is a colimit cocone.  -/
ModuleCat.directLimitCocone : {R : Type u} →
  [inst : Ring R] →
    {ι : Type v} →
      [DecidableEq ι] →
        [inst_2 : Preorder ι] →
          (G : ι → Type v) →
            [inst_3 : (i : ι) → AddCommGroup (G i)] →
              [inst_4 : (i : ι) → Module R (G i)] →
                (f : (i j : ι) → i ≤ j → G i →ₗ[R] G j) →
                  [inst_5 : DirectedSystem G fun i j h => ⇑(f i j h)] →
                    CategoryTheory.Limits.Cocone (ModuleCat.directLimitDiagram G f)
-- Mathlib.CategoryTheory.Comma.StructuredArrow.Basic
CategoryTheory.CostructuredArrow.mk_surjective : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  {T : D} {S : CategoryTheory.Functor C D} (f : CategoryTheory.CostructuredArrow S T),
  ∃ Y g, f = CategoryTheory.CostructuredArrow.mk g
-- Mathlib.Order.Hom.Lattice
LatticeHom.mk.inj : ∀ {α : Type u_6} {β : Type u_7} {inst : Lattice α} {inst_1 : Lattice β} {toSupHom : SupHom α β}
  {map_inf' : ∀ (a b : α), toSupHom.toFun (a ⊓ b) = toSupHom.toFun a ⊓ toSupHom.toFun b} {toSupHom_1 : SupHom α β}
  {map_inf'_1 : ∀ (a b : α), toSupHom_1.toFun (a ⊓ b) = toSupHom_1.toFun a ⊓ toSupHom_1.toFun b},
  { toSupHom := toSupHom, map_inf' := map_inf' } = { toSupHom := toSupHom_1, map_inf' := map_inf'_1 } →
    toSupHom = toSupHom_1
-- Mathlib.MeasureTheory.Measure.Dirac
MeasureTheory.Measure.ae_eq_or_eq_iff_eq_dirac_add_dirac : ∀ {α : Type u_4} {mα : MeasurableSpace α} [MeasurableSingletonClass α] {μ : MeasureTheory.Measure α} {a₁ a₂ : α},
  a₁ ≠ a₂ →
    ((∀ᵐ (a : α) ∂μ, a = a₁ ∨ a = a₂) ↔
      μ = μ {a₁} • MeasureTheory.Measure.dirac a₁ + μ {a₂} • MeasureTheory.Measure.dirac a₂)
-- Init.Meta.Defs
Lean.githash : String
-- Mathlib.Combinatorics.SimpleGraph.Walk.Subwalks
SimpleGraph.Walk.isSubwalk_take : ∀ {V : Type u_1} {G : SimpleGraph V} {u v : V} (p : G.Walk u v) (n : ℕ), (p.take n).IsSubwalk p
-- Mathlib.RingTheory.Polynomial.IntegralNormalization
Polynomial.integralNormalization_coeff_natDegree : ∀ {R : Type u} [inst : Semiring R] {p : Polynomial R}, p ≠ 0 → p.integralNormalization.coeff p.natDegree = 1
-- Mathlib.Analysis.SpecialFunctions.Exp
Real.map_exp_atBot : Filter.map Real.exp Filter.atBot = nhdsWithin 0 (Set.Ioi 0)
-- Mathlib.LinearAlgebra.Matrix.Notation
Matrix.diagonal_fin_two : ∀ {α : Type u} [inst : Zero α] (d : Fin 2 → α), Matrix.diagonal d = !![d 0, 0; 0, d 1]
-- Mathlib.Topology.Algebra.Module.Spaces.CompactConvergenceCLM
/-- **Alias** of `ContinuousLinearMap.postcompCompactConvergenceCLM`.

---

Specialization of `ContinuousLinearMap.postcomp_uniformConvergenceCLM` to compact
convergence.  -/
postcomp_compactConvergenceCLM : {𝕜₁ : Type u_1} →
  {𝕜₂ : Type u_2} →
    {𝕜₃ : Type u_3} →
      [inst : NormedField 𝕜₁] →
        [inst_1 : NormedField 𝕜₂] →
          [inst_2 : NormedField 𝕜₃] →
            {σ : 𝕜₁ →+* 𝕜₂} →
              {τ : 𝕜₂ →+* 𝕜₃} →
                {ρ : 𝕜₁ →+* 𝕜₃} →
                  [RingHomCompTriple σ τ ρ] →
                    (E : Type u_4) →
                      {F : Type u_5} →
                        {G : Type u_6} →
                          [inst_4 : AddCommGroup E] →
                            [inst_5 : Module 𝕜₁ E] →
                              [inst_6 : AddCommGroup F] →
                                [inst_7 : Module 𝕜₂ F] →
                                  [inst_8 : AddCommGroup G] →
                                    [inst_9 : Module 𝕜₃ G] →
                                      [inst_10 : TopologicalSpace E] →
                                        [inst_11 : TopologicalSpace F] →
                                          [inst_12 : TopologicalSpace G] →
                                            [inst_13 : IsTopologicalAddGroup F] →
                                              [inst_14 : IsTopologicalAddGroup G] →
                                                [inst_15 : ContinuousConstSMul 𝕜₃ G] →
                                                  [inst_16 : ContinuousConstSMul 𝕜₂ F] →
                                                    (F →SL[τ] G) →
                                                      CompactConvergenceCLM σ E F →SL[τ] CompactConvergenceCLM ρ E G
-- Mathlib.Combinatorics.Additive.DoublingConst
Finset.divConst_inv_left : ∀ {G : Type u_1} [inst : CommGroup G] [inst_1 : DecidableEq G] (A B : Finset G), A⁻¹.divConst B = A.mulConst B
-- Lean.Data.Lsp.Basic
Lean.Lsp.instFromJsonLocation : Lean.FromJson Lean.Lsp.Location
-- Mathlib.GroupTheory.Perm.Cycle.Concrete
/-- Any cyclic `f : Perm α` is isomorphic to the nontrivial `Cycle α`
that corresponds to repeated application of `f`.
The forward direction is implemented by `Equiv.Perm.toCycle`.
 -/
Equiv.Perm.isoCycle : {α : Type u_1} → [Fintype α] → [DecidableEq α] → { f // f.IsCycle } ≃ { s // s.Nodup ∧ s.Nontrivial }
-- Mathlib.Topology.Algebra.Module.ContinuousLinearMap.Basic
/-- See Note [custom simps projection].  -/
ContinuousLinearMap.Simps.coe : {R₁ : Type u_1} →
  {R₂ : Type u_2} →
    [inst : Semiring R₁] →
      [inst_1 : Semiring R₂] →
        {σ₁₂ : R₁ →+* R₂} →
          {M₁ : Type u_4} →
            [inst_2 : TopologicalSpace M₁] →
              [inst_3 : AddCommMonoid M₁] →
                {M₂ : Type u_6} →
                  [inst_4 : TopologicalSpace M₂] →
                    [inst_5 : AddCommMonoid M₂] →
                      [inst_6 : Module R₁ M₁] → [inst_7 : Module R₂ M₂] → (M₁ →SL[σ₁₂] M₂) → M₁ →ₛₗ[σ₁₂] M₂
-- Mathlib.Algebra.Category.Ring.Colimits
/-- The function from the free commutative ring on the diagram to the cone point of any other
cocone.  -/
CommRingCat.Colimits.descFunLift : {J : Type v} →
  [inst : CategoryTheory.SmallCategory J] →
    (F : CategoryTheory.Functor J CommRingCat) →
      (s : CategoryTheory.Limits.Cocone F) → CommRingCat.Colimits.Prequotient F → ↑s.pt
-- Mathlib.Combinatorics.Matroid.Rank.ENat
Matroid.eRank_add_eRank_dual : ∀ {α : Type u_1} (M : Matroid α), M.eRank + M✶.eRank = M.E.encard
-- Mathlib.CategoryTheory.Monoidal.Closed.Functor
/-- If `F` is full and faithful, and has a left adjoint which preserves binary products, then it is
Cartesian closed.

TODO: Show the converse, that if `F` is Cartesian closed and its left adjoint preserves binary
products, then it is full and faithful.
 -/
CategoryTheory.cartesianClosedFunctorOfLeftAdjointPreservesBinaryProducts : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {D : Type u'} [inst_1 : CategoryTheory.Category.{v, u'} D]
  [inst_2 : CategoryTheory.CartesianMonoidalCategory C] [inst_3 : CategoryTheory.CartesianMonoidalCategory D]
  (F : CategoryTheory.Functor C D) {L : CategoryTheory.Functor D C} [inst_4 : CategoryTheory.MonoidalClosed C]
  [inst_5 : CategoryTheory.MonoidalClosed D]
  [inst_6 : CategoryTheory.Limits.PreservesLimitsOfShape (CategoryTheory.Discrete CategoryTheory.Limits.WalkingPair) F]
  (h : L ⊣ F) [F.Full] [F.Faithful]
  [CategoryTheory.Limits.PreservesLimitsOfShape (CategoryTheory.Discrete CategoryTheory.Limits.WalkingPair) L],
  CategoryTheory.MonoidalClosedFunctor F
-- Std.Internal.Do.Assertion
/-- An assertion type is equipped with a `CompleteLattice` structure,
used as the carrier for pre- and postconditions.  -/
Std.Internal.Do.Assertion : Type w → Type w
-- Mathlib.Data.Set.Function
Set.BijOn.mapsTo : ∀ {α : Type u_1} {β : Type u_2} {s : Set α} {t : Set β} {f : α → β}, Set.BijOn f s t → Set.MapsTo f s t
-- Mathlib.AlgebraicGeometry.OpenImmersion
AlgebraicGeometry.Scheme.Hom.opensFunctor_map_homOfLE : ∀ {X Y : AlgebraicGeometry.Scheme} (f : X ⟶ Y) [H : AlgebraicGeometry.IsOpenImmersion f] {U V : X.Opens} (e : U ≤ V),
  (AlgebraicGeometry.Scheme.Hom.opensFunctor f).map (CategoryTheory.homOfLE e) = CategoryTheory.homOfLE ⋯
-- Mathlib.Data.Multiset.ZeroCons
Multiset.cons_subset : ∀ {α : Type u_1} {a : α} {s t : Multiset α}, a ::ₘ s ⊆ t ↔ a ∈ t ∧ s ⊆ t
-- Init.Data.String.Lemmas.FindPos
String.Slice.posGE_inc : ∀ {s : String.Slice} {p : String.Pos.Raw} {h : p.inc ≤ s.rawEndPos}, s.posGE p.inc h = s.posGT p h
-- Init.Data.SInt.Lemmas
Int64.ofBitVec_lt_iff_slt : ∀ (a b : BitVec 64), Int64.ofBitVec a < Int64.ofBitVec b ↔ a.slt b = true
-- Mathlib.Algebra.GroupWithZero.Associated
Associated.dvd_iff_dvd_right : ∀ {M : Type u_1} [inst : Monoid M] {a b c : M}, Associated b c → (a ∣ b ↔ a ∣ c)
-- Mathlib.Analysis.InnerProductSpace.Defs
/-- Given an `InnerProductSpace.Core` structure on a space with a topology, one can use it to turn
the space into an inner product space. The `NormedAddCommGroup` structure is expected
to already be defined with `InnerProductSpace.ofCore.toNormedAddCommGroupOfTopology`.  -/
InnerProductSpace.ofCoreOfTopology : {𝕜 : Type u_1} →
  {F : Type u_3} →
    [inst : RCLike 𝕜] →
      [inst_1 : AddCommGroup F] →
        [hF : Module 𝕜 F] →
          [inst_2 : TopologicalSpace F] →
            [inst_3 : IsTopologicalAddGroup F] →
              [inst_4 : ContinuousConstSMul 𝕜 F] →
                (cd : InnerProductSpace.Core 𝕜 F) →
                  (h : ContinuousAt (fun v => inner 𝕜 v v) 0) →
                    (h' : Bornology.IsVonNBounded 𝕜 {v | RCLike.re (inner 𝕜 v v) < 1}) → InnerProductSpace 𝕜 F
-- Mathlib.RingTheory.Extension.Cotangent.Basic
Algebra.Extension.H1Cotangent.map_id : ∀ {R : Type u} {S : Type v} [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : Algebra R S]
  {P : Algebra.Extension R S}, Algebra.Extension.H1Cotangent.map (Algebra.Extension.Hom.id P) = LinearMap.id
-- Mathlib.RingTheory.NonUnitalSubring.Basic
/-- Sum of a list of elements in a non-unital subring is in the non-unital subring.  -/
NonUnitalSubring.list_sum_mem : ∀ {R : Type u} [inst : NonUnitalNonAssocRing R] (s : NonUnitalSubring R) {l : List R}, (∀ x ∈ l, x ∈ s) → l.sum ∈ s
-- Lean.Compiler.LCNF.Basic
Lean.Compiler.LCNF.LetValue.pap.inj : ∀ {pu : Lean.Compiler.LCNF.Purity} {fn : Lean.Name} {args : Array (Lean.Compiler.LCNF.Arg pu)}
  {h : autoParam (pu = Lean.Compiler.LCNF.Purity.impure) Lean.Compiler.LCNF.LetValue._auto_15} {fn_1 : Lean.Name}
  {args_1 : Array (Lean.Compiler.LCNF.Arg pu)}
  {h_1 : autoParam (pu = Lean.Compiler.LCNF.Purity.impure) Lean.Compiler.LCNF.LetValue._auto_15},
  Lean.Compiler.LCNF.LetValue.pap fn args h = Lean.Compiler.LCNF.LetValue.pap fn_1 args_1 h_1 →
    fn = fn_1 ∧ args = args_1
-- Mathlib.LinearAlgebra.Eigenspace.Basic
/-- The generalized eigenrange for a linear map `f`, a scalar `μ`, and an exponent `k ∈ ℕ∞`
is the range of `(f - μ • id) ^ k` if `k` is a natural number,
or the infimum of these ranges if `k = ∞`.  -/
Module.End.genEigenrange : {R : Type v} →
  {M : Type w} →
    [inst : CommRing R] → [inst_1 : AddCommGroup M] → [inst_2 : Module R M] → Module.End R M → R → ℕ∞ → Submodule R M
-- Mathlib.CategoryTheory.Limits.Shapes.BinaryBiproducts
CategoryTheory.Limits.BinaryBicones.functoriality_full : ∀ {C : Type uC} [inst : CategoryTheory.Category.{uC', uC} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  {D : Type uD} [inst_2 : CategoryTheory.Category.{uD', uD} D] [inst_3 : CategoryTheory.Limits.HasZeroMorphisms D]
  (P Q : C) (F : CategoryTheory.Functor C D) [inst_4 : F.PreservesZeroMorphisms] [F.Full] [F.Faithful],
  (CategoryTheory.Limits.BinaryBicones.functoriality P Q F).Full
-- Mathlib.Algebra.Group.Subgroup.Lattice
Subgroup.exists_ne_one_of_nontrivial : ∀ {G : Type u_1} [inst : Group G] (H : Subgroup G) [Nontrivial ↥H], ∃ x ∈ H, x ≠ 1
-- Lean.Meta.Tactic.Simp.Arith.Int.Basic
/-- Converts the linear polynomial into the "simplified" expression  -/
Int.Internal.Linear.Poly.toExpr : Int.Internal.Linear.Poly → Int.Internal.Linear.Expr
-- Mathlib.Topology.FiberBundle.Trivialization
Bundle.Trivialization.symm_trans_target_eq : ∀ {B : Type u_1} {F : Type u_2} {Z : Type u_4} [inst : TopologicalSpace B] [inst_1 : TopologicalSpace F] {proj : Z → B}
  [inst_2 : TopologicalSpace Z] (e e' : Bundle.Trivialization F proj),
  (e.symm.trans e'.toPartialEquiv).target = (e.baseSet ∩ e'.baseSet) ×ˢ Set.univ
-- Lean.Parser.Types
/-- Creates a new string that consists of the region of the input string delimited by the two positions.

The result is `""` if the start position is greater than or equal to the end position or if the
start position is at the end of the string. If either position is invalid (that is, if either points
at the middle of a multi-byte UTF-8 character) then the result is unspecified.
 -/
Lean.Parser.InputContext.extract : Lean.Parser.InputContext → String.Pos.Raw → String.Pos.Raw → String
-- Mathlib.Data.Set.Defs
Set.instSDiff : {α : Type u} → SDiff (Set α)
-- Mathlib.Topology.Algebra.ContinuousAffineEquiv
/-- Product of two continuous affine equivalences. The map comes from `Equiv.prodCongr`  -/
ContinuousAffineEquiv.prodCongr : {k : Type u_1} →
  {P₁ : Type u_2} →
    {P₂ : Type u_3} →
      {P₃ : Type u_4} →
        {P₄ : Type u_5} →
          {V₁ : Type u_6} →
            {V₂ : Type u_7} →
              {V₃ : Type u_8} →
                {V₄ : Type u_9} →
                  [inst : Ring k] →
                    [inst_1 : AddCommGroup V₁] →
                      [inst_2 : Module k V₁] →
                        [inst_3 : AddTorsor V₁ P₁] →
                          [inst_4 : TopologicalSpace P₁] →
                            [inst_5 : AddCommGroup V₂] →
                              [inst_6 : Module k V₂] →
                                [inst_7 : AddTorsor V₂ P₂] →
                                  [inst_8 : TopologicalSpace P₂] →
                                    [inst_9 : AddCommGroup V₃] →
                                      [inst_10 : Module k V₃] →
                                        [inst_11 : AddTorsor V₃ P₃] →
                                          [inst_12 : TopologicalSpace P₃] →
                                            [inst_13 : AddCommGroup V₄] →
                                              [inst_14 : Module k V₄] →
                                                [inst_15 : AddTorsor V₄ P₄] →
                                                  [inst_16 : TopologicalSpace P₄] →
                                                    (P₁ ≃ᴬ[k] P₂) → (P₃ ≃ᴬ[k] P₄) → P₁ × P₃ ≃ᴬ[k] P₂ × P₄
-- Mathlib.Computability.AkraBazzi.GrowsPolynomially
AkraBazziRecurrence.growsPolynomially_zpow : ∀ (p : ℤ), AkraBazziRecurrence.GrowsPolynomially fun x => x ^ p
-- Mathlib.MeasureTheory.Group.FundamentalDomain
MeasureTheory.IsFundamentalDomain.setIntegral_eq : ∀ {G : Type u_1} {α : Type u_3} {E : Type u_5} [inst : Group G] [inst_1 : MulAction G α] [inst_2 : MeasurableSpace α]
  [inst_3 : NormedAddCommGroup E] {s t : Set α} {μ : MeasureTheory.Measure α} [MeasurableConstSMul G α]
  [MeasureTheory.SMulInvariantMeasure G α μ] [Countable G] [inst_7 : NormedSpace ℝ E],
  MeasureTheory.IsFundamentalDomain G s μ →
    MeasureTheory.IsFundamentalDomain G t μ →
      ∀ {f : α → E}, (∀ (g : G) (x : α), f (g • x) = f x) → ∫ (x : α) in s, f x ∂μ = ∫ (x : α) in t, f x ∂μ
-- Mathlib.Topology.Algebra.IsUniformGroup.Basic
Subgroup.tendsto_coe_cofinite_of_discrete : ∀ {G : Type u_1} [inst : Group G] [inst_1 : TopologicalSpace G] [IsTopologicalGroup G] [T2Space G] (H : Subgroup G),
  IsDiscrete ↑H → Filter.Tendsto Subtype.val Filter.cofinite (Filter.cocompact G)
-- Std.Data.Internal.List.Associative
Std.Internal.List.congr_filter_not_contains_map_fst_of_perm : ∀ {α : Type u} {β : α → Type v} {l₁ l₂ l₃ l₄ : List ((a : α) × β a)} [inst : BEq α] [EquivBEq α],
  l₁.Perm l₃ →
    l₂.Perm l₄ →
      Std.Internal.List.DistinctKeys l₃ →
        (List.filter (fun p => !(List.map Sigma.fst l₂).contains p.fst) l₁).Perm
          (List.filter (fun p => !(List.map Sigma.fst l₄).contains p.fst) l₃)
-- Mathlib.CategoryTheory.Comma.Basic
CategoryTheory.Comma.mapRightIso_counitIso_inv_app_right : ∀ {B : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} B] {A : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} A]
  {T : Type u₃} [inst_2 : CategoryTheory.Category.{v₃, u₃} T] (L : CategoryTheory.Functor A T)
  {R₁ R₂ : CategoryTheory.Functor B T} (i : R₁ ≅ R₂) (X : CategoryTheory.Comma L R₂),
  ((CategoryTheory.Comma.mapRightIso L i).counitIso.inv.app X).right = CategoryTheory.CategoryStruct.id X.right
-- Mathlib.Combinatorics.SimpleGraph.Connectivity.Connected
SimpleGraph.Reachable.degree_pos_right : ∀ {V : Type u} {G : SimpleGraph V} {u v : V} [inst : Fintype ↑(G.neighborSet v)],
  u ≠ v → G.Reachable u v → 0 < G.degree v
-- Mathlib.RingTheory.Extension.Basic
Algebra.Extension.Cotangent.map_comp : ∀ {R : Type u} {S : Type v} [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : Algebra R S] {P : Algebra.Extension R S}
  {R' : Type u_1} {S' : Type u_2} [inst_3 : CommRing R'] [inst_4 : CommRing S'] [inst_5 : Algebra R' S']
  {P' : Algebra.Extension R' S'} {R'' : Type u_4} {S'' : Type u_5} [inst_6 : CommRing R''] [inst_7 : CommRing S'']
  [inst_8 : Algebra R'' S''] (P'' : Algebra.Extension R'' S'') [inst_9 : Algebra R R'] [inst_10 : Algebra R' R'']
  [inst_11 : Algebra R' S''] [inst_12 : Algebra S S'] [inst_13 : Algebra S' S''] [inst_14 : Algebra S S'']
  [inst_15 : Algebra R S'] [inst_16 : IsScalarTower R R' S'] [inst_17 : Algebra R R'']
  [inst_18 : IsScalarTower R R' R''] [inst_19 : IsScalarTower R' R'' S''] [inst_20 : Algebra R S'']
  [inst_21 : IsScalarTower R R'' S''] [inst_22 : IsScalarTower S S' S''] (f : P.Hom P') (g : P'.Hom P''),
  Algebra.Extension.Cotangent.map (g.comp f) =
    ↑S (Algebra.Extension.Cotangent.map g) ∘ₗ Algebra.Extension.Cotangent.map f
-- Batteries.Data.UnionFind.Basic
/-- Create an empty union-find structure with specific capacity  -/
Batteries.UnionFind.mkEmpty : ℕ → Batteries.UnionFind
-- Init.Prelude
EStateM.instMonadStateOf : {ε σ : Type u} → MonadStateOf σ (EStateM ε σ)
-- Init.Data.Order.Ord
Option.instLawfulEqOrd : ∀ {α : Type u_1} [inst : Ord α] [Std.LawfulEqOrd α], Std.LawfulEqOrd (Option α)
-- Mathlib.MeasureTheory.Function.StronglyMeasurable.AEStronglyMeasurable
MeasureTheory.AEFinStronglyMeasurable.neg : ∀ {α : Type u_1} {β : Type u_2} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} [inst : TopologicalSpace β]
  {f : α → β} [inst_1 : SubtractionMonoid β] [ContinuousNeg β],
  MeasureTheory.AEFinStronglyMeasurable f μ → MeasureTheory.AEFinStronglyMeasurable (-f) μ
-- Mathlib.Algebra.Order.Monoid.Unbundled.Pow
Right.pow_le_one_of_le : ∀ {M : Type u_3} [inst : Monoid M] [inst_1 : Preorder M] [MulRightMono M] {x : M}, x ≤ 1 → ∀ {n : ℕ}, x ^ n ≤ 1
-- Mathlib.Data.Part
Part.instMembership : {α : Type u_1} → Membership α (Part α)
-- Init.Data.Array.GetLit
_private.Init.Data.Array.GetLit.0.Array.toArrayLit_eq.getLit_eq : ∀ {α : Type u_1} (n : ℕ) (xs : Array α) (i : ℕ) (h₁ : xs.size = n) (h₂ : i < n), xs.getLit i h₁ h₂ = xs.toList[i]
-- Mathlib.Control.Bitraversable.Lemmas
Bitraversable.tsnd_eq_snd_id : ∀ {t : Type u → Type u → Type u} [inst : Bitraversable t] [LawfulBitraversable t] {α β β' : Type u} (f : β → β')
  (x : t α β), Bitraversable.tsnd (pure ∘ f) x = pure (Bifunctor.snd f x)
-- Mathlib.RingTheory.Adjoin.Field
minpoly_neg_splits : ∀ {K : Type u_2} {L : Type u_3} [inst : Field K] [inst_1 : Field L] [inst_2 : Algebra K L] {x : L},
  (Polynomial.map (algebraMap K L) (minpoly K x)).Splits → (Polynomial.map (algebraMap K L) (minpoly K (-x))).Splits
-- Mathlib.CategoryTheory.Preadditive.CommGrp_
/-- An additive category is equivalent to its category of commutative group objects.  -/
CategoryTheory.Preadditive.commGrpEquivalence : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    [CategoryTheory.Preadditive C] →
      [inst_2 : CategoryTheory.CartesianMonoidalCategory C] →
        [inst_3 : CategoryTheory.BraidedCategory C] → C ≌ CategoryTheory.CommGrp C
-- Mathlib.RingTheory.Valuation.ValuationRing
ValuationRing.coe_equivInteger_apply : ∀ (A : Type u) [inst : CommRing A] (K : Type v) [inst_1 : Field K] [inst_2 : Algebra A K] [inst_3 : IsDomain A]
  [inst_4 : ValuationRing A] [inst_5 : IsFractionRing A K] (a : A),
  ↑((ValuationRing.equivInteger A K) a) = (algebraMap A K) a
-- Init.Data.UInt.Lemmas
UInt32.ofNatLT_uInt16ToNat : ∀ (n : UInt16), UInt32.ofNatLT n.toNat ⋯ = n.toUInt32
-- Init.Data.Slice.List.Lemmas
ListSlice.size_mkSlice_roi : ∀ {α : Type u_1} {xs : ListSlice α} {lo : ℕ},
  Std.Slice.size (Std.Roi.Sliceable.mkSlice xs lo<...*) = Std.Slice.size xs - (lo + 1)
-- Mathlib.Analysis.Normed.Group.Subgroup
AddSubgroupClass.normedAddGroup : {E : Type u_1} →
  [inst : NormedAddGroup E] →
    {S : Type u_2} → [inst_1 : SetLike S E] → [AddSubgroupClass S E] → (s : S) → NormedAddGroup ↥s
-- Mathlib.LinearAlgebra.Prod
LinearMap.span_inl_union_inr : ∀ {R : Type u} {M : Type v} {M₂ : Type w} [inst : Semiring R] [inst_1 : AddCommMonoid M] [inst_2 : AddCommMonoid M₂]
  [inst_3 : Module R M] [inst_4 : Module R M₂] {s : Set M} {t : Set M₂},
  Submodule.span R (⇑(LinearMap.inl R M M₂) '' s ∪ ⇑(LinearMap.inr R M M₂) '' t) =
    (Submodule.span R s).prod (Submodule.span R t)
-- Mathlib.Order.KrullDimension
Order.coheight_orderIso : ∀ {α : Type u_1} {β : Type u_2} [inst : Preorder α] [inst_1 : Preorder β] (f : α ≃o β) (x : α),
  Order.coheight (f x) = Order.coheight x
-- Std.Data.ExtTreeMap.Lemmas
Std.ExtTreeMap.mem_ofList : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} [inst : Std.TransCmp cmp] [inst_1 : BEq α] [Std.LawfulBEqCmp cmp]
  {l : List (α × β)} {k : α}, k ∈ Std.ExtTreeMap.ofList l cmp ↔ (List.map Prod.fst l).contains k = true
-- Mathlib.Data.Matrix.Mul
sub_dotProduct : ∀ {m : Type u_2} {α : Type v} [inst : Fintype m] [inst_1 : NonUnitalNonAssocRing α] (u v w : m → α),
  (u - v) ⬝ᵥ w = u ⬝ᵥ w - v ⬝ᵥ w
-- Mathlib.Algebra.Algebra.Hom.Rat
/-- Reinterpret a `RingEquiv` as a `ℚ`-algebra isomorphism. This actually yields an
equivalence, see `RingEquiv.equivRatAlgEquiv`.  -/
RingEquiv.toRatAlgEquiv : {R : Type u_1} →
  {S : Type u_2} →
    [inst : Ring R] → [inst_1 : Ring S] → [inst_2 : Algebra ℚ R] → [inst_3 : Algebra ℚ S] → R ≃+* S → R ≃ₐ[ℚ] S
-- Mathlib.ModelTheory.Semantics
FirstOrder.Language.Formula.realize_iAlls : ∀ {L : FirstOrder.Language} {M : Type w} [inst : L.Structure M] {α : Type u'} {β : Type v'} [inst_1 : Finite β]
  {φ : L.Formula (α ⊕ β)} {v : α → M},
  (FirstOrder.Language.Formula.iAlls β φ).Realize v ↔ ∀ (i : β → M), φ.Realize fun a => Sum.elim v i a