mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.LinearAlgebra.GeneralLinearGroup.Basic
/-- An invertible linear map `f` determines an equivalence from `M` to itself.  -/
LinearMap.GeneralLinearGroup.toLinearEquiv : {R : Type u_1} →
  {M : Type u_2} →
    [inst : Semiring R] →
      [inst_1 : AddCommMonoid M] → [inst_2 : Module R M] → LinearMap.GeneralLinearGroup R M → M ≃ₗ[R] M
-- Lean.Elab.Do.Basic
/-- Inferred and cached information about the monad.  -/
Lean.Elab.Do.Context.monadInfo : Lean.Elab.Do.Context → Lean.Elab.Do.MonadInfo
-- Mathlib.Data.Fin.SuccPred
Fin.sub_castAdd_eq_castAdd_sub_of_le : ∀ {m n : ℕ} {a b : Fin n}, b ≤ a → Fin.castAdd m a - Fin.castAdd m b = Fin.castAdd m (a - b)
-- Mathlib.Algebra.Order.Group.Cone
instPartialOrderAddGroupCone.eq_1 : ∀ (G : Type u_1) [inst : AddCommGroup G], instPartialOrderAddGroupCone G = PartialOrder.ofSetLike (AddGroupCone G) G
-- Mathlib.AlgebraicTopology.SimplicialSet.AnodyneExtensions.RelativeCellComplex
SSet.Subcomplex.Pairing.RankFunction.Cell.subcomplex_not_le_filtration : ∀ {X : SSet} {A : X.Subcomplex} {P : A.Pairing} {ι : Type v} [inst : LinearOrder ι] {f : P.RankFunction ι} {j : ι}
  (c : f.Cell j), ¬(↑c.s).subcomplex ≤ f.filtration j
-- Mathlib.Order.Interval.Basic
Interval.coe_inj : ∀ {α : Type u_1} [inst : LE α] {s t : NonemptyInterval α}, ↑s = ↑t ↔ s = t
-- Mathlib.LinearAlgebra.Matrix.Charpoly.Coeff
Matrix.charpoly_fin_two : ∀ {R : Type u} [inst : CommRing R] [Nontrivial R] (M : Matrix (Fin 2) (Fin 2) R),
  M.charpoly = Polynomial.X ^ 2 - Polynomial.C M.trace * Polynomial.X + Polynomial.C M.det
-- Mathlib.Analysis.SpecialFunctions.Exp
Real.image_exp_Ioo : ∀ (a b : ℝ), Real.exp '' Set.Ioo a b = Set.Ioo (Real.exp a) (Real.exp b)
-- Mathlib.LinearAlgebra.Matrix.ConjTranspose
Matrix.conjTranspose_submatrix : ∀ {l : Type u_1} {m : Type u_2} {n : Type u_3} {o : Type u_4} {α : Type v} [inst : Star α] (A : Matrix m n α)
  (r : l → m) (c : o → n), (A.submatrix r c).conjTranspose = A.conjTranspose.submatrix c r
-- Mathlib.Order.Lex
ofColex_toColex : ∀ {α : Type u_1} (a : α), ofColex (toColex a) = a
-- Mathlib.Topology.Algebra.InfiniteSum.NatInt
Multipliable.prod_mul_tprod_nat_add : ∀ {G : Type u_2} [inst : CommGroup G] [inst_1 : TopologicalSpace G] [IsTopologicalGroup G] [T2Space G] {f : ℕ → G}
  (k : ℕ), Multipliable f → (∏ i ∈ Finset.range k, f i) * ∏' (i : ℕ), f (i + k) = ∏' (i : ℕ), f i
-- Mathlib.CategoryTheory.Comma.StructuredArrow.Basic
CategoryTheory.CostructuredArrow.Hom.w_assoc : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  {S : CategoryTheory.Functor C D} {T : D} {X Y : CategoryTheory.CostructuredArrow S T} (f : X ⟶ Y) {Z : D} (h : T ⟶ Z),
  CategoryTheory.CategoryStruct.comp (S.map f.left) (CategoryTheory.CategoryStruct.comp Y.hom h) =
    CategoryTheory.CategoryStruct.comp X.hom h
-- Mathlib.Order.Heyting.Basic
/-- `p → true`  -/
himp_top : ∀ {α : Type u_2} [inst : GeneralizedHeytingAlgebra α] {a : α}, a ⇨ ⊤ = ⊤
-- Mathlib.Order.ConditionallyCompleteLattice.Basic
csInf_Ioi : ∀ {α : Type u_1} [inst : ConditionallyCompleteLattice α] {a : α} [NoMaxOrder α] [DenselyOrdered α], sInf (Set.Ioi a) = a
-- Mathlib.Order.Lattice
Pi.instSemilatticeInf.eq_1 : ∀ {ι : Type u_1} {α' : ι → Type u_2} [inst : (i : ι) → SemilatticeInf (α' i)],
  Pi.instSemilatticeInf =
    { toPartialOrder := Pi.partialOrder, inf := fun x y i => x i ⊓ y i, inf_le_left := ⋯, inf_le_right := ⋯,
      le_inf := ⋯ }
-- Mathlib.RepresentationTheory.Rep.Basic
/-- When `H = {1}`, the `G`-representation on `k[H]` induced by an action of `G` on `H` is
isomorphic to the trivial representation on `k`.  -/
Rep.ofMulActionSubsingletonIsoTrivial : (k : Type u) →
  (G : Type v) →
    [inst : Ring k] →
      [inst_1 : Monoid G] →
        (H : Type u) →
          [Subsingleton H] → [MulOneClass H] → [inst_4 : MulAction G H] → Rep.ofMulAction k G H ≅ Rep.trivial k G k
-- Mathlib.Data.Finset.Grade
/-- Finsets form an order-connected suborder of multisets.  -/
Finset.ordConnected_range_val : ∀ {α : Type u_1}, (Set.range Finset.val).OrdConnected
-- Lean.PrettyPrinter.Delaborator.TopDownAnalyze
Lean.PrettyPrinter.Delaborator.TopDownAnalyze.App.Context.f : Lean.PrettyPrinter.Delaborator.TopDownAnalyze.App.Context → Lean.Expr
-- Init.Data.Array.Range
Array.range_eq_range' : ∀ {n : ℕ}, Array.range n = Array.range' 0 n
-- Init.Data.Array.Count
Array.countP_reverse : ∀ {α : Type u_1} {p : α → Bool} {xs : Array α}, Array.countP p xs.reverse = Array.countP p xs
-- Mathlib.CategoryTheory.Subobject.Classifier.Defs
CategoryTheory.SubobjectRepresentableBy.χ.eq_1 : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Limits.HasPullbacks C] {Ω : C}
  (h : CategoryTheory.SubobjectRepresentableBy Ω) {U X : C} (m : U ⟶ X) [inst_2 : CategoryTheory.Mono m],
  h.χ m = h.homEquiv.symm (CategoryTheory.Subobject.mk m)
-- Mathlib.Algebra.Algebra.Equiv
AlgEquiv.equivCongr_symm : ∀ {R : Type uR} {A₁ : Type uA₁} {A₂ : Type uA₂} {A₁' : Type uA₁'} {A₂' : Type uA₂'} [inst : CommSemiring R]
  [inst_1 : Semiring A₁] [inst_2 : Semiring A₂] [inst_3 : Semiring A₁'] [inst_4 : Semiring A₂'] [inst_5 : Algebra R A₁]
  [inst_6 : Algebra R A₂] [inst_7 : Algebra R A₁'] [inst_8 : Algebra R A₂'] (e : A₁ ≃ₐ[R] A₂) (e' : A₁' ≃ₐ[R] A₂'),
  (e.equivCongr e').symm = e.symm.equivCongr e'.symm
-- Mathlib.CategoryTheory.Limits.Shapes.ZeroMorphisms
CategoryTheory.Limits.HasZeroMorphisms.instSubsingleton : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C], Subsingleton (CategoryTheory.Limits.HasZeroMorphisms C)
-- Mathlib.CategoryTheory.MorphismProperty.TransfiniteComposition
CategoryTheory.MorphismProperty.transfiniteCompositionsOfShape_le_transfiniteCompositions : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] (W : CategoryTheory.MorphismProperty C) (J : Type w)
  [inst_1 : LinearOrder J] [inst_2 : SuccOrder J] [inst_3 : OrderBot J] [inst_4 : WellFoundedLT J],
  W.transfiniteCompositionsOfShape J ≤ CategoryTheory.MorphismProperty.transfiniteCompositions.{w, v, u} W
-- Mathlib.FieldTheory.Relrank
Subfield.relrank_mul_relrank_eq_inf_relrank : ∀ {E : Type v} [inst : Field E] (A : Subfield E) {B C : Subfield E},
  B ≤ C → A.relrank B * B.relrank C = (A ⊓ B).relrank C
-- Mathlib.Analysis.Calculus.ImplicitContDiff
IsContDiffImplicitAt.ne_zero : ∀ {𝕜 : Type u_1} [inst : RCLike 𝕜] {E₁ : Type u_2} [inst_1 : NormedAddCommGroup E₁] [inst_2 : NormedSpace 𝕜 E₁]
  {E₂ : Type u_3} [inst_3 : NormedAddCommGroup E₂] [inst_4 : NormedSpace 𝕜 E₂] {F : Type u_4}
  [inst_5 : NormedAddCommGroup F] [inst_6 : NormedSpace 𝕜 F] {n : WithTop ℕ∞} {f : E₁ × E₂ → F} {f' : E₁ × E₂ →L[𝕜] F}
  {u : E₁ × E₂}, IsContDiffImplicitAt n f f' u → n ≠ 0
-- Mathlib.Data.Finset.Lattice.Lemmas
Finset.insert_inter_of_notMem : ∀ {α : Type u_1} [inst : DecidableEq α] {s₁ s₂ : Finset α} {a : α}, a ∉ s₂ → insert a s₁ ∩ s₂ = s₁ ∩ s₂
-- Mathlib.RingTheory.HahnSeries.Summable
HahnSeries.SummableFamily.pow_finite_co_support : ∀ {Γ : Type u_1} {R : Type u_3} [inst : AddCommMonoid Γ] [inst_1 : LinearOrder Γ] [inst_2 : IsOrderedCancelAddMonoid Γ]
  [inst_3 : CommRing R] {x : HahnSeries Γ R}, 0 < x.orderTop → ∀ (g : Γ), {a | ((fun n => x ^ n) a).coeff g ≠ 0}.Finite
-- Mathlib.Order.GaloisConnection.Defs
GaloisConnection.l_unique : ∀ {α : Type u} {β : Type v} [inst : PartialOrder α] [inst_1 : Preorder β] {u : α → β} {l : β → α},
  GaloisConnection l u →
    ∀ {u' : α → β} {l' : β → α}, GaloisConnection l' u' → (∀ (a : α), u a = u' a) → ∀ {b : β}, l b = l' b
-- Init.Data.Ord.Basic
Ordering.isLE_gt : Ordering.gt.isLE = false
-- Std.Async.Signal
/-- Quit program.
 -/
Std.Async.Signal.sigquit : Std.Async.Signal
-- Mathlib.GroupTheory.Congruence.Defs
AddCon.toSetoid_bot : ∀ {M : Type u_1} [inst : Add M], ⊥.toSetoid = ⊥
-- Mathlib.CategoryTheory.Limits.Shapes.Pullback.Iso
/-- If `f : X ⟶ Z` is iso, then `Y ⨿[X] Z ≅ Y`. This is the explicit colimit cocone.  -/
CategoryTheory.Limits.pushoutCoconeOfRightIso : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    {X Y Z : C} → (f : X ⟶ Y) → (g : X ⟶ Z) → [CategoryTheory.IsIso g] → CategoryTheory.Limits.PushoutCocone f g
-- Mathlib.CategoryTheory.Triangulated.TStructure.ETrunc
CategoryTheory.Triangulated.TStructure.eTruncLTGEIsoGELT_hom_app_fac'_assoc : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Preadditive C]
  [inst_2 : CategoryTheory.Limits.HasZeroObject C] [inst_3 : CategoryTheory.HasShift C ℤ]
  [inst_4 : ∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive] [inst_5 : CategoryTheory.Pretriangulated C]
  (t : CategoryTheory.Triangulated.TStructure C) [inst_6 : CategoryTheory.IsTriangulated C] (a b : EInt) (X : C) {Z : C}
  (h : (t.eTruncGE.obj a).obj X ⟶ Z),
  CategoryTheory.CategoryStruct.comp ((t.eTruncLTGEIsoGELT a b).hom.app X)
      (CategoryTheory.CategoryStruct.comp ((t.eTruncGE.obj a).map ((t.eTruncLTι b).app X)) h) =
    CategoryTheory.CategoryStruct.comp ((t.eTruncLTι b).app ((t.eTruncGE.obj a).obj X)) h
-- Mathlib.MeasureTheory.Function.StronglyMeasurable.AEStronglyMeasurable
MeasureTheory.AEFinStronglyMeasurable.mul : ∀ {α : Type u_1} {β : Type u_2} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} [inst : TopologicalSpace β]
  {f g : α → β} [inst_1 : MulZeroClass β] [ContinuousMul β],
  MeasureTheory.AEFinStronglyMeasurable f μ →
    MeasureTheory.AEFinStronglyMeasurable g μ → MeasureTheory.AEFinStronglyMeasurable (f * g) μ
-- Mathlib.Data.PNat.Factors
/-- The gcd and lcm operations on positive integers correspond
to the inf and sup operations on multisets.  -/
PNat.factorMultiset_gcd : ∀ (m n : ℕ+), (m.gcd n).factorMultiset = m.factorMultiset ⊓ n.factorMultiset
-- Mathlib.Algebra.Group.End
AddAut.addConj_apply : ∀ {G : Type u_3} [inst : AddGroup G] (g h : G), (AddAut.addConj g) h = g + h + -g
-- Mathlib.Algebra.Group.Subgroup.Finite
Subgroup.card_le_card_group : ∀ {G : Type u_1} [inst : Group G] (H : Subgroup G) [Finite G], Nat.card ↥H ≤ Nat.card G
-- Mathlib.Algebra.Category.Ring.Limits
/-- The category of commutative rings has all limits.  -/
CommRingCat.hasLimitsOfSize : ∀ [UnivLE.{v, u}], CategoryTheory.Limits.HasLimitsOfSize.{w, v, u, u + 1} CommRingCat
-- Lean.Parser.Extra
Lean.Parser.manyIndent.formatter : Lean.PrettyPrinter.Formatter → Lean.PrettyPrinter.Formatter
-- Lean.Meta.MatchUtil
Lean.Meta.matchHEq? : Lean.Expr → Lean.MetaM (Option (Lean.Expr × Lean.Expr × Lean.Expr × Lean.Expr))
-- Mathlib.MeasureTheory.Function.AEEqFun
MeasureTheory.AEEqFun.le_inf : ∀ {α : Type u_1} {β : Type u_2} [inst : MeasurableSpace α] {μ : MeasureTheory.Measure α} [inst_1 : TopologicalSpace β]
  [inst_2 : SemilatticeInf β] [inst_3 : ContinuousInf β] (f' f g : α →ₘ[μ] β), f' ≤ f → f' ≤ g → f' ≤ f ⊓ g
-- Init.Data.Int.Order
Int.add_lt_add_of_lt_of_le : ∀ {a b c d : ℤ}, a < b → c ≤ d → a + c < b + d
-- Init.Data.UInt.Lemmas
UInt8.toUInt32_ofFin : ∀ {n : Fin UInt8.size}, (UInt8.ofFin n).toUInt32 = UInt32.ofNatLT ↑n ⋯
-- Std.Tactic.BVDecide.Normalize.BitVec
Std.Tactic.BVDecide.Normalize.Int16.toBitVec_ite : ∀ {c : Prop} {t e : Int16} [inst : Decidable c], (if c then t else e).toBitVec = if c then t.toBitVec else e.toBitVec
-- Mathlib.Analysis.MeanInequalities
/-- **Minkowski inequality**: the `L_p` seminorm of the infinite sum of two vectors is less than or
equal to the infinite sum of the `L_p`-seminorms of the summands, if these infinite sums both
exist. A version for `ℝ`-valued functions. For an alternative version, convenient if the infinite
sums are already expressed as `p`-th powers, see `Lp_add_le_hasSum_of_nonneg`.  -/
Real.Lp_add_le_tsum_of_nonneg : ∀ {ι : Type u} {f g : ι → ℝ} {p : ℝ},
  1 ≤ p →
    (∀ (i : ι), 0 ≤ f i) →
      (∀ (i : ι), 0 ≤ g i) →
        (Summable fun i => f i ^ p) →
          (Summable fun i => g i ^ p) →
            (Summable fun i => (f i + g i) ^ p) ∧
              (∑' (i : ι), (f i + g i) ^ p) ^ (1 / p) ≤
                (∑' (i : ι), f i ^ p) ^ (1 / p) + (∑' (i : ι), g i ^ p) ^ (1 / p)
-- Std.Data.HashSet.Lemmas
Std.HashSet.size_le_size_insertMany_list : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} {m : Std.HashSet α} [EquivBEq α] [LawfulHashable α] {l : List α},
  m.size ≤ (m.insertMany l).size
-- Mathlib.Data.Finset.Empty
/-- The empty finset  -/
Finset.empty : {α : Type u_1} → Finset α
-- Mathlib.Topology.ContinuousMap.Algebra
ContinuousMap.instCommMonoidWithZeroOfContinuousMul : {α : Type u_1} →
  {β : Type u_2} →
    [inst : TopologicalSpace α] →
      [inst_1 : TopologicalSpace β] → [inst_2 : CommMonoidWithZero β] → [ContinuousMul β] → CommMonoidWithZero C(α, β)
-- Mathlib.Topology.Algebra.Group.Matrix
Topology.IsInducing.generalLinearGroup_map : ∀ {n : Type u_1} {R : Type u_2} {S : Type u_3} [inst : Fintype n] [inst_1 : DecidableEq n] [inst_2 : CommRing R]
  [inst_3 : TopologicalSpace R] [inst_4 : CommRing S] [inst_5 : TopologicalSpace S] {f : R →+* S},
  Topology.IsInducing ⇑f → Topology.IsInducing ⇑(Matrix.GeneralLinearGroup.map f)
-- Lean.Widget.InteractiveDiagnostic
/-- A piece of Lean code with elaboration/typing data.
Note: does not necessarily correspond to an `Expr`, the name is for RPC API compatibility.  -/
Lean.Widget.MsgEmbed.expr : Lean.Widget.CodeWithInfos → Lean.Widget.MsgEmbed
-- Mathlib.Algebra.Group.Submonoid.Membership
Submonoid.closure_singleton_eq : ∀ {M : Type u_1} [inst : Monoid M] (x : M), Submonoid.closure {x} = MonoidHom.mrange ((powersHom M) x)
-- Mathlib.Topology.MetricSpace.Pseudo.Defs
Metric.eball_top : ∀ {α : Type u} [inst : PseudoMetricSpace α] (x : α), Metric.eball x ⊤ = Set.univ
-- Mathlib.Algebra.Homology.ShortComplex.Basic
CategoryTheory.ShortComplex.unopFunctor_obj : ∀ (C : Type u_1) [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  (S : CategoryTheory.ShortComplex Cᵒᵖ), (CategoryTheory.ShortComplex.unopFunctor C).obj S = Opposite.op S.unop
-- Mathlib.CategoryTheory.Sites.Descent.DescentDataPrime
CategoryTheory.Pseudofunctor.DescentData'.pullHom'.congr_simp : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C]
  {F : CategoryTheory.Pseudofunctor (CategoryTheory.LocallyDiscrete Cᵒᵖ) CategoryTheory.Cat} {ι : Type t} {S : C}
  {X : ι → C} {f : (i : ι) → X i ⟶ S} {sq : (i j : ι) → CategoryTheory.Limits.ChosenPullback (f i) (f j)}
  {obj obj' : (i : ι) → ↑(F.obj { as := Opposite.op (X i) })}
  (hom hom_1 :
    (i j : ι) →
      (F.map (sq i j).p₁.op.toLoc).toFunctor.obj (obj i) ⟶ (F.map (sq i j).p₂.op.toLoc).toFunctor.obj (obj' j)),
  hom = hom_1 →
    ∀ ⦃Y : C⦄ (q q_1 : Y ⟶ S) (e_q : q = q_1) ⦃i₁ i₂ : ι⦄ (f₁ : Y ⟶ X i₁) (f₂ : Y ⟶ X i₂)
      (hf₁ : CategoryTheory.CategoryStruct.comp f₁ (f i₁) = q) (hf₂ : CategoryTheory.CategoryStruct.comp f₂ (f i₂) = q),
      CategoryTheory.Pseudofunctor.DescentData'.pullHom' hom q f₁ f₂ hf₁ hf₂ =
        CategoryTheory.Pseudofunctor.DescentData'.pullHom' hom_1 q_1 f₁ f₂ ⋯ ⋯
-- Init.Omega.LinearCombo
Lean.Omega.LinearCombo.neg_eval : ∀ (lc : Lean.Omega.LinearCombo) (v : Lean.Omega.Coeffs), (-lc).eval v = -lc.eval v
-- Mathlib.Algebra.MvPolynomial.Degrees
MvPolynomial.degreeOf_rename_of_injective : ∀ {R : Type u} {σ : Type u_1} {τ : Type u_2} [inst : CommSemiring R] {p : MvPolynomial σ R} {f : σ → τ},
  Function.Injective f → ∀ (i : σ), MvPolynomial.degreeOf (f i) ((MvPolynomial.rename f) p) = MvPolynomial.degreeOf i p
-- Mathlib.CategoryTheory.Idempotents.FunctorCategories
CategoryTheory.Idempotents.app_p_comm : ∀ {J : Type u_1} {C : Type u_2} [inst : CategoryTheory.Category.{v_1, u_1} J]
  [inst_1 : CategoryTheory.Category.{v_2, u_2} C]
  {P Q : CategoryTheory.Idempotents.Karoubi (CategoryTheory.Functor J C)} (f : P ⟶ Q) (X : J),
  CategoryTheory.CategoryStruct.comp (P.p.app X) (f.f.app X) =
    CategoryTheory.CategoryStruct.comp (f.f.app X) (Q.p.app X)
-- Mathlib.MeasureTheory.Integral.IntervalIntegral.TrapezoidalRule
/-- The absolute error of trapezoidal integration.  -/
trapezoidal_error : (ℝ → ℝ) → ℕ → ℝ → ℝ → ℝ
-- Mathlib.Order.PiLex
Pi.Lex.lt_iff_of_unique : ∀ {ι : Type u_1} {β : ι → Type u_2} [inst : Unique ι] [inst_1 : (i : ι) → LT (β i)] [inst_2 : Preorder ι]
  {x y : Lex ((i : ι) → β i)}, x < y ↔ x default < y default