mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Algebra.Category.Ring.Basic
RingCat.of.sizeOf_spec : ∀ (carrier : Type u) [ring : Ring carrier], sizeOf (RingCat.of carrier) = 1 + sizeOf carrier + sizeOf ring
-- Mathlib.Algebra.Homology.Embedding.Basic
/-- The opposite embedding in `Embedding c.symm c'.symm` of `e : Embedding c c'`.  -/
ComplexShape.Embedding.op : {ι : Type u_1} →
  {ι' : Type u_2} → {c : ComplexShape ι} → {c' : ComplexShape ι'} → c.Embedding c' → c.symm.Embedding c'.symm
-- Mathlib.Algebra.Group.Pi.Lemmas
/-- The monoid homomorphism including a single monoid into a dependent family of additive monoids,
as functions supported at a point.

This is the `MonoidHom` version of `Pi.mulSingle`.  -/
MonoidHom.mulSingle : {I : Type u} →
  (f : I → Type v) → [DecidableEq I] → [inst : (i : I) → MulOneClass (f i)] → (i : I) → f i →* (i : I) → f i
-- Mathlib.Combinatorics.SimpleGraph.Extremal.Turan
/-- For `0 < r`, `turanGraph n r` is Turán-maximal.  -/
SimpleGraph.isTuranMaximal_turanGraph : ∀ {n r : ℕ}, 0 < r → (SimpleGraph.turanGraph n r).IsTuranMaximal r
-- Std.Internal.Do.Order.PreservesSup
Lean.Order.PreservesSup.mk : ∀ {α : Type u} [inst : Lean.Order.CompleteLattice α] {f : α → α},
  (∀ (s : α → Prop),
      f (Lean.Order.CompleteLattice.sup s) = Lean.Order.CompleteLattice.sup fun y => ∃ x, s x ∧ y = f x) →
    Lean.Order.PreservesSup f
-- Mathlib.Analysis.Normed.Operator.Banach
/-- The Banach open mapping theorem: a surjective bounded linear map between Banach spaces is
open.  -/
ContinuousLinearMap.isOpenMap : ∀ {𝕜 : Type u_1} {𝕜' : Type u_2} [inst : NontriviallyNormedField 𝕜] [inst_1 : NontriviallyNormedField 𝕜'] {σ : 𝕜 →+* 𝕜'}
  {E : Type u_3} [inst_2 : NormedAddCommGroup E] [inst_3 : NormedSpace 𝕜 E] {F : Type u_4}
  [inst_4 : NormedAddCommGroup F] [inst_5 : NormedSpace 𝕜' F] (f : E →SL[σ] F) {σ' : 𝕜' →+* 𝕜} [RingHomInvPair σ σ']
  [RingHomIsometric σ] [RingHomIsometric σ'] [CompleteSpace F] [CompleteSpace E], Function.Surjective ⇑f → IsOpenMap ⇑f
-- Mathlib.Topology.Algebra.Module.Complement
Submodule.IsTopCompl.t3Space : ∀ {R : Type u_1} [inst : Ring R] {M : Type u_2} [inst_1 : TopologicalSpace M] [inst_2 : AddCommGroup M]
  [inst_3 : Module R M] {p q : Submodule R M} [IsTopologicalAddGroup M],
  Submodule.IsTopCompl p q → IsClosed ↑q → T3Space ↥p
-- Mathlib.CategoryTheory.SmallObject.Iteration.Nonempty
CategoryTheory.SmallObject.SuccStruct.Iteration.nonempty : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] (Φ : CategoryTheory.SmallObject.SuccStruct C)
  {J : Type u} [inst_1 : LinearOrder J] [inst_2 : OrderBot J] [inst_3 : SuccOrder J] [inst_4 : WellFoundedLT J]
  [inst_5 : CategoryTheory.Limits.HasIterationOfShape J C] (j : J), Nonempty (Φ.Iteration j)
-- Mathlib.RingTheory.Ideal.Height
Ideal.FiniteHeight.eq_top_or_height_ne_top : ∀ {R : Type u_1} {inst : CommRing R} {I : Ideal R} [self : I.FiniteHeight], I = ⊤ ∨ I.height ≠ ⊤
-- Mathlib.Algebra.Group.Hom.Instances
ZeroHom.instAddGroup.eq_1 : ∀ {M : Type uM} {N : Type uN} [inst : Zero M] [inst_1 : AddGroup N],
  ZeroHom.instAddGroup =
    { toAddMonoid := ZeroHom.instAddMonoid, toNeg := ZeroHom.instNeg, toSub := ZeroHom.instSub, toZSMul := ZSMul.ofSMul,
      sub_eq_add_neg := ⋯, zsmul_zero' := ⋯, zsmul_succ' := ⋯, zsmul_neg' := ⋯, neg_add_cancel := ⋯ }
-- Mathlib.Algebra.Group.Equiv.Opposite
/-- `MulOpposite.op` on a commutative monoid is an isomorphism.  -/
MulOpposite.opMulEquiv : {M : Type u_1} → [inst : CommMonoid M] → M ≃* Mᵐᵒᵖ
-- Mathlib.AlgebraicTopology.FundamentalGroupoid.SimplyConnected
Homeomorph.isSimplyConnected_image : ∀ {X : Type u_1} {Y : Type u_2} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y] (f : X ≃ₜ Y) {s : Set X},
  IsSimplyConnected (⇑f '' s) ↔ IsSimplyConnected s
-- Lean.Elab.AuxDef
Lean.Elab.Command.elabAuxDef : Lean.Elab.Command.CommandElab
-- Mathlib.SetTheory.Descriptive.Tree
Descriptive.Tree.pullSub.eq_1 : ∀ {A : Type u_1} (T : ↥(Descriptive.tree A)) (x : List A),
  Descriptive.Tree.pullSub T x = ⟨{y | List.take x.length y <+: x ∧ List.drop x.length y ∈ T}, ⋯⟩
-- Mathlib.Topology.DerivedSet
AccPt.map : ∀ {X : Type u_1} [inst : TopologicalSpace X] {β : Type u_2} [inst_1 : TopologicalSpace β] {F : Filter X} {x : X},
  AccPt x F → ∀ {f : X → β}, ContinuousAt f x → Function.Injective f → AccPt (f x) (Filter.map f F)
-- Mathlib.Algebra.Order.Group.Pointwise.Interval
Set.image_mul_left_Icc' : ∀ {G₀ : Type u_2} [inst : GroupWithZero G₀] [inst_1 : PartialOrder G₀] [PosMulReflectLT G₀] {a : G₀},
  0 < a → ∀ (b c : G₀), (fun x => a * x) '' Set.Icc b c = Set.Icc (a * b) (a * c)
-- Mathlib.Topology.ContinuousOn
ContinuousWithinAt.comp_inter_of_eq : ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} [inst : TopologicalSpace α] [inst_1 : TopologicalSpace β]
  [inst_2 : TopologicalSpace γ] {f : α → β} {s : Set α} {x : α} {g : β → γ} {t : Set β} {y : β},
  ContinuousWithinAt g t y → ContinuousWithinAt f s x → f x = y → ContinuousWithinAt (g ∘ f) (s ∩ f ⁻¹' t) x
-- Init.Data.Range.Polymorphic.NatLemmas
Nat.toArray_ric_eq_singleton_append_iff : ∀ {xs : Array ℕ} {n a : ℕ}, (*...=n).toArray = #[a] ++ xs ↔ 0 = a ∧ (1...=n).toArray = xs
-- Lean.PrettyPrinter.Delaborator.Builtins
/-- Runs the given unexpanders, returning the resulting syntax if any are applicable, and otherwise fails.
 -/
_private.Lean.PrettyPrinter.Delaborator.Builtins.0.Lean.PrettyPrinter.Delaborator.delabAppImplicitCore.tryUnexpand : Lean.Syntax → List Lean.PrettyPrinter.Unexpander → Lean.Syntax → Lean.PrettyPrinter.Delaborator.DelabM Lean.Syntax
-- Mathlib.CategoryTheory.Localization.Construction
CategoryTheory.Localization.Construction.natTransExtension_hcomp : ∀ {C : Type uC} [inst : CategoryTheory.Category.{uC', uC} C] {W : CategoryTheory.MorphismProperty C} {D : Type uD}
  [inst_1 : CategoryTheory.Category.{uD', uD} D] {F G : CategoryTheory.Functor W.Localization D}
  (τ : W.Q.comp F ⟶ W.Q.comp G),
  CategoryTheory.CategoryStruct.id W.Q ◫ CategoryTheory.Localization.Construction.natTransExtension τ = τ
-- Mathlib.Algebra.Order.GroupWithZero.Defs
mul_lt_mul_of_pos' : ∀ {α : Type u_1} [inst : Mul α] [inst_1 : Zero α] [inst_2 : Preorder α] {a b c d : α} [PosMulStrictMono α]
  [MulPosStrictMono α], a < b → c < d → 0 < c → 0 < b → a * c < b * d
-- Mathlib.LinearAlgebra.Matrix.ToLin
LinearMap.toMatrix'_algebraMap : ∀ {R : Type u_1} [inst : CommSemiring R] {n : Type u_5} [inst_1 : DecidableEq n] [inst_2 : Fintype n] (x : R),
  LinearMap.toMatrix' ((algebraMap R (Module.End R (n → R))) x) = (Matrix.scalar n) x
-- Mathlib.LinearAlgebra.Matrix.ToLin
Algebra.leftMulMatrix_eq_repr_mul : ∀ {R : Type u_1} {S : Type u_2} [inst : CommSemiring R] [inst_1 : Semiring S] [inst_2 : Algebra R S] {m : Type u_3}
  [inst_3 : Fintype m] [inst_4 : DecidableEq m] (b : Module.Basis m R S) (x : S) (i j : m),
  (Algebra.leftMulMatrix b) x i j = (b.repr (x * b j)) i
-- Mathlib.Topology.Algebra.Module.ModuleTopology
/-- The module topology is `≤` any topology making `A` into a topological module.  -/
moduleTopology_le : ∀ (R : Type u_1) [inst : TopologicalSpace R] (A : Type u_2) [inst_1 : Add A] [inst_2 : SMul R A]
  [τA : TopologicalSpace A] [ContinuousSMul R A] [ContinuousAdd A], moduleTopology R A ≤ τA
-- Aesop.Tracing
Aesop.exceptRuleResultToEmoji : {α : Type u_1} → {ε : Type u_2} → (α → String) → Except ε α → String
-- Mathlib.Algebra.Ring.Subring.MulOpposite
/-- A subring `S` of `R` determines a subring `S.op` of the opposite ring `Rᵐᵒᵖ`.  -/
Subring.opEquiv : {R : Type u_2} → [inst : NonAssocRing R] → Subring R ≃o Subring Rᵐᵒᵖ
-- Mathlib.Combinatorics.SimpleGraph.Subgraph
SimpleGraph.Subgraph.coeSubgraph_adj : ∀ {V : Type u} {G : SimpleGraph V} {G' : G.Subgraph} (G'' : G'.coe.Subgraph) (v w : V),
  (SimpleGraph.Subgraph.coeSubgraph G'').Adj v w ↔ ∃ (hv : v ∈ G'.verts) (hw : w ∈ G'.verts), G''.Adj ⟨v, hv⟩ ⟨w, hw⟩
-- Mathlib.Combinatorics.SimpleGraph.Maps
SimpleGraph.induceHomOfLE_toHom : ∀ {V : Type u_1} (G : SimpleGraph V) {s s' : Set V} (h : s ⊆ s'),
  (G.induceHomOfLE h).toHom = SimpleGraph.induceHom SimpleGraph.Hom.id ⋯
-- Mathlib.Analysis.Seminorm
/-- Any action on `ℝ` which factors through `ℝ≥0` applies to a seminorm.  -/
Seminorm.instSMul : {R : Type u_1} →
  {𝕜 : Type u_3} →
    {E : Type u_7} →
      [inst : SeminormedRing 𝕜] →
        [inst_1 : AddGroup E] →
          [inst_2 : SMul 𝕜 E] →
            [inst_3 : SMul R ℝ] → [inst_4 : SMul R NNReal] → [IsScalarTower R NNReal ℝ] → SMul R (Seminorm 𝕜 E)
-- Mathlib.Algebra.Category.ModuleCat.Monoidal.Closed
/-- Describes the unit of the adjunction `M ⊗ - ⊣ Hom(M, -)`. Given an `R`-module `N` this should
define a map `N ⟶ Hom(M, M ⊗ N)`, which is given by flipping the arguments in the natural
`R`-bilinear map `M ⟶ N ⟶ M ⊗ N`.  -/
ModuleCat.ihom_coev_app : ∀ {R : Type u} [inst : CommRing R] (M N : ModuleCat R),
  (CategoryTheory.ihom.coev M).app N =
    ModuleCat.ofHom₂
      (TensorProduct.mk R ↑(Opposite.unop (Opposite.op M)) ↑((CategoryTheory.Functor.id (ModuleCat R)).obj N)).flip
-- Std.Data.ExtHashMap.Basic
/-- Computes the intersection of the given hash maps. The result will only contain entries from the first map.

This function always iterates through the smaller map, so the expected runtime is
`O(min(m₁.size, m₂.size))`.
 -/
Std.ExtHashMap.inter : {α : Type u} →
  {β : Type v} →
    {x : BEq α} →
      {x_1 : Hashable α} →
        [EquivBEq α] → [LawfulHashable α] → Std.ExtHashMap α β → Std.ExtHashMap α β → Std.ExtHashMap α β
-- Mathlib.Geometry.Manifold.Immersion
/-- A function `f : M → N` between `C^n` manifolds is `C^n` at `x` if and only if it is continuous
at `x` and its composition `φ ∘ f` with a `C^n` immersion `φ : N → N'` at `f x` is `C^n` at `x`.  -/
ContMDiffAt.iff_comp_isImmersionAt : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} {E''' : Type u_4} {E'' : Type u}
  [inst_1 : NormedAddCommGroup E] [inst_2 : NormedSpace 𝕜 E] [inst_3 : NormedAddCommGroup E'']
  [inst_4 : NormedSpace 𝕜 E''] [inst_5 : NormedAddCommGroup E'''] [inst_6 : NormedSpace 𝕜 E'''] {H : Type u_7}
  [inst_7 : TopologicalSpace H] {G : Type u_9} [inst_8 : TopologicalSpace G] {G' : Type u_10}
  [inst_9 : TopologicalSpace G'] {I : ModelWithCorners 𝕜 E H} {J : ModelWithCorners 𝕜 E'' G}
  {J' : ModelWithCorners 𝕜 E''' G'} {M : Type u_11} [inst_10 : TopologicalSpace M] [inst_11 : ChartedSpace H M]
  {N : Type u_13} [inst_12 : TopologicalSpace N] [inst_13 : ChartedSpace G N] {N' : Type u_14}
  [inst_14 : TopologicalSpace N'] [inst_15 : ChartedSpace G' N'] {n : WithTop ℕ∞} {x : M} {f : M → N} {φ : N → N'},
  Manifold.IsImmersionAt J J' n φ (f x) → (ContMDiffAt I J n f x ↔ ContinuousAt f x ∧ ContMDiffAt I J' n (φ ∘ f) x)
-- Mathlib.LinearAlgebra.Matrix.Kronecker
Matrix.kroneckerMap_reindex : ∀ {α : Type u_3} {β : Type u_5} {γ : Type u_7} {l : Type u_9} {m : Type u_10} {n : Type u_11} {p : Type u_12}
  {l' : Type u_15} {m' : Type u_16} {n' : Type u_17} {p' : Type u_18} (f : α → β → γ) (el : l ≃ l') (em : m ≃ m')
  (en : n ≃ n') (ep : p ≃ p') (M : Matrix l m α) (N : Matrix n p β),
  Matrix.kroneckerMap f ((Matrix.reindex el em) M) ((Matrix.reindex en ep) N) =
    (Matrix.reindex (el.prodCongr en) (em.prodCongr ep)) (Matrix.kroneckerMap f M N)
-- Mathlib.Algebra.Order.Archimedean.Class
MulArchimedeanClass.mk_left_le_mk_div_iff : ∀ {M : Type u_1} [inst : CommGroup M] [inst_1 : LinearOrder M] [inst_2 : IsOrderedMonoid M] {a b : M},
  MulArchimedeanClass.mk a ≤ MulArchimedeanClass.mk (a / b) ↔ MulArchimedeanClass.mk a ≤ MulArchimedeanClass.mk b
-- Init.WF
Acc.below.intro : ∀ {α : Sort u} {r : α → α → Prop} {motive : (a : α) → Acc r a → Prop} (x : α) (h : ∀ (y : α), r y x → Acc r y),
  (∀ (y : α) (a : r y x), Acc.below ⋯) → (∀ (y : α) (a : r y x), motive y ⋯) → Acc.below ⋯
-- Mathlib.Data.Finset.Basic
Equiv.piFinsetUnion.eq_1 : ∀ {ι : Type u_5} [inst : DecidableEq ι] (α : ι → Type u_4) {s t : Finset ι} (h : Disjoint s t),
  Equiv.piFinsetUnion α h =
    (Equiv.sumPiEquivProdPi fun b => α ↑((Equiv.Finset.union s t h) b)).symm.trans
      (Equiv.piCongrLeft (fun i => α ↑i) (Equiv.Finset.union s t h))
-- Mathlib.Combinatorics.SimpleGraph.Coloring.EdgeLabeling
/-- An edge labeling of a simple graph `G` with labels in type `K`. Sometimes this is called an
edge-coloring, but we reserve that terminology for labelings where incident edges cannot share a
label.
 -/
SimpleGraph.EdgeLabeling : {V : Type u_1} → SimpleGraph V → Type u_5 → Type (max u_1 u_5)
-- Mathlib.Analysis.InnerProductSpace.Harmonic.HarmonicContOnCl
InnerProductSpace.HarmonicContOnCl.contDiffAt : ∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : InnerProductSpace ℝ E] [inst_2 : FiniteDimensional ℝ E]
  {F : Type u_2} [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace ℝ F] {f : E → F} {x : E} {s : Set E},
  InnerProductSpace.HarmonicContOnCl f s → x ∈ s → ContDiffAt ℝ 2 f x
-- Mathlib.MeasureTheory.MeasurableSpace.Constructions
Sum.instMeasurableSpace : {α : Type u_6} → {β : Type u_7} → [m₁ : MeasurableSpace α] → [m₂ : MeasurableSpace β] → MeasurableSpace (α ⊕ β)
-- Mathlib.CategoryTheory.Limits.Types.ColimitType
/-- the point of the cocone  -/
CategoryTheory.Functor.CoconeTypes.pt : {J : Type u} →
  [inst : CategoryTheory.Category.{v, u} J] → {F : CategoryTheory.Functor J (Type w₀)} → F.CoconeTypes → Type w₁
-- Mathlib.CategoryTheory.Comma.StructuredArrow.Basic
CategoryTheory.StructuredArrow.mapIso_functor_obj_right : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  {S S' : D} {T : CategoryTheory.Functor C D} (i : S ≅ S')
  (X : CategoryTheory.Comma (CategoryTheory.Functor.fromPUnit S) T),
  ((CategoryTheory.StructuredArrow.mapIso i).functor.obj X).right = X.right
-- Lean.Linter.UnusedVariables
/-- A (usually `.ident`) syntax for the defined variable  -/
Lean.Linter.UnusedVariables.FVarDefinition.stx : Lean.Linter.UnusedVariables.FVarDefinition → Lean.Syntax
-- Mathlib.ModelTheory.Arithmetic.Presburger.Semilinear.Defs
IsSemilinearSet.of_fg : ∀ {M : Type u_1} [inst : AddCommMonoid M] {P : AddSubmonoid M}, P.FG → IsSemilinearSet ↑P
-- Mathlib.RingTheory.Valuation.ValuationSubring
ValuationSubring.le_top : ∀ {K : Type u} [inst : Field K] (A : ValuationSubring K), A ≤ ⊤
-- Mathlib.Combinatorics.SimpleGraph.VertexCover
SimpleGraph.isVertexCover_preimage_iso : ∀ {V : Type u_1} {W : Type u_2} {G : SimpleGraph V} {H : SimpleGraph W} (f : G ≃g H) {c : Set W},
  G.IsVertexCover (⇑f ⁻¹' c) ↔ H.IsVertexCover c
-- Mathlib.CategoryTheory.Limits.Cones
CategoryTheory.Functor.functorialityCompPrecompose_hom_app_hom : ∀ {J : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} J] {C : Type u₃} [inst_1 : CategoryTheory.Category.{v₃, u₃} C]
  {D : Type u₄} [inst_2 : CategoryTheory.Category.{v₄, u₄} D] {F : CategoryTheory.Functor J C}
  {H H' : CategoryTheory.Functor C D} (α : H ≅ H') (X : CategoryTheory.Limits.Cocone F),
  ((CategoryTheory.Functor.functorialityCompPrecompose α).hom.app X).hom = α.hom.app X.pt
-- Mathlib.Data.Set.Finite.Basic
Set.Finite.toFinset_ofPred : ∀ {α : Type u} [inst : Fintype α] (p : α → Prop) [inst_1 : DecidablePred p] (h : {x | p x}.Finite),
  h.toFinset = {x | p x}
-- Mathlib.CategoryTheory.Limits.Shapes.Multiequalizer
CategoryTheory.Limits.MulticospanShape.prod_L : ∀ (ι : Type w), (CategoryTheory.Limits.MulticospanShape.prod ι).L = ι
-- Init.Data.Rat.Lemmas
Rat.ofInt_num : ∀ {n : ℤ}, (Rat.ofInt n).num = n
-- Mathlib.Order.Hom.Bounded
BotHom.instOrderBot.eq_1 : ∀ {α : Type u_2} {β : Type u_3} [inst : Bot α] [inst_1 : LE β] [inst_2 : OrderBot β],
  BotHom.instOrderBot = { bot := { toFun := ⊥, map_bot' := ⋯ }, bot_le := ⋯ }
-- Mathlib.Algebra.DirectSum.Algebra
DirectSum.GAlgebra.smul_def : ∀ {ι : Type uι} {R : Type uR} {A : ι → Type uA} {inst : CommSemiring R} {inst_1 : (i : ι) → AddCommMonoid (A i)}
  {inst_2 : (i : ι) → Module R (A i)} {inst_3 : AddMonoid ι} {inst_4 : DirectSum.GSemiring A}
  [self : DirectSum.GAlgebra R A] (r : R) (x : GradedMonoid A),
  r • x = GradedMonoid.mk 0 (DirectSum.GAlgebra.toFun r) * x
-- Mathlib.Geometry.Manifold.VectorField.LieBracket
/-- Variant of `mlieBracketWithin_eventually_congr_set` where one requires the sets to coincide only
in the complement of a point.  -/
VectorField.mlieBracketWithin_eventually_congr_set' : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {H : Type u_2} [inst_1 : TopologicalSpace H] {E : Type u_3}
  [inst_2 : NormedAddCommGroup E] [inst_3 : NormedSpace 𝕜 E] {I : ModelWithCorners 𝕜 E H} {M : Type u_4}
  [inst_4 : TopologicalSpace M] [inst_5 : ChartedSpace H M] {s t : Set M} {x : M} {V W : (x : M) → TangentSpace I x}
  (y : M),
  s =ᶠ[nhdsWithin x {y}ᶜ] t → VectorField.mlieBracketWithin I V W s =ᶠ[nhds x] VectorField.mlieBracketWithin I V W t
-- Mathlib.Order.SuccPred.Basic
coe_succ_of_mem : ∀ {α : Type u_3} [inst : PartialOrder α] {s : Set α} [inst_1 : s.OrdConnected] [inst_2 : SuccOrder α] {a : ↑s},
  Order.succ ↑a ∈ s → ↑(Order.succ a) = Order.succ ↑a
-- Mathlib.Logic.Function.Basic
Function.injective_of_subsingleton : ∀ {α : Sort u_1} {β : Sort u_2} [Subsingleton α] (f : α → β), Function.Injective f
-- Init.Data.SInt.Bitwise
ISize.toInt32_not : ∀ (a : ISize), (~~~a).toInt32 = ~~~a.toInt32
-- Mathlib.Algebra.Lie.IdealOperations
LieSubmodule.map_comap_le : ∀ {R : Type u} {L : Type v} {M : Type w} {M₂ : Type w₁} [inst : CommRing R] [inst_1 : LieRing L]
  [inst_2 : AddCommGroup M] [inst_3 : Module R M] [inst_4 : LieRingModule L M] [inst_5 : AddCommGroup M₂]
  [inst_6 : Module R M₂] [inst_7 : LieRingModule L M₂] (N₂ : LieSubmodule R L M₂) (f : M →ₗ⁅R,L⁆ M₂),
  LieSubmodule.map f (LieSubmodule.comap f N₂) ≤ N₂
-- Init.Data.List.Find
List.lookup_cons_self : ∀ {α : Type u_2} [inst : BEq α] {β : Type u_1} {b : β} {es : List (α × β)} [ReflBEq α] {k : α},
  List.lookup k ((k, b) :: es) = some b
-- Init.Data.String.TakeDrop
/-- If `pat` matches a suffix of `s`, returns the remainder. Returns `s` unmodified
otherwise.

Use `String.dropSuffix?` to return `none` when `pat` does not match a prefix.

This is a cheap operation because it does not allocate a new string to hold the result.
To convert the result into a string, use `String.Slice.copy`.

This function is generic over all currently supported patterns.

Examples:

* `"red green blue".dropSuffix " blue" == "red green".toSlice`

* `"red green blue".dropSuffix "bluu " == "red green blue".toSlice`

* `"red green blue".dropSuffix 'e' == "red green blu".toSlice`

* `"red green blue".dropSuffix Char.isLower == "red green blu".toSlice`
 -/
String.dropSuffix : {ρ : Type} → String → (pat : ρ) → [String.Slice.Pattern.BackwardPattern pat] → String.Slice
-- Mathlib.LinearAlgebra.Matrix.Rank
Matrix.rank_add_rank_le_card_of_mul_eq_zero : ∀ {l : Type ul} {m : Type um} {n : Type un} {R : Type uR} [inst : Fintype n] [inst_1 : Field R] [Finite l]
  [inst_3 : Fintype m] {A : Matrix l m R} {B : Matrix m n R}, A * B = 0 → A.rank + B.rank ≤ Fintype.card m
-- Mathlib.RingTheory.Ideal.Span
instIsPrincipalSpanSingletonSet : ∀ {R : Type u_1} [inst : Semiring R] {x : R}, Submodule.IsPrincipal (Ideal.span {x})
-- Mathlib.Topology.Sets.Compacts
TopologicalSpace.Compacts.map_injective : ∀ {α : Type u_1} {β : Type u_2} [inst : TopologicalSpace α] [inst_1 : TopologicalSpace β] {f : α → β}
  (hf : Continuous f), Function.Injective f → Function.Injective (TopologicalSpace.Compacts.map f hf)
-- Mathlib.ModelTheory.Arithmetic.Presburger.Semilinear.Basic
IsSemilinearSet.exists_fg_eq_subtypeVal : ∀ {M : Type u_1} [inst : AddCommMonoid M] {s : Set M},
  IsSemilinearSet s → ∃ P s', P.FG ∧ IsSemilinearSet s' ∧ s = Subtype.val '' s'
-- Mathlib.Combinatorics.SimpleGraph.Copy
SimpleGraph.isContained_congr_left : ∀ {α : Type u_4} {β : Type u_5} {γ : Type u_6} {A : SimpleGraph α} {B : SimpleGraph β} {C : SimpleGraph γ}
  (e₁ : A ≃g B), A.IsContained C ↔ B.IsContained C
-- Init.Data.List.ToArray
_private.Init.Data.List.ToArray.0.List.getLast?.match_1.splitter : {α : Type u_1} →
  (motive : List α → Sort u_2) →
    (x : List α) → (Unit → motive []) → ((a : α) → (as : List α) → motive (a :: as)) → motive x
-- Mathlib.GroupTheory.Coset.Basic
mem_rightCoset : ∀ {α : Type u_1} [inst : Mul α] {s : Set α} {x : α} (a : α), x ∈ s → x * a ∈ MulOpposite.op a • s
-- Std.Do.Triple.SpecLemmas
List.length_of_range'_eq_append_cons : ∀ {s n step : ℕ} {xs : List ℕ} {cur : ℕ} {ys : List ℕ},
  List.range' s n step = xs ++ cur :: ys → n = xs.length + ys.length + 1
-- Mathlib.Analysis.Analytic.Linear
ContinuousLinearMap.hasFPowerSeriesAt_bilinear : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {F : Type u_3} [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F] {G : Type u_4}
  [inst_5 : NormedAddCommGroup G] [inst_6 : NormedSpace 𝕜 G] (f : E →L[𝕜] F →L[𝕜] G) (x : E × F),
  HasFPowerSeriesAt (fun x => (f x.1) x.2) (f.fpowerSeriesBilinear x) x
-- Init.Core
instNonemptyPProd : ∀ {α : Sort u_1} {β : Sort u_2} [h1 : Nonempty α] [h2 : Nonempty β], Nonempty (α ×' β)
-- Init.Data.Array.Basic
List.size_toArray : ∀ {α : Type u} {as : List α}, as.toArray.size = as.length
-- Mathlib.Algebra.EuclideanDomain.Basic
EuclideanDomain.mod_self : ∀ {R : Type u} [inst : EuclideanDomain R] (a : R), a % a = 0
-- Mathlib.Geometry.Manifold.MFDeriv.Basic
MDifferentiableOn.continuousOn : ∀ {𝕜 : 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] {E' : Type u_5} [inst_6 : NormedAddCommGroup E']
  [inst_7 : NormedSpace 𝕜 E'] {H' : Type u_6} [inst_8 : TopologicalSpace H'] {I' : ModelWithCorners 𝕜 E' H'}
  {M' : Type u_7} [inst_9 : TopologicalSpace M'] [inst_10 : ChartedSpace H' M'] {f : M → M'} {s : Set M},
  MDiff[s] f → ContinuousOn f s
-- Mathlib.Data.Set.FiniteExhaustion
/-- The sequence of sets in a `FiniteExhaustion` are monotonically increasing.  -/
Set.FiniteExhaustion.subset_succ' : ∀ {α : Type u_1} {s : Set α} (self : s.FiniteExhaustion) (n : ℕ), self.toFun n ⊆ self.toFun (n + 1)
-- Mathlib.Order.Bounds.Basic
BddBelow.exists_le : ∀ {γ : Type u_3} [inst : SemilatticeInf γ] {s : Set γ}, BddBelow s → ∀ (x₀ : γ), ∃ x ≤ x₀, ∀ y ∈ s, x ≤ y
-- Init.Data.Slice.List.Lemmas
List.mkSlice_ric_eq_mkSlice_rco : ∀ {α : Type u_1} {xs : List α} {hi : ℕ},
  (Std.Ric.Sliceable.mkSlice xs *...=hi) = Std.Rco.Sliceable.mkSlice xs 0...hi + 1
-- Mathlib.GroupTheory.Coprod.Basic
AddMonoid.Coprod.snd_surjective : ∀ {M : Type u_1} {N : Type u_2} [inst : AddMonoid M] [inst_1 : AddMonoid N], Function.Surjective ⇑AddMonoid.Coprod.snd
-- Init.Data.Slice.List.Basic
Std.Slice.Internal.ListSliceData.mk.inj : ∀ {α : Type u} {list : List α} {stop : Option ℕ} {list_1 : List α} {stop_1 : Option ℕ},
  { list := list, stop := stop } = { list := list_1, stop := stop_1 } → list = list_1 ∧ stop = stop_1
-- Mathlib.Algebra.Polynomial.Laurent
LaurentPolynomial.invOf_T : ∀ {R : Type u_1} [inst : Semiring R] (n : ℤ), ⅟(LaurentPolynomial.T n) = LaurentPolynomial.T (-n)
-- Mathlib.RingTheory.Etale.Basic
Algebra.FormallySmooth.iff_restrictScalars : ∀ {R : Type u} {A : Type v} {B : Type u_1} [inst : CommRing R] [inst_1 : CommRing A] [inst_2 : Algebra R A]
  [inst_3 : CommRing B] [inst_4 : Algebra R B] [inst_5 : Algebra A B] [IsScalarTower R A B] [Algebra.FormallyEtale R A],
  Algebra.FormallySmooth R B ↔ Algebra.FormallySmooth A B
-- Std.Data.TreeSet.Lemmas
Std.TreeSet.max_insert : ∀ {α : Type u} {cmp : α → α → Ordering} {t : Std.TreeSet α cmp} [inst : Std.TransCmp cmp] {k : α},
  (t.insert k).max ⋯ = t.max?.elim k fun k' => if cmp k' k = Ordering.lt then k else k'
-- Mathlib.CategoryTheory.Limits.Shapes.Pullback.Categorical.Basic
CategoryTheory.Limits.CategoricalPullback.CatCommSqOver.iso_hom_naturality : ∀ {A : Type u₁} {B : Type u₂} {C : Type u₃} [inst : CategoryTheory.Category.{v₁, u₁} A]
  [inst_1 : CategoryTheory.Category.{v₂, u₂} B] [inst_2 : CategoryTheory.Category.{v₃, u₃} C]
  {F : CategoryTheory.Functor A B} {G : CategoryTheory.Functor C B} (X : Type u₄)
  [inst_3 : CategoryTheory.Category.{v₄, u₄} X] (S : CategoryTheory.Limits.CategoricalPullback.CatCommSqOver F G X)
  {x x' : X} (f : x ⟶ x'),
  CategoryTheory.CategoryStruct.comp (F.map (S.fst.map f)) (S.iso.hom.app x') =
    CategoryTheory.CategoryStruct.comp (S.iso.hom.app x) (G.map (S.snd.map f))