mathlib-initiative/mathlib-types huggingface dataset:
-- Std.Tactic.BVDecide.Bitblast.BVExpr.Circuit.Impl.Expr
_private.Std.Tactic.BVDecide.Bitblast.BVExpr.Circuit.Impl.Expr.0.Std.Tactic.BVDecide.BVExpr.bitblast.go.match_15.eq_7 : ∀ (motive : Std.Tactic.BVDecide.BVUnOp → Sort u_1) (h_1 : Unit → motive Std.Tactic.BVDecide.BVUnOp.not)
  (h_2 : (distance : ℕ) → motive (Std.Tactic.BVDecide.BVUnOp.rotateLeft distance))
  (h_3 : (distance : ℕ) → motive (Std.Tactic.BVDecide.BVUnOp.rotateRight distance))
  (h_4 : (distance : ℕ) → motive (Std.Tactic.BVDecide.BVUnOp.arithShiftRightConst distance))
  (h_5 : Unit → motive Std.Tactic.BVDecide.BVUnOp.reverse) (h_6 : Unit → motive Std.Tactic.BVDecide.BVUnOp.clz)
  (h_7 : Unit → motive Std.Tactic.BVDecide.BVUnOp.cpop),
  (match Std.Tactic.BVDecide.BVUnOp.cpop with
    | Std.Tactic.BVDecide.BVUnOp.not => h_1 ()
    | Std.Tactic.BVDecide.BVUnOp.rotateLeft distance => h_2 distance
    | Std.Tactic.BVDecide.BVUnOp.rotateRight distance => h_3 distance
    | Std.Tactic.BVDecide.BVUnOp.arithShiftRightConst distance => h_4 distance
    | Std.Tactic.BVDecide.BVUnOp.reverse => h_5 ()
    | Std.Tactic.BVDecide.BVUnOp.clz => h_6 ()
    | Std.Tactic.BVDecide.BVUnOp.cpop => h_7 ()) =
    h_7 ()
-- Mathlib.Data.List.Chain
List.isChain_cons_append_cons_cons : ∀ {α : Type u_1} {R : α → α → Prop} {a b c : α} {l₁ l₂ : List α},
  List.IsChain R (a :: (l₁ ++ b :: c :: l₂)) ↔ List.IsChain R (a :: (l₁ ++ [b])) ∧ R b c ∧ List.IsChain R (c :: l₂)
-- Lean.Meta.Basic
Lean.Meta.getResetPostponed : Lean.MetaM (Lean.PersistentArray Lean.Meta.PostponedEntry)
-- Mathlib.LinearAlgebra.Projection
Submodule.toLinearMap_quotientEquivOfIsCompl : ∀ {R : Type u_1} [inst : Ring R] {E : Type u_2} [inst_1 : AddCommGroup E] [inst_2 : Module R E] {p q : Submodule R E}
  (h : IsCompl p q), ↑(p.quotientEquivOfIsCompl q h) = p.liftQ (q.projectionOnto p ⋯) ⋯
-- Mathlib.Algebra.Order.Monoid.Unbundled.Defs
/-- Typeclass for strict reverse monotonicity of addition on the right,
namely `a₁ * b < a₂ * b → a₁ < a₂`.

You should usually not use this very granular typeclass directly, but rather a typeclass like
`IsOrderedAddMonoid`.  -/
AddRightReflectLT : (M : Type u_1) → [Add M] → [LT M] → Prop
-- Mathlib.Data.Set.Lattice
Set.BijOn.iUnion_comp : ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} {s : Set β} {t : Set γ} {f : β → γ} (g : γ → Set α),
  Set.BijOn f s t → ⋃ x ∈ s, g (f x) = ⋃ y ∈ t, g y
-- Mathlib.Data.Finset.Card
Finset.card_lt_card : ∀ {α : Type u_1} {s t : Finset α}, s ⊂ t → s.card < t.card
-- Mathlib.Algebra.Field.Periodic
Function.Periodic.image_uIcc : ∀ {α : Type u_1} {β : Type u_2} {f : α → β} {c : α} [inst : AddCommGroup α] [inst_1 : LinearOrder α]
  [IsOrderedAddMonoid α] [Archimedean α],
  Function.Periodic f c → c ≠ 0 → ∀ (a : α), f '' Set.uIcc a (a + c) = Set.range f
-- Mathlib.Topology.Sets.Closeds
/-- Reinterpret a clopen as a closed.  -/
TopologicalSpace.Clopens.toCloseds : {α : Type u_2} → [inst : TopologicalSpace α] → TopologicalSpace.Clopens α → TopologicalSpace.Closeds α
-- Mathlib.Algebra.Homology.ComplexShape
ComplexShape.subsingleton_prev : ∀ {ι : Type u_1} (c : ComplexShape ι) (i : ι), Subsingleton { j // c.Rel j i }
-- Mathlib.Algebra.Ring.Subsemiring.Defs
Subsemiring.instPartialOrder : {R : Type u} → [inst : NonAssocSemiring R] → PartialOrder (Subsemiring R)
-- Mathlib.Order.Closure
OrderIso.equivClosureOperator_apply : ∀ {α : Type u_4} {β : Type u_5} [inst : Preorder α] [inst_1 : Preorder β] (e : α ≃o β) (c : ClosureOperator α),
  e.equivClosureOperator c = c.conjBy e
-- Mathlib.Combinatorics.Enumerative.Composition
Composition.blocksFun_mem_blocks : ∀ {n : ℕ} (c : Composition n) (i : Fin c.length), c.blocksFun i ∈ c.blocks
-- Mathlib.RingTheory.Perfection
/-- A variant of `PreTilt.coeff_iterate_frobenius` using `m-n` and `n`.  -/
PreTilt.coeff_iterate_frobenius' : ∀ {O : Type u₂} [inst : CommRing O] {p : ℕ} [inst_1 : Fact (Nat.Prime p)] [inst_2 : Fact ¬IsUnit ↑p] (x : PreTilt O p)
  {m n : ℕ}, m ≤ n → (PreTilt.coeff n) ((⇑(frobenius (PreTilt O p) p))^[m] x) = (PreTilt.coeff (n - m)) x
-- Init.CbvSimproc
/-- A user-defined simplification procedure used by the `cbv` tactic.
The body must have type `Lean.Meta.Sym.Simp.Simproc` (`Expr → SimpM Result`).
Procedures are indexed by a discrimination tree pattern and fire at one of three phases:
`↓` (pre), `cbv_eval` (eval), or `↑` (post, default).
 -/
Lean.Parser.«command__Cbv_simproc____(_):=_» : Lean.ParserDescr
-- Std.Data.Internal.List.Associative
/-- Internal implementation detail of the hash map  -/
Std.Internal.List.insertList : {α : Type u} → {β : α → Type v} → [BEq α] → List ((a : α) × β a) → List ((a : α) × β a) → List ((a : α) × β a)
-- Mathlib.CategoryTheory.Sites.Point.Basic
/-- Given a point `Φ` of a site `(C, J)`, `X : C` and `x : Φ.fiber.obj X`,
this is the map `P.obj (op X) ⟶ Φ.presheafFiber.obj P` for any `P : Cᵒᵖ ⥤ A`
as a natural transformation.  -/
CategoryTheory.GrothendieckTopology.Point.toPresheafFiberNatTrans : {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.Limits.HasColimitsOfSize.{w, w, v', u'} A] →
              (X : C) → Φ.fiber.obj X → ((CategoryTheory.evaluation Cᵒᵖ A).obj (Opposite.op X) ⟶ Φ.presheafFiber)
-- Mathlib.MeasureTheory.MeasurableSpace.Constructions
measurable_diag' : ∀ {α : Type u_1} {m m' : MeasurableSpace α}, m' ≤ m → Measurable Function.diag
-- Mathlib.CategoryTheory.Limits.Preserves.Opposites
/-- If `F.rightOp : C ⥤ Dᵒᵖ` preserves colimits, then `F : Cᵒᵖ ⥤ D` preserves limits.  -/
CategoryTheory.Limits.preservesLimits_of_rightOp : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  (F : CategoryTheory.Functor Cᵒᵖ D) [CategoryTheory.Limits.PreservesColimits F.rightOp],
  CategoryTheory.Limits.PreservesLimits F
-- Std.Data.ExtTreeSet.Lemmas
Std.ExtTreeSet.toList_eq_nil_iff : ∀ {α : Type u} {cmp : α → α → Ordering} {t : Std.ExtTreeSet α cmp} [inst : Std.TransCmp cmp], t.toList = [] ↔ t = ∅
-- Mathlib.RingTheory.LinearDisjoint
/-- In a commutative ring, if a basis of `A` is also `B`-linearly independent,
then `A` and `B` are linearly disjoint.  -/
Subalgebra.LinearDisjoint.of_basis_left : ∀ {R : Type u} {S : Type v} [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : Algebra R S] (A B : Subalgebra R S)
  {ι : Type u_1} (a : Module.Basis ι R ↥A), LinearIndependent (↥B) (⇑A.val ∘ ⇑a) → A.LinearDisjoint B
-- Mathlib.RingTheory.RingHom.QuasiFinite
/-- If `T` is both a finite type `R`-algebra, and the localization of an integral `R`-algebra,
then `T` is quasi-finite over `R`  -/
RingHom.QuasiFinite.of_isIntegral_of_finiteType : ∀ {R : Type u_6} {S : Type u_7} {T : Type u_8} [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : CommRing T]
  {f : R →+* S},
  f.IsIntegral → ∀ {g : S →+* T}, g.IsStandardOpenImmersion → (g.comp f).FiniteType → (g.comp f).QuasiFinite
-- Std.Http.Data.Chunk
/-- Attempts to create an `ExtensionName` from a `String`, returning `none` if the string contains
invalid characters or is empty.
 -/
Std.Http.Chunk.ExtensionName.ofString? : String → Option Std.Http.Chunk.ExtensionName
-- Mathlib.Analysis.SpecialFunctions.Trigonometric.Inverse
Real.mapsTo_sin_Ioo : Set.MapsTo Real.sin (Set.Ioo (-(Real.pi / 2)) (Real.pi / 2)) (Set.Ioo (-1) 1)
-- Mathlib.Algebra.Pointwise.Stabilizer
AddAction.stabilizer_subset_sub_right : ∀ {G : Type u_1} [inst : AddGroup G] {a : G} {s : Set G}, a ∈ s → ↑(AddAction.stabilizer G s) ⊆ s - {a}
-- Mathlib.Algebra.Group.Prod
AddMonoidHom.coprod_comp_inl : ∀ {M : Type u_3} {N : Type u_4} {P : Type u_5} [inst : AddZeroClass M] [inst_1 : AddZeroClass N]
  [inst_2 : AddCommMonoid P] (f : M →+ P) (g : N →+ P), (f.coprod g).comp (AddMonoidHom.inl M N) = f
-- Mathlib.Analysis.Calculus.ContDiff.Defs
/-- If a function is `C^n` with `n ≥ 1` at a point, then it is differentiable there.  -/
ContDiffAt.differentiableAt : ∀ {𝕜 : Type u} [inst : NontriviallyNormedField 𝕜] {E : Type uE} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {F : Type uF} [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F] {f : E → F}
  {x : E} {n : WithTop ℕ∞}, ContDiffAt 𝕜 n f x → n ≠ 0 → DifferentiableAt 𝕜 f x
-- Mathlib.RingTheory.Ideal.Quotient.ChineseRemainder
/-- A form of Chinese remainder theorem for modules, part II: if ideals `Iᵢ` of `R` are pairwise
coprime, then for any `R`-module `M`, the kernel of `M → Πᵢ (R ⧸ Iᵢ) ⊗[R] M` equals `(⋂ᵢ Iᵢ) • M`.
 -/
Ideal.ker_tensorProductMk_quotient : ∀ {R : Type u_1} [inst : CommRing R] {ι : Type u_2} (M : Type u_3) [inst_1 : AddCommGroup M] [inst_2 : Module R M]
  (I : ι → Ideal R),
  Pairwise (Function.onFun IsCoprime I) →
    ∀ [Finite ι], (LinearMap.pi fun i => (TensorProduct.mk R (R ⧸ I i) M) 1).ker = (⨅ i, I i) • ⊤
-- Lean.Data.Json.Elab
/-- Json object syntax.  -/
Lean.Json.«json{_}» : Lean.ParserDescr
-- Mathlib.Topology.MetricSpace.IsometricSMul
/-- **Alias** of `Metric.preimage_add_left_eball`. -/
EMetric.preimage_add_left_ball : ∀ {G : Type v} [inst : AddGroup G] [inst_1 : PseudoEMetricSpace G] [IsIsometricVAdd G G] (a b : G) (r : ENNReal),
  (fun x => a + x) ⁻¹' Metric.eball b r = Metric.eball (-a + b) r
-- Mathlib.SetTheory.Cardinal.Finite
ENat.card_eq_coe_fintype_card : ∀ {α : Type u_1} [inst : Fintype α], ENat.card α = ↑(Fintype.card α)
-- Mathlib.Order.Filter.EventuallyConst
Filter.EventuallyConst.bot : ∀ {α : Type u_1} {β : Type u_2} {f : α → β}, Filter.EventuallyConst f ⊥
-- Mathlib.AlgebraicTopology.SimplexCategory.Augmented.Basic
AugmentedSimplexCategory.equivAugmentedCosimplicialObject_counitIso_inv_app_left : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C]
  (X :
    CategoryTheory.Comma (CategoryTheory.Functor.const SimplexCategory)
      (CategoryTheory.Functor.id (CategoryTheory.Functor SimplexCategory C))),
  (AugmentedSimplexCategory.equivAugmentedCosimplicialObject.counitIso.inv.app X).left =
    CategoryTheory.CategoryStruct.id X.left
-- Mathlib.Algebra.Ring.BooleanRing
ofBoolAlg_toBoolAlg : ∀ {α : Type u_1} (a : α), ofBoolAlg (toBoolAlg a) = a
-- Mathlib.RingTheory.Extension.Basic
Algebra.Extension.commRing : {R : Type u} →
  {S : Type v} →
    [inst : CommRing R] →
      [inst_1 : CommRing S] → [inst_2 : Algebra R S] → (self : Algebra.Extension R S) → CommRing self.Ring
-- Mathlib.Topology.UnitInterval
Set.Icc.addNSMul_eq_right : ∀ {α : Type u_1} [inst : AddCommGroup α] [inst_1 : LinearOrder α] [IsOrderedAddMonoid α] {a b : α} (h : a ≤ b) {δ : α}
  [Archimedean α], 0 < δ → ∃ m, ∀ n ≥ m, ↑(Set.Icc.addNSMul h δ n) = b
-- Lean.Compiler.IR.CompilerM
Lean.IR.findEnvDecl' : Lean.Environment → Lean.Name → Array Lean.IR.Decl → Option Lean.IR.Decl
-- Init.Data.Char.Lemmas
Char.lt_irrefl : ∀ (a : Char), ¬a < a
-- Mathlib.RingTheory.MvPolynomial.Symmetric.FundamentalTheorem
AddMonoidAlgebra.supDegree.eq_1 : ∀ {R : Type u_1} {A : Type u_3} {B : Type u_5} [inst : Semiring R] [inst_1 : SemilatticeSup B] [inst_2 : OrderBot B]
  (D : A → B) (f : AddMonoidAlgebra R A), AddMonoidAlgebra.supDegree D f = f.coeff.support.sup D
-- Lean.Parser.Command
Lean.Parser.Command.universe.formatter : Lean.PrettyPrinter.Formatter
-- Mathlib.Tactic.ClickSuggestions.ApplyAt
Mathlib.Tactic.ClickSuggestions.instInhabitedApplyAtKey.default : Mathlib.Tactic.ClickSuggestions.ApplyAtKey
-- Mathlib.LinearAlgebra.Trace
LinearMap.llcomp.congr_simp : ∀ {R : Type u_2} [inst : CommSemiring R] {R₂ : Type u_14} (R₃ : Type u_15) (M : Type u_17) (N : Type u_18)
  (P : Type u_19) [inst_1 : CommSemiring R₂] [inst_2 : CommSemiring R₃] [inst_3 : AddCommMonoid M]
  [inst_4 : AddCommMonoid N] [inst_5 : AddCommMonoid P] [inst_6 : Module R M] [inst_7 : Module R₂ N]
  [inst_8 : Module R₃ P] {σ₁₂ : R →+* R₂} {σ₁₃ : R →+* R₃} {σ₂₃ : R₂ →+* R₃} [inst_9 : RingHomCompTriple σ₁₂ σ₂₃ σ₁₃],
  LinearMap.llcomp R₃ M N P = LinearMap.llcomp R₃ M N P
-- Mathlib.CategoryTheory.Triangulated.Subcategory
CategoryTheory.ObjectProperty.instIsClosedUnderFiniteProductsOfIsTriangulatedOfIsClosedUnderIsomorphisms : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Limits.HasZeroObject C]
  [inst_2 : CategoryTheory.HasShift C ℤ] [inst_3 : CategoryTheory.Preadditive C]
  [inst_4 : ∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive] [inst_5 : CategoryTheory.Pretriangulated C]
  (P : CategoryTheory.ObjectProperty C) [P.IsTriangulated] [P.IsClosedUnderIsomorphisms], P.IsClosedUnderFiniteProducts
-- Aesop.Script.StructureStatic
Aesop.Script.StaticStructureM.State.mk.injEq : ∀ (perfect perfect_1 : Bool), ({ perfect := perfect } = { perfect := perfect_1 }) = (perfect = perfect_1)
-- Mathlib.CategoryTheory.Triangulated.Opposite.Basic
CategoryTheory.Pretriangulated.shiftFunctorZero_op_inv_app : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.HasShift C ℤ] (X : Cᵒᵖ),
  (CategoryTheory.shiftFunctorZero Cᵒᵖ ℤ).inv.app X =
    CategoryTheory.CategoryStruct.comp ((CategoryTheory.shiftFunctorZero C ℤ).hom.app (Opposite.unop X)).op
      ((CategoryTheory.Pretriangulated.shiftFunctorOpIso C 0 0 ⋯).inv.app X)
-- Init.Core
DoResultSBC.pureReturn.inj : ∀ {α σ : Type u} {a : α} {a_1 : σ} {a_2 : α} {a_3 : σ},
  DoResultSBC.pureReturn a a_1 = DoResultSBC.pureReturn a_2 a_3 → a = a_2 ∧ a_1 = a_3
-- Mathlib.AlgebraicGeometry.EllipticCurve.DivisionPolynomial.Basic
WeierstrassCurve.Affine.CoordinateRing.mk_φ : ∀ {R : Type r} [inst : CommRing R] (W : WeierstrassCurve R) (n : ℤ),
  (WeierstrassCurve.Affine.CoordinateRing.mk W) (W.φ n) =
    (WeierstrassCurve.Affine.CoordinateRing.mk W) (Polynomial.C (W.Φ n))
-- Mathlib.CategoryTheory.Preadditive.CommGrp_
CategoryTheory.Preadditive.inv_def : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Preadditive C]
  [inst_2 : CategoryTheory.CartesianMonoidalCategory C] (X : C),
  CategoryTheory.GrpObj.inv = -CategoryTheory.CategoryStruct.id X
-- Mathlib.CategoryTheory.Presentable.IsCardinalFiltered
CategoryTheory.isCardinalFiltered_of_hasTerminal : ∀ (J : Type u) [inst : CategoryTheory.Category.{v, u} J] [CategoryTheory.Limits.HasTerminal J] (κ : Cardinal.{w})
  [inst_2 : Fact κ.IsRegular], CategoryTheory.IsCardinalFiltered J κ
-- Std.Sat.AIG.CNF
/-- Produce a Tseitin style CNF for a `Decl.atom`, using `output` as the tree node variable.
 -/
_private.Std.Sat.AIG.CNF.0.Std.Sat.AIG.Decl.atomToCNF : {α : Type u_1} → α → α → Std.Sat.CNF α
-- Mathlib.Topology.ExtremallyDisconnected
/-- Lemma 2.1 in [Gleason, *Projective topological spaces*][gleason1958]:
if $\rho$ is a continuous surjection from a topological space $E$ to a topological space $A$
satisfying the "Zorn subset condition", then $\rho(G)$ is contained in
the closure of $A \setminus \rho(E \setminus G)$ for any open set $G$ of $E$.  -/
image_subset_closure_compl_image_compl_of_isOpen : ∀ {A E : Type u} [inst : TopologicalSpace A] [inst_1 : TopologicalSpace E] {ρ : E → A},
  Continuous ρ →
    Function.Surjective ρ →
      (∀ (E₀ : Set E), E₀ ≠ Set.univ → IsClosed E₀ → ρ '' E₀ ≠ Set.univ) →
        ∀ {G : Set E}, IsOpen G → ρ '' G ⊆ closure (ρ '' Gᶜ)ᶜ
-- Init.System.IO
/-- Returns the process ID of the calling process.  -/
IO.Process.getPID : BaseIO UInt32
-- Mathlib.Analysis.InnerProductSpace.ExteriorPower
exteriorPower.instNormedAddCommGroupSubtypeExteriorAlgebraRealMemSubmoduleExteriorPowerOfFiniteDimensional : {n : ℕ} →
  {E : Type u_1} →
    [inst : NormedAddCommGroup E] →
      [inst_1 : InnerProductSpace ℝ E] → [FiniteDimensional ℝ E] → NormedAddCommGroup ↥(⋀[ℝ]^n E)
-- Mathlib.Analysis.Normed.Ring.Basic
MulOpposite.instSeminormedCommRing : {α : Type u_2} → [SeminormedCommRing α] → SeminormedCommRing αᵐᵒᵖ
-- Mathlib.Algebra.Homology.HomotopyCategory.ShiftSequence
HomotopyCategory.homologyShiftIso_hom_app : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Preadditive C]
  [inst_2 : CategoryTheory.CategoryWithHomology C] (n a a' : ℤ) (ha' : n + a = a') (K : CochainComplex C ℤ),
  ((HomotopyCategory.homologyFunctor C (ComplexShape.up ℤ) 0).shiftIso n a a' ha').hom.app
      ((HomotopyCategory.quotient C (ComplexShape.up ℤ)).obj K) =
    CategoryTheory.CategoryStruct.comp
      ((HomotopyCategory.homologyFunctor C (ComplexShape.up ℤ) a).map
        ((CategoryTheory.Functor.commShiftIso (HomotopyCategory.quotient C (ComplexShape.up ℤ)) n).inv.app K))
      (CategoryTheory.CategoryStruct.comp
        ((HomotopyCategory.homologyFunctorFactors C (ComplexShape.up ℤ) a).hom.app
          ((CategoryTheory.shiftFunctor (HomologicalComplex C (ComplexShape.up ℤ)) n).obj K))
        (CategoryTheory.CategoryStruct.comp
          (((HomologicalComplex.homologyFunctor C (ComplexShape.up ℤ) 0).shiftIso n a a' ha').hom.app K)
          ((HomotopyCategory.homologyFunctorFactors C (ComplexShape.up ℤ) a').inv.app K)))
-- Mathlib.Algebra.LieRinehartAlgebra.Subalgebra
instInhabitedLieRinehartSubalgebra : (A : Type u_1) →
  (L : Type u_2) →
    [inst : CommRing A] → [inst_1 : LieRing L] → [inst_2 : Module A L] → Inhabited (LieRinehartSubalgebra A L)
-- Mathlib.Analysis.Normed.Module.Multilinear.Basic
ContinuousMultilinearMap.compContinuousLinearMapContinuousMultilinear_apply_apply : ∀ (𝕜 : Type u) {ι : Type v} (E : ι → Type wE) (E₁ : ι → Type wE₁) (G : Type wG) [inst : NontriviallyNormedField 𝕜]
  [inst_1 : (i : ι) → SeminormedAddCommGroup (E i)] [inst_2 : (i : ι) → NormedSpace 𝕜 (E i)]
  [inst_3 : (i : ι) → SeminormedAddCommGroup (E₁ i)] [inst_4 : (i : ι) → NormedSpace 𝕜 (E₁ i)]
  [inst_5 : SeminormedAddCommGroup G] [inst_6 : NormedSpace 𝕜 G] [inst_7 : Fintype ι] (f : (i : ι) → E i →L[𝕜] E₁ i)
  (g : ContinuousMultilinearMap 𝕜 E₁ G),
  ((ContinuousMultilinearMap.compContinuousLinearMapContinuousMultilinear 𝕜 E E₁ G) f) g = g.compContinuousLinearMap f
-- Mathlib.LinearAlgebra.Matrix.Invertible
/-- If matrices `A`, `C`, and `C⁻¹ + V * A⁻¹ * U` are invertible, then so is `A + U * C * V`.  -/
Matrix.invertibleAddMulMul : {m : Type u_1} →
  {n : Type u_2} →
    {α : Type u_3} →
      [inst : Fintype n] →
        [inst_1 : DecidableEq n] →
          [inst_2 : Fintype m] →
            [inst_3 : DecidableEq m] →
              [inst_4 : Ring α] →
                (A : Matrix n n α) →
                  (U : Matrix n m α) →
                    (C : Matrix m m α) →
                      (V : Matrix m n α) →
                        [inst_5 : Invertible A] →
                          [inst_6 : Invertible C] → [Invertible (⅟C + V * ⅟A * U)] → Invertible (A + U * C * V)
-- Mathlib.RingTheory.HahnSeries.Lex
/-- For `Archimedean` coefficients, there is a correspondence between
archimedean classes (with top) and `HahnSeries.orderTop`.  -/
HahnSeries.archimedeanClassOrderIsoWithTop : (Γ : Type u_1) →
  (R : Type u_2) →
    [inst : LinearOrder Γ] →
      [inst_1 : LinearOrder R] →
        [inst_2 : AddCommGroup R] →
          [inst_3 : IsOrderedAddMonoid R] →
            [Archimedean R] → [Nontrivial R] → ArchimedeanClass (Lex (HahnSeries Γ R)) ≃o WithTop Γ
-- Mathlib.Order.Category.PartOrd
partOrd_dual_comp_forget_to_preord : PartOrd.dual.comp (CategoryTheory.forget₂ PartOrd Preord) = (CategoryTheory.forget₂ PartOrd Preord).comp Preord.dual
-- Std.Data.ExtDHashMap.Lemmas
Std.ExtDHashMap.not_insert_eq_empty : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} {β : α → Type v} {m : Std.ExtDHashMap α β} [inst : EquivBEq α]
  [inst_1 : LawfulHashable α] {k : α} {v : β k}, ¬m.insert k v = ∅
-- Mathlib.CategoryTheory.Limits.MorphismProperty
CategoryTheory.StructuredArrow.closedUnderColimitsOfShape_discrete_empty : ∀ {T : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} T] (P : CategoryTheory.MorphismProperty T) {A : Type u_2}
  [inst_1 : CategoryTheory.Category.{v_2, u_2} A] {L : CategoryTheory.Functor A T} [L.Faithful] [L.Full] {Y : A}
  [P.ContainsIdentities] [P.RespectsIso],
  (CategoryTheory.MorphismProperty.structuredArrowObj L P).IsClosedUnderColimitsOfShape
    (CategoryTheory.Discrete PEmpty.{1})
-- Mathlib.LinearAlgebra.Span.Basic
Submodule.comap_map_sup_of_comap_le : ∀ {R : Type u_1} {R₂ : Type u_2} {M : Type u_4} {M₂ : Type u_5} [inst : Semiring R] [inst_1 : Semiring R₂]
  [inst_2 : AddCommGroup M] [inst_3 : Module R M] [inst_4 : AddCommGroup M₂] [inst_5 : Module R₂ M₂] {τ₁₂ : R →+* R₂}
  [inst_6 : RingHomSurjective τ₁₂] {f : M →ₛₗ[τ₁₂] M₂} {p : Submodule R M} {q : Submodule R₂ M₂},
  Submodule.comap f q ≤ p → Submodule.comap f (Submodule.map f p ⊔ q) = p
-- Lean.Data.Lsp.LanguageFeatures
Lean.Lsp.SignatureHelpTriggerKind.triggerCharacter : Lean.Lsp.SignatureHelpTriggerKind
-- Mathlib.Topology.Algebra.Group.Defs
/-- Eta-expanded form of `ContinuousAt.inv` -/
ContinuousAt.fun_inv : ∀ {G : Type u_1} {X : Type u_3} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace G] [inst_2 : Inv G]
  [ContinuousInv G] {f : X → G} {x : X}, ContinuousAt f x → ContinuousAt (fun i => (f i)⁻¹) x
-- Mathlib.Order.Heyting.Hom
CoheytingHomClass.toLatticeHomClass : ∀ {F : Type u_6} {α : Type u_7} {β : Type u_8} {inst : CoheytingAlgebra α} {inst_1 : CoheytingAlgebra β}
  {inst_2 : FunLike F α β} [self : CoheytingHomClass F α β], LatticeHomClass F α β
-- Init.Data.Float.Model.Float32
Float32.Model.instDecidableLE : DecidableLE Float32.Model
-- Mathlib.Algebra.CharP.Lemmas
sub_pow_expChar_pow_of_commute : ∀ {R : Type u_1} [inst : Ring R] {x y : R} (p n : ℕ) [hR : ExpChar R p],
  Commute x y → (x - y) ^ p ^ n = x ^ p ^ n - y ^ p ^ n
-- Mathlib.Order.Category.Preord
/-- Use the `ConcreteCategory.hom` projection for `@[simps]` lemmas.  -/
Preord.Hom.Simps.hom : (X Y : Preord) → X.Hom Y → ↑X →o ↑Y
-- Mathlib.Geometry.Group.Growth.LinearLowerBound
/-- The growth of a set generating an infinite group is at least linear.  -/
Finset.add_nonneg_card_nsmul : ∀ {G : Type u_1} [inst : AddGroup G] [inst_1 : DecidableEq G] {X : Finset G},
  0 ∈ X → (↑(AddSubgroup.closure ↑X)).Infinite → ∀ (n : ℕ), n + 1 ≤ (n • X).card
-- Mathlib.RepresentationTheory.Homological.GroupHomology.LowDegree
groupHomology.eq_d₂₁_comp_inv : ∀ {k G : Type u} [inst : CommRing k] [inst_1 : Group G] (A : Rep.{u, u, u} k G),
  CategoryTheory.CategoryStruct.comp (groupHomology.chainsIso₂ A).inv ((groupHomology.inhomogeneousChains A).d 2 1) =
    CategoryTheory.CategoryStruct.comp (groupHomology.d₂₁ A) (groupHomology.chainsIso₁ A).inv
-- Mathlib.Topology.UnitInterval
unitInterval.two_mul_sub_one_mem_iff : ∀ {t : ℝ}, 2 * t - 1 ∈ unitInterval ↔ t ∈ Set.Icc (1 / 2) 1
-- Init.Grind.Ring.Basic
Lean.Grind.Semiring.toAdd : {α : Type u} → [self : Lean.Grind.Semiring α] → Add α
-- Mathlib.Topology.Bornology.Absorbs
/-- A set `s` absorbs another set `t` if `t` is contained in all scalings of `s`
by all but a bounded set of elements.  -/
Absorbs : (M : Type u_1) → {α : Type u_2} → [Bornology M] → [SMul M α] → Set α → Set α → Prop
-- Mathlib.Probability.Independence.BoundedContinuousFunction
indepSets_comap_process_of_prod_bcf : ∀ {Ω : Type u_1} {S : Type u_2} {mΩ : MeasurableSpace Ω} {P : MeasureTheory.Measure Ω} {E : S → Type u_4}
  [inst : (s : S) → TopologicalSpace (E s)] [inst_1 : (s : S) → MeasurableSpace (E s)] [∀ (s : S), BorelSpace (E s)]
  [∀ (s : S), HasOuterApproxClosed (E s)] {X : (s : S) → Ω → E s} [MeasureTheory.IsProbabilityMeasure P]
  {𝒜 : Set (Set Ω)},
  (∀ A ∈ 𝒜, MeasureTheory.NullMeasurableSet A P) →
    (∀ (s : S), AEMeasurable (X s) P) →
      (∀ A ∈ 𝒜,
          ∀ (I : Finset S) (f : (s : ↥I) → BoundedContinuousFunction (E ↑s) ℝ),
            ∫ (ω : Ω) in A, ∏ s, (f s) (X (↑s) ω) ∂P = P.real A * ∫ (ω : Ω), ∏ s, (f s) (X (↑s) ω) ∂P) →
        ProbabilityTheory.IndepSets 𝒜 {A | MeasurableSet A} P
-- Mathlib.RingTheory.MatrixAlgebra
kroneckerTMulAlgEquiv_symm_single_tmul : ∀ (l : Type u_1) (m : Type u_2) (n : Type u_3) (p : Type u_4) (R : Type u_5) (S : Type u_6) (M : Type u_9)
  (N : Type u_10) [inst : CommSemiring R] [inst_1 : Semiring S] [inst_2 : AddCommMonoid M] [inst_3 : AddCommMonoid N]
  [inst_4 : Algebra R S] [inst_5 : Module R M] [inst_6 : Module S M] [inst_7 : Module R N]
  [inst_8 : IsScalarTower R S M] [inst_9 : Fintype l] [inst_10 : Fintype m] [inst_11 : Fintype n] [inst_12 : Fintype p]
  [inst_13 : DecidableEq l] [inst_14 : DecidableEq m] [inst_15 : DecidableEq n] [inst_16 : DecidableEq p] (ia : l)
  (ja : m) (ib : n) (jb : p) (a : M) (b : N),
  (kroneckerTMulLinearEquiv l m n p R S M N).symm (Matrix.single (ia, ib) (ja, jb) (a ⊗ₜ[R] b)) =
    Matrix.single ia ja a ⊗ₜ[R] Matrix.single ib jb b