mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.LinearAlgebra.QuadraticForm.Signature
_private.Mathlib.LinearAlgebra.QuadraticForm.Signature.0.QuadraticForm.negSemidef_spanSubset : ∀ {𝕜 : Type u_4} [inst : Field 𝕜] [inst_1 : LinearOrder 𝕜] {ι : Type u_5} [inst_2 : Fintype ι] {w : ι → 𝕜}
  [IsStrictOrderedRing 𝕜] (s : Set ι),
  (∀ i ∈ s, w i ≤ 0) → ∀ x ∈ Pi.spanSubset 𝕜 s, (QuadraticMap.weightedSumSquares 𝕜 w) x ≤ 0
-- Mathlib.Analysis.RCLike.ContinuousMap
ContinuousMap.realToRCLike_lt_realToRCLike_iff : ∀ {X : Type u_1} (𝕜 : Type u_2) [inst : TopologicalSpace X] [inst_1 : RCLike 𝕜] {f g : C(X, ℝ)},
  ContinuousMap.realToRCLike 𝕜 f < ContinuousMap.realToRCLike 𝕜 g ↔ f < g
-- Mathlib.Algebra.Category.Grp.Basic
/-- Turn a morphism in `AddGrpCat` back into an `AddMonoidHom`.  -/
AddGrpCat.Hom.hom : {X Y : AddGrpCat} → X.Hom Y → ↑X →+ ↑Y
-- Aesop.Forward.LevelIndex
Aesop.instOrdLevelIndex.ord : Aesop.LevelIndex → Aesop.LevelIndex → Ordering
-- Mathlib.Algebra.Module.Torsion.Basic
Module.isTorsionBySet_iff_subset_annihilator : ∀ (R : Type u_1) (M : Type u_2) [inst : Semiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M] {s : Set R},
  Module.IsTorsionBySet R M s ↔ s ⊆ ↑(Module.annihilator R M)
-- Lean.Compiler.NameMangling
_private.Lean.Compiler.NameMangling.0.String.pushHex.match_1.congr_eq_2 : ∀ (motive : ℕ → Sort u_1) (n : ℕ) (h_1 : Unit → motive 0) (h_2 : (k : ℕ) → motive k.succ) (k : ℕ),
  n = k.succ →
    (match n with
      | 0 => h_1 ()
      | k.succ => h_2 k) ≍
      h_2 k
-- Mathlib.Topology.Algebra.ConstMulAction
OrderDual.continuousConstVAdd' : ∀ {M : Type u_1} {α : Type u_2} [inst : TopologicalSpace α] [inst_1 : VAdd M α] [ContinuousConstVAdd M α],
  ContinuousConstVAdd Mᵒᵈ α
-- Std.Sat.AIG.RelabelNat
/-- Proof that we never reuse a number.
 -/
Std.Sat.AIG.RelabelNat.State.inv1 : ∀ {α : Type} [inst : DecidableEq α] [inst_1 : Hashable α] {decls : Array (Std.Sat.AIG.Decl α)} {idx : ℕ}
  (self : Std.Sat.AIG.RelabelNat.State α decls idx), Std.Sat.AIG.RelabelNat.State.Inv1 self.max self.map
-- Mathlib.LinearAlgebra.Matrix.Orthogonal
Matrix.HasOrthogonalCols.transpose_hasOrthogonalRows : ∀ {α : Type u_1} {n : Type u_2} {m : Type u_3} [inst : Mul α] [inst_1 : AddCommMonoid α] {A : Matrix m n α}
  [inst_2 : Fintype m], A.HasOrthogonalCols → A.transpose.HasOrthogonalRows
-- Mathlib.FieldTheory.AbelRuffini
IsSolvableByRad.mul : ∀ {F : Type u_1} {E : Type u_2} [inst : Field F] [inst_1 : Field E] [inst_2 : Algebra F E] (α β : E),
  IsSolvableByRad F α → IsSolvableByRad F β → IsSolvableByRad F (α * β)
-- Init.Data.Nat.Lemmas
Nat.add_left_max_self : ∀ {a b : ℕ}, max (b + a) a = b + a
-- Mathlib.AlgebraicGeometry.Modules.Tilde
AlgebraicGeometry.tilde.isIso_toOpen_top : ∀ {R : CommRingCat} {M : ModuleCat ↑R}, CategoryTheory.IsIso (AlgebraicGeometry.tilde.toOpen M ⊤)
-- Init.Data.Nat.Coprime
Nat.Coprime.coprime_mul_right : ∀ {m k n : ℕ}, (m * k).Coprime n → m.Coprime n
-- Mathlib.Logic.Function.Basic
Function.Surjective.bijective₂_of_injective : ∀ {α : Sort u_1} {β : Sort u_2} {γ : Sort u_3} {f : α → β} {g : γ → α},
  Function.Surjective f →
    Function.Surjective g → Function.Injective (f ∘ g) → Function.Bijective f ∧ Function.Bijective g
-- Mathlib.Analysis.Asymptotics.Defs
/-- **Alias** of the reverse direction of `Asymptotics.isBigO_abs_abs`. -/
Asymptotics.IsBigO.abs_abs : ∀ {α : Type u_1} {l : Filter α} {u v : α → ℝ}, u =O[l] v → (fun x => |u x|) =O[l] fun x => |v x|
-- Mathlib.MeasureTheory.Function.StronglyMeasurable.Basic
MeasureTheory.SimpleFunc.stronglyMeasurable : ∀ {α : Type u_1} {β : Type u_2} {x : MeasurableSpace α} [inst : TopologicalSpace β] (f : MeasureTheory.SimpleFunc α β),
  MeasureTheory.StronglyMeasurable ⇑f
-- Lean.Meta.Basic
Lean.Meta.FunInfo.mk.inj : ∀ {paramInfo : Array Lean.Meta.ParamInfo} {resultDeps : Array ℕ} {paramInfo_1 : Array Lean.Meta.ParamInfo}
  {resultDeps_1 : Array ℕ},
  { paramInfo := paramInfo, resultDeps := resultDeps } = { paramInfo := paramInfo_1, resultDeps := resultDeps_1 } →
    paramInfo = paramInfo_1 ∧ resultDeps = resultDeps_1
-- Mathlib.Algebra.Group.Submonoid.Basic
Submonoid.gi.eq_1 : ∀ (M : Type u_1) [inst : MulOneClass M],
  Submonoid.gi M = { choice := fun s x => Submonoid.closure s, gc := ⋯, le_l_u := ⋯, choice_eq := ⋯ }
-- Init.Data.Rat.Lemmas
Rat.ceil_eq_neg_floor_neg : ∀ (a : ℚ), a.ceil = -(-a).floor
-- Mathlib.Algebra.Category.MonCat.FilteredColimits
MonCat.FilteredColimits.M.mk_eq : ∀ {J : Type v} [inst : CategoryTheory.SmallCategory J] (F : CategoryTheory.Functor J MonCat)
  (x y : (j : J) × ↑(F.obj j)),
  (∃ k f g,
      (CategoryTheory.ConcreteCategory.hom (F.map f)) x.snd = (CategoryTheory.ConcreteCategory.hom (F.map g)) y.snd) →
    MonCat.FilteredColimits.M.mk F x = MonCat.FilteredColimits.M.mk F y
-- Init.Data.Vector.Lemmas
Vector.anyM_mk : ∀ {m : Type → Type u_1} {α : Type u_2} {n : ℕ} [inst : Monad m] {p : α → m Bool} {xs : Array α} (h : xs.size = n),
  Vector.anyM p (Vector.mk xs h) = Array.anyM p xs
-- Init.Data.Fin.Lemmas
Fin.forall_fin_one : ∀ {p : Fin 1 → Prop}, (∀ (i : Fin 1), p i) ↔ p 0
-- Mathlib.Algebra.Group.Pointwise.Finset.Basic
Finset.image_mul_left : ∀ {α : Type u_2} [inst : DecidableEq α] [inst_1 : Group α] {t : Finset α} {a : α},
  Finset.image (fun b => a * b) t = t.preimage (fun b => a⁻¹ * b) ⋯
-- Mathlib.LinearAlgebra.Matrix.Rank
/-- A special case of `lift_cRank_reindex` for when the row types are in the same universe.  -/
Matrix.cRank_reindex : ∀ {m : Type um} {n₀ : Type un₀} {R : Type uR} {m₀ : Type um} {n : Type un} [inst : Semiring R] (A : Matrix m n R)
  (em : m ≃ m₀) (en : n ≃ n₀), ((Matrix.reindex em en) A).cRank = A.cRank
-- Mathlib.AlgebraicTopology.ModelCategory.Cylinder
HomotopicalAlgebra.Cylinder.IsVeryGood.toIsGood : ∀ {C : Type u} {inst : CategoryTheory.Category.{v, u} C} {A : C}
  {inst_1 : HomotopicalAlgebra.CategoryWithWeakEquivalences C} {P : HomotopicalAlgebra.Cylinder A}
  {inst_2 : CategoryTheory.Limits.HasBinaryCoproduct A A} {inst_3 : HomotopicalAlgebra.CategoryWithCofibrations C}
  {inst_4 : HomotopicalAlgebra.CategoryWithFibrations C} [self : P.IsVeryGood], P.IsGood
-- Mathlib.AlgebraicGeometry.Birational.Birational
AlgebraicGeometry.Scheme.PartialIso.refl_source : ∀ (X : AlgebraicGeometry.Scheme), (AlgebraicGeometry.Scheme.PartialIso.refl X).source = ⊤
-- Std.Time.Format.Modifier
Std.Time.Year.extended.sizeOf_spec : ∀ (num : ℕ), sizeOf (Std.Time.Year.extended num) = 1 + sizeOf num
-- Mathlib.GroupTheory.FreeGroup.Reduce
FreeGroup.reduce_singleton : ∀ {α : Type u_1} [inst : DecidableEq α] (s : α × Bool), FreeGroup.reduce [s] = [s]
-- Init.Data.Float.Float
/-- Rounds to the nearest integer, rounding away from zero at half-way points.

This function does not reduce in the kernel. It is implemented in compiled code by the C function
`round`.
 -/
Float.round : Float → Float
-- Mathlib.Algebra.Module.CharacterModule
CharacterModule.instLinearMapClassIntAddCircleRatOfNat : ∀ (A : Type uA) [inst : AddCommGroup A], LinearMapClass (CharacterModule A) ℤ A (AddCircle 1)
-- Mathlib.Probability.Distributions.Gamma
ProbabilityTheory.gammaPDFReal.eq_1 : ∀ (a r x : ℝ),
  ProbabilityTheory.gammaPDFReal a r x = if 0 ≤ x then r ^ a / Real.Gamma a * x ^ (a - 1) * Real.exp (-(r * x)) else 0
-- Mathlib.CategoryTheory.Bicategory.Basic
CategoryTheory.Bicategory.rightUnitor_inv_naturality : ∀ {B : Type u} [inst : CategoryTheory.Bicategory B] {a b : B} {f g : a ⟶ b} (η : f ⟶ g),
  CategoryTheory.CategoryStruct.comp η (CategoryTheory.Bicategory.rightUnitor g).inv =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.rightUnitor f).inv
      (CategoryTheory.Bicategory.whiskerRight η (CategoryTheory.CategoryStruct.id b))
-- Mathlib.Algebra.Homology.HomotopyCategory.HomComplex
/-- The type of `n`-cocycles, as a subtype of `Cochain F G n`.  -/
CochainComplex.HomComplex.Cocycle : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    [inst_1 : CategoryTheory.Preadditive C] → CochainComplex C ℤ → CochainComplex C ℤ → ℤ → Type v
-- Mathlib.Order.Filter.CountablyGenerated
Filter.countable_biInf_eq_iInf_seq' : ∀ {α : Type u_1} {ι : Type u_4} [inst : CompleteLattice α] {B : Set ι},
  B.Countable → ∀ (f : ι → α) {i₀ : ι}, f i₀ = ⊤ → ∃ x, ⨅ t ∈ B, f t = ⨅ i, f (x i)
-- Mathlib.Algebra.Lie.Rank
LieModule.isRegular_iff_natTrailingDegree_charpoly_eq_rank : ∀ (R : Type u_1) {L : Type u_3} (M : Type u_4) [inst : CommRing R] [inst_1 : LieRing L] [inst_2 : LieAlgebra R L]
  [inst_3 : Module.Finite R L] [inst_4 : Module.Free R L] [inst_5 : AddCommGroup M] [inst_6 : Module R M]
  [inst_7 : LieRingModule L M] [inst_8 : LieModule R L M] [inst_9 : Module.Finite R M] [inst_10 : Module.Free R M]
  (x : L) [Nontrivial R],
  LieModule.IsRegular R M x ↔ (LinearMap.charpoly ((LieModule.toEnd R L M) x)).natTrailingDegree = LieModule.rank R L M
-- Mathlib.Topology.Homotopy.HomotopyGroup
HomotopyGroup.symmAt_indep : ∀ {N : Type u_1} {X : Type u_2} [inst : TopologicalSpace X] {x : X} [inst_1 : DecidableEq N] {i : N} (j : N)
  (f : ↑(GenLoop N X x)), ⟦GenLoop.symmAt i f⟧ = ⟦GenLoop.symmAt j f⟧
-- Mathlib.RingTheory.TensorProduct.Maps
Algebra.TensorProduct.uliftEquiv_symm_tmul : ∀ (R : Type u_4) (S : Type u_5) {A : Type u_6} {B : Type u_7} [inst : CommSemiring R] [inst_1 : CommSemiring S]
  [inst_2 : Algebra R S] [inst_3 : Semiring A] [inst_4 : Algebra R A] [inst_5 : Algebra S A]
  [inst_6 : IsScalarTower R S A] [inst_7 : Semiring B] [inst_8 : Algebra R B] (a : ULift.{u_8, u_6} A)
  (b : ULift.{u_9, u_7} B),
  (Algebra.TensorProduct.uliftEquiv R S A B).symm (a ⊗ₜ[ULift.{u_11, u_4} R] b) = { down := a.down ⊗ₜ[R] b.down }
-- Init.Data.String.Pattern.Basic
String.Slice.Pattern.ToForwardSearcher.DefaultForwardSearcher.iter : {ρ : Type} → (pat : ρ) → (s : String.Slice) → Std.Iter (String.Slice.Pattern.SearchStep s)
-- Mathlib.GroupTheory.Congruence.Basic
/-- If e : M →* N is surjective then (c.comap e).Quotient ≃* c.Quotient with c : Con N  -/
Con.comapQuotientEquivOfSurj : {M : Type u_1} →
  {N : Type u_2} →
    [inst : MulOneClass M] →
      [inst_1 : MulOneClass N] →
        (c : Con M) → (f : N →* M) → Function.Surjective ⇑f → (Con.comap ⇑f ⋯ c).Quotient ≃* c.Quotient
-- Mathlib.Combinatorics.Matroid.Minor.Delete
Matroid.delete_isRestriction : ∀ {α : Type u_1} (M : Matroid α) (D : Set α), (M.delete D).IsRestriction M
-- Mathlib.Combinatorics.Additive.ApproximateSubgroup
IsApproximateSubgroup.one_mem : ∀ {G : Type u_1} [inst : Group G] {K : ℝ} {A : Set G}, IsApproximateSubgroup K A → 1 ∈ A
-- Mathlib.Analysis.LocallyConvex.PointwiseConvergence
PointwiseConvergenceCLM.tendsto_nhds : ∀ {α : Type u_1} {𝕜₁ : Type u_3} {𝕜₂ : Type u_4} [inst : NormedField 𝕜₁] [inst_1 : NormedField 𝕜₂] {σ : 𝕜₁ →+* 𝕜₂}
  {E : Type u_7} {F : Type u_8} [inst_2 : AddCommGroup E] [inst_3 : TopologicalSpace E] [inst_4 : Module 𝕜₁ E]
  [inst_5 : NormedAddCommGroup F] [inst_6 : NormedSpace 𝕜₂ F] {f : Filter α} (u : α → E →SLₚₜ[σ] F) (y₀ : E →SLₚₜ[σ] F),
  Filter.Tendsto u f (nhds y₀) ↔ ∀ (x : E) (ε : ℝ), 0 < ε → ∀ᶠ (k : α) in f, ‖(u k) x - y₀ x‖ < ε
-- Mathlib.CategoryTheory.Triangulated.Basic
/-- Constructor for natural isomorphisms between functors to the
category of triangles.  -/
CategoryTheory.Pretriangulated.Triangle.functorIsoMk : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    [inst_1 : CategoryTheory.HasShift C ℤ] →
      {J : Type u_1} →
        [inst_2 : CategoryTheory.Category.{v_1, u_1} J] →
          (A B : CategoryTheory.Functor J (CategoryTheory.Pretriangulated.Triangle C)) →
            (iso₁ :
                A.comp CategoryTheory.Pretriangulated.Triangle.π₁ ≅ B.comp CategoryTheory.Pretriangulated.Triangle.π₁) →
              (iso₂ :
                  A.comp CategoryTheory.Pretriangulated.Triangle.π₂ ≅
                    B.comp CategoryTheory.Pretriangulated.Triangle.π₂) →
                (iso₃ :
                    A.comp CategoryTheory.Pretriangulated.Triangle.π₃ ≅
                      B.comp CategoryTheory.Pretriangulated.Triangle.π₃) →
                  CategoryTheory.CategoryStruct.comp (A.whiskerLeft CategoryTheory.Pretriangulated.Triangle.π₁Toπ₂)
                        iso₂.hom =
                      CategoryTheory.CategoryStruct.comp iso₁.hom
                        (B.whiskerLeft CategoryTheory.Pretriangulated.Triangle.π₁Toπ₂) →
                    CategoryTheory.CategoryStruct.comp (A.whiskerLeft CategoryTheory.Pretriangulated.Triangle.π₂Toπ₃)
                          iso₃.hom =
                        CategoryTheory.CategoryStruct.comp iso₂.hom
                          (B.whiskerLeft CategoryTheory.Pretriangulated.Triangle.π₂Toπ₃) →
                      CategoryTheory.CategoryStruct.comp (A.whiskerLeft CategoryTheory.Pretriangulated.Triangle.π₃Toπ₁)
                            (CategoryTheory.Functor.whiskerRight iso₁.hom (CategoryTheory.shiftFunctor C 1)) =
                          CategoryTheory.CategoryStruct.comp iso₃.hom
                            (B.whiskerLeft CategoryTheory.Pretriangulated.Triangle.π₃Toπ₁) →
                        (A ≅ B)
-- Init.Data.String.Lemmas.Pattern.Basic
String.Slice.Pattern.Model.IsLongestRevMatchAt.lt : ∀ {ρ : Type} {pat : ρ} [inst : String.Slice.Pattern.Model.PatternModel pat]
  [String.Slice.Pattern.Model.StrictPatternModel pat] {s : String.Slice} {startPos endPos : s.Pos},
  String.Slice.Pattern.Model.IsLongestRevMatchAt pat startPos endPos → startPos < endPos
-- Mathlib.Topology.Closure
interior_mono : ∀ {X : Type u} [inst : TopologicalSpace X] {s t : Set X}, s ⊆ t → interior s ⊆ interior t
-- Mathlib.Analysis.Complex.OpenMapping
Polynomial.C_eq_or_isOpenQuotientMap_eval : ∀ (p : Polynomial ℂ), (∃ x, Polynomial.C x = p) ∨ IsOpenQuotientMap fun x => Polynomial.eval x p
-- Mathlib.AlgebraicTopology.SimplicialSet.Skeleton
/-- the right morphism of the pushout square `isPushout i d`.  -/
SSet.relativeCellComplexOfMono.r : {X Y : SSet} → (i : X ⟶ Y) → (d : ℕ) → ((SSet.skeletonOfMono i) d).toSSet ⟶ ((SSet.skeletonOfMono i) (d + 1)).toSSet
-- Mathlib.AlgebraicGeometry.Fiber
AlgebraicGeometry.instJacobsonSpaceCarrierCarrierCommRingCatFiberOfLocallyOfFiniteType : ∀ {X Y : AlgebraicGeometry.Scheme} (f : X ⟶ Y) (y : ↥Y) [AlgebraicGeometry.LocallyOfFiniteType f],
  JacobsonSpace ↥(AlgebraicGeometry.Scheme.Hom.fiber f y)
-- Aesop.Script.SpecificTactics
Aesop.introsUnfoldingS : Lean.MVarId → Lean.Meta.TransparencyMode → Aesop.ScriptM (Lean.MVarId × Array Lean.FVarId)
-- Mathlib.Algebra.Group.Subgroup.Lattice
Subgroup.mem_sup' : ∀ {C : Type u_2} [inst : CommGroup C] {s t : Subgroup C} {x : C}, x ∈ s ⊔ t ↔ ∃ y z, ↑y * ↑z = x
-- Mathlib.CategoryTheory.Limits.HasLimits
/-- The colimits of `F : J ⥤ C` and `G : K ⥤ C` are isomorphic,
if there is an equivalence `e : J ≌ K` making the triangle commute up to natural isomorphism.
 -/
CategoryTheory.Limits.HasColimit.isoOfEquivalence : {J : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} J] →
    {K : Type u₂} →
      [inst_1 : CategoryTheory.Category.{v₂, u₂} K] →
        {C : Type u} →
          [inst_2 : CategoryTheory.Category.{v, u} C] →
            {F : CategoryTheory.Functor J C} →
              [inst_3 : CategoryTheory.Limits.HasColimit F] →
                {G : CategoryTheory.Functor K C} →
                  [inst_4 : CategoryTheory.Limits.HasColimit G] →
                    (e : J ≌ K) →
                      (e.functor.comp G ≅ F) → (CategoryTheory.Limits.colimit F ≅ CategoryTheory.Limits.colimit G)
-- Mathlib.MeasureTheory.Function.LpSpace.ContinuousFunctions
/-- The bounded linear map of considering a continuous function on a compact finite-measure
space `α` as an element of `Lp`.  By definition, the norm on `C(α, E)` is the sup-norm, transferred
from the space `α →ᵇ E` of bounded continuous functions, so this construction is just a matter of
transferring the structure from `BoundedContinuousFunction.toLp` along the isometry.  -/
ContinuousMap.toLp : {α : Type u_1} →
  {E : Type u_2} →
    {m0 : MeasurableSpace α} →
      (p : ENNReal) →
        (μ : MeasureTheory.Measure α) →
          [inst : TopologicalSpace α] →
            [BorelSpace α] →
              [inst_2 : NormedAddCommGroup E] →
                [SecondCountableTopologyEither α E] →
                  [CompactSpace α] →
                    [MeasureTheory.IsFiniteMeasure μ] →
                      (𝕜 : Type u_3) →
                        [inst_6 : Fact (1 ≤ p)] →
                          [inst_7 : NormedRing 𝕜] →
                            [inst_8 : Module 𝕜 E] →
                              [inst_9 : IsBoundedSMul 𝕜 E] → C(α, E) →L[𝕜] ↥(MeasureTheory.Lp E p μ)
-- Mathlib.NumberTheory.Padics.RingHoms
PadicInt.norm_sub_modPart : ∀ {p : ℕ} [hp_prime : Fact (Nat.Prime p)] (r : ℚ) (h : ‖↑r‖ ≤ 1), ‖⟨↑r, h⟩ - ↑(PadicInt.modPart p r)‖ < 1
-- Mathlib.RingTheory.Coalgebra.TensorProduct
_private.Mathlib.RingTheory.Coalgebra.TensorProduct.0.Coalgebra.termε : Lean.ParserDescr
-- Mathlib.Combinatorics.Configuration
Configuration.ofField.instProjectivePlaneProjectivizationForallFinOfNatNatOfDecidableEq : {K : Type u_3} →
  [inst : Field K] →
    [DecidableEq K] → Configuration.ProjectivePlane (Projectivization K (Fin 3 → K)) (Projectivization K (Fin 3 → K))
-- Mathlib.Order.Booleanisation
Booleanisation.comp_sup_comp : ∀ {α : Type u_1} [inst : GeneralizedBooleanAlgebra α] (a b : α),
  Booleanisation.comp a ⊔ Booleanisation.comp b = Booleanisation.comp (a ⊓ b)
-- Mathlib.Data.Nat.Choose.Basic
Nat.multichoose_two : ∀ (k : ℕ), Nat.multichoose 2 k = k + 1
-- Mathlib.GroupTheory.Coset.Basic
/-- The natural embedding `α ⧸ (⨅ i, f i) ↪ Π i, α ⧸ f i`.  -/
AddSubgroup.quotientiInfEmbedding : {α : Type u_1} → [inst : AddGroup α] → {ι : Type u_2} → (f : ι → AddSubgroup α) → α ⧸ ⨅ i, f i ↪ (i : ι) → α ⧸ f i
-- Init.Data.UInt.Bitwise
USize.ofBitVec_shiftRight : ∀ (a : BitVec System.Platform.numBits),
  ∀ b < System.Platform.numBits, { toBitVec := a >>> b } = { toBitVec := a } >>> USize.ofNat b
-- Mathlib.Analysis.Normed.Group.Basic
nndist_nnnorm_nnnorm_le_nnnorm_inv_mul : ∀ {E : Type u_5} [inst : SeminormedGroup E] (a b : E), nndist ‖a‖₊ ‖b‖₊ ≤ ‖a⁻¹ * b‖₊
-- Std.Data.ExtHashMap.Lemmas
Std.ExtHashMap.size_filterMap_eq_size_iff : ∀ {α : Type u} {β : Type v} {γ : Type w} {x : BEq α} {x_1 : Hashable α} {m : Std.ExtHashMap α β} [inst : EquivBEq α]
  [inst_1 : LawfulHashable α] {f : α → β → Option γ},
  (Std.ExtHashMap.filterMap f m).size = m.size ↔ ∀ (k : α) (h : k ∈ m), (f (m.getKey k h) m[k]).isSome = true
-- Mathlib.CategoryTheory.ObjectProperty.ColimitsOfShape
CategoryTheory.ObjectProperty.ColimitOfShape.toCostructuredArrow_map : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] {P : CategoryTheory.ObjectProperty C} {J : Type u'}
  [inst_1 : CategoryTheory.Category.{v', u'} J] {X : C} (p : P.ColimitOfShape J X) {X_1 Y : J} (f : X_1 ⟶ Y),
  p.toCostructuredArrow.map f =
    CategoryTheory.CostructuredArrow.homMk (CategoryTheory.ObjectProperty.homMk (p.diag.map f)) ⋯
-- Mathlib.RingTheory.Kaehler.JacobiZariski
/-- Given representations `0 → I → R[X] → S → 0` and `0 → K → S[Y] → T → 0`,
we may consider the induced representation `0 → J → R[X, Y] → T → 0`, and the sequence
`T ⊗[S] (I/I²) → J/J² → K/K²` is exact.
 -/
Algebra.Generators.Cotangent.exact : ∀ {R : Type u₁} {S : Type u₂} [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : Algebra R S] {T : Type u₃}
  [inst_3 : CommRing T] [inst_4 : Algebra R T] [inst_5 : Algebra S T] [inst_6 : IsScalarTower R S T] {ι : Type w₁}
  {σ : Type w₂} (Q : Algebra.Generators S T ι) (P : Algebra.Generators R S σ),
  Function.Exact ⇑(LinearMap.liftBaseChange T (Algebra.Extension.Cotangent.map (Q.toComp P).toExtensionHom))
    ⇑(Algebra.Extension.Cotangent.map (Q.ofComp P).toExtensionHom)
-- Mathlib.Algebra.Lie.Normalizer
LieSubmodule.normalizer_inf : ∀ {R : Type u_1} {L : Type u_2} {M : Type u_3} [inst : CommRing R] [inst_1 : LieRing L] [inst_2 : LieAlgebra R L]
  [inst_3 : AddCommGroup M] [inst_4 : Module R M] [inst_5 : LieRingModule L M] [inst_6 : LieModule R L M]
  {N₁ N₂ : LieSubmodule R L M}, (N₁ ⊓ N₂).normalizer = N₁.normalizer ⊓ N₂.normalizer
-- Mathlib.MeasureTheory.MeasurableSpace.Constructions
MeasurableSet.prod : ∀ {α : Type u_1} {β : Type u_2} {m : MeasurableSpace α} {mβ : MeasurableSpace β} {s : Set α} {t : Set β},
  MeasurableSet s → MeasurableSet t → MeasurableSet (s ×ˢ t)
-- Mathlib.CategoryTheory.Preadditive.Mat
CategoryTheory.Mat_.hom_ext_iff : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.Preadditive C]
  {M N : CategoryTheory.Mat_ C} {f g : M ⟶ N}, f = g ↔ ∀ (i : M.ι) (j : N.ι), f i j = g i j
-- Mathlib.Algebra.QuadraticAlgebra.Basic
/-- Conjugation in `QuadraticAlgebra R a b`.
The conjugate of `x + y ω` is `x + y ω' = (x + b * y) - y ω`.  -/
QuadraticAlgebra.instStar : {R : Type u_2} → {a b : R} → [CommRing R] → Star (QuadraticAlgebra R a b)
-- Lean.Data.Lsp.Extra
Lean.Lsp.LeanFileProgressParams.textDocument : Lean.Lsp.LeanFileProgressParams → Lean.Lsp.VersionedTextDocumentIdentifier
-- Mathlib.Algebra.Group.Subgroup.Defs
Subgroup.le_normalizer : ∀ {G : Type u_1} [inst : Group G] {H : Subgroup G}, H ≤ Subgroup.normalizer ↑H
-- Mathlib.Algebra.Homology.HomotopyCategory.HomComplex
CochainComplex.HomComplex.δ_zero_cochain_comp : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Preadditive C]
  {F G K : CochainComplex C ℤ} {n₂ : ℤ} (z₁ : CochainComplex.HomComplex.Cochain F G 0)
  (z₂ : CochainComplex.HomComplex.Cochain G K n₂) (m₂ : ℤ) (h₂ : n₂ + 1 = m₂),
  CochainComplex.HomComplex.δ n₂ m₂ (z₁.comp z₂ ⋯) =
    z₁.comp (CochainComplex.HomComplex.δ n₂ m₂ z₂) ⋯ + n₂.negOnePow • (CochainComplex.HomComplex.δ 0 1 z₁).comp z₂ ⋯
-- Mathlib.Data.Finsupp.Fin
Finsupp.cons_ne_zero_of_right : ∀ {n : ℕ} {M : Type u_1} [inst : Zero M] {y : M} {s : Fin n →₀ M}, s ≠ 0 → Finsupp.cons y s ≠ 0
-- Mathlib.Data.Finsupp.Basic
/-- Given `f : α → β`, `l : β →₀ M` and a proof `hf` that `f` is injective on
the preimage of `l.support`, `comapDomain f l hf` is the finitely supported function
from `α` to `M` given by composing `l` with `f`.  -/
Finsupp.comapDomain : {α : Type u_1} →
  {β : Type u_2} →
    {M : Type u_5} → [inst : Zero M] → (f : α → β) → (l : β →₀ M) → Set.InjOn f (f ⁻¹' ↑l.support) → α →₀ M
-- Mathlib.RingTheory.AlgebraicIndependent.Adjoin
/-- Canonical isomorphism between rational function field and the
intermediate field generated by algebraically independent elements.  -/
AlgebraicIndependent.aevalEquivField : {ι : Type u_1} →
  {F : Type u_2} →
    {E : Type u_3} →
      {x : ι → E} →
        [inst : Field F] →
          [inst_1 : Field E] →
            [inst_2 : Algebra F E] →
              AlgebraicIndependent F x →
                FractionRing (MvPolynomial ι F) ≃ₐ[F] ↥(IntermediateField.adjoin F (Set.range x))
-- Mathlib.Analysis.Complex.Trigonometric
Complex.cosh_add_sinh : ∀ (x : ℂ), Complex.cosh x + Complex.sinh x = Complex.exp x
-- Lean.Elab.Tactic.Induction
_private.Lean.Elab.Tactic.Induction.0.Lean.Elab.Tactic.getElimNameInfo : Lean.Syntax → Array Lean.Expr → Bool → Lean.Elab.Tactic.TacticM Lean.Meta.ElimInfo
-- Mathlib.CategoryTheory.Sites.Types
/-- Given a sheaf `S`, construct an equivalence `S(α) ≃ (α → S(*))`.  -/
CategoryTheory.evalEquiv : (S : CategoryTheory.Functor Type uᵒᵖ (Type u)) →
  CategoryTheory.Presheaf.IsSheaf CategoryTheory.typesGrothendieckTopology S →
    (α : Type u) → S.obj (Opposite.op α) ≃ (α ⟶ S.obj (Opposite.op PUnit.{u + 1}))
-- Mathlib.Order.Partition.Finpartition
/-- The sum of a set-valued function over a combined partition equals the sum of sums over component
partitions.  -/
Finpartition.sum_combine : ∀ {α : Type u_1} [inst : Lattice α] [inst_1 : OrderBot α] [inst_2 : IsModularLattice α] [inst_3 : DecidableEq α]
  {ι : Type u_2} {I : Finset ι} {s : ι → α} (P : (i : ι) → Finpartition (s i)) (ha : I.SupIndep s) {M : Type u_3}
  [inst_4 : AddCommMonoid M] (f : α → M), ∑ p ∈ (Finpartition.combine P ha).parts, f p = ∑ i ∈ I, ∑ p ∈ (P i).parts, f p
-- Std.Http.Data.URI.Encoding
Std.Http.URI.instHashableOptionEncodedQueryString : {r : UInt8 → Bool} → Hashable (Option (Std.Http.URI.EncodedQueryString r))
-- Mathlib.CategoryTheory.Generator.Basic
CategoryTheory.ObjectProperty.isGroupoid_of_isDetecting_bot : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C], ⊥.IsDetecting → CategoryTheory.IsGroupoid C
-- Mathlib.Order.Bounds.Basic
upperBounds_mono_mem : ∀ {α : Type u_1} [inst : Preorder α] {s : Set α} ⦃a b : α⦄, a ≤ b → a ∈ upperBounds s → b ∈ upperBounds s