mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Algebra.Group.Subgroup.Map
AddSubgroup.comap_inf : ∀ {G : Type u_1} [inst : AddGroup G] {N : Type u_5} [inst_1 : AddGroup N] (H K : AddSubgroup N) (f : G →+ N),
  AddSubgroup.comap f (H ⊓ K) = AddSubgroup.comap f H ⊓ AddSubgroup.comap f K
-- Mathlib.CategoryTheory.SmallObject.Iteration.ExtendToSucc
CategoryTheory.SmallObject.SuccStruct.extendToSucc.obj_succ_eq : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] {J : Type u} [inst_1 : LinearOrder J]
  [inst_2 : SuccOrder J] {j : J},
  ¬IsMax j →
    ∀ (F : CategoryTheory.Functor (↑(Set.Iic j)) C) (X : C),
      CategoryTheory.SmallObject.SuccStruct.extendToSucc.obj F X ⟨Order.succ j, ⋯⟩ = X
-- Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic
Complex.cos_sub_pi_div_two : ∀ (x : ℂ), Complex.cos (x - ↑Real.pi / 2) = Complex.sin x
-- Mathlib.GroupTheory.MonoidLocalization.Basic
AddSubmonoid.IsLocalizationMap.exists_of_eq : ∀ {M : Type u_1} [inst : AddCommMonoid M] {N : Type u_2} [inst_1 : AddCommMonoid N] {S : AddSubmonoid M} {f : M → N},
  S.IsLocalizationMap f → ∀ {x y : M}, f x = f y → ∃ c, ↑c + x = ↑c + y
-- Mathlib.Topology.Sets.VietorisTopology
/-- The Vietoris topology on the compact subsets of a topological space.  -/
TopologicalSpace.Compacts.topology : {α : Type u_1} → [inst : TopologicalSpace α] → TopologicalSpace (TopologicalSpace.Compacts α)
-- Mathlib.NumberTheory.NumberField.Discriminant.Basic
NumberField.hermiteTheorem.finite_of_discr_bdd_of_isComplex : ∀ (A : Type u_2) [inst : Field A] [inst_1 : CharZero A] (N : ℕ),
  {K | {w | w.IsComplex}.Nonempty ∧ |NumberField.discr ↥↑K| ≤ ↑N}.Finite
-- Mathlib.Order.OmegaCompletePartialOrder
/-- `ωScottContinuous f` asserts that `f` is both monotone and distributes over ωSup.  -/
OmegaCompletePartialOrder.ωScottContinuous_iff_monotone_map_ωSup : ∀ {α : Type u_2} {β : Type u_3} [inst : OmegaCompletePartialOrder α] [inst_1 : OmegaCompletePartialOrder β] {f : α → β},
  OmegaCompletePartialOrder.ωScottContinuous f ↔
    ∃ (hf : Monotone f),
      ∀ (c : OmegaCompletePartialOrder.Chain α),
        f (OmegaCompletePartialOrder.ωSup c) = OmegaCompletePartialOrder.ωSup (c.map { toFun := f, monotone' := hf })
-- Lean.Elab.MutualInductive
_private.Lean.Elab.MutualInductive.0.Lean.Elab.Command.FinalizeContext.mk.inj : ∀ {elabs : Array Lean.Elab.Command.InductiveElabStep2} {mctx : Lean.MetavarContext} {levelParams : List Lean.Name}
  {params : Array Lean.Expr} {lctx : Lean.LocalContext} {localInsts : Lean.LocalInstances}
  {replaceIndFVars : Lean.Expr → Lean.MetaM Lean.Expr} {elabs_1 : Array Lean.Elab.Command.InductiveElabStep2}
  {mctx_1 : Lean.MetavarContext} {levelParams_1 : List Lean.Name} {params_1 : Array Lean.Expr}
  {lctx_1 : Lean.LocalContext} {localInsts_1 : Lean.LocalInstances}
  {replaceIndFVars_1 : Lean.Expr → Lean.MetaM Lean.Expr},
  { elabs := elabs, mctx := mctx, levelParams := levelParams, params := params, lctx := lctx, localInsts := localInsts,
        replaceIndFVars := replaceIndFVars } =
      { elabs := elabs_1, mctx := mctx_1, levelParams := levelParams_1, params := params_1, lctx := lctx_1,
        localInsts := localInsts_1, replaceIndFVars := replaceIndFVars_1 } →
    elabs = elabs_1 ∧
      mctx = mctx_1 ∧
        levelParams = levelParams_1 ∧
          params = params_1 ∧ lctx = lctx_1 ∧ localInsts = localInsts_1 ∧ replaceIndFVars = replaceIndFVars_1
-- Mathlib.Data.Num.Bitwise
SNum.bit_zero : ∀ (b : Bool), SNum.bit b (SNum.zero b) = SNum.zero b
-- Init.Data.String.Basic
String.sliceFrom.eq_1 : ∀ (s : String) (p : s.Pos), s.sliceFrom p = s.toSlice.sliceFrom p.toSlice
-- Mathlib.CategoryTheory.Limits.Cones
/-- `mapCone` is the left inverse to `mapConeInv`.  -/
CategoryTheory.Functor.mapConeMapConeInv : {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 D} →
              (H : CategoryTheory.Functor D C) →
                [inst_3 : H.IsEquivalence] →
                  (c : CategoryTheory.Limits.Cone (F.comp H)) → H.mapCone (H.mapConeInv c) ≅ c
-- Mathlib.Algebra.Homology.ShortComplex.Preadditive
CategoryTheory.ShortComplex.Homotopy.compRight_h₃ : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Preadditive C]
  {S₁ S₂ S₃ : CategoryTheory.ShortComplex C} {φ₁ φ₂ : S₁ ⟶ S₂} (h : CategoryTheory.ShortComplex.Homotopy φ₁ φ₂)
  (ψ : S₂ ⟶ S₃), (h.compRight ψ).h₃ = CategoryTheory.CategoryStruct.comp h.h₃ ψ.τ₃
-- Mathlib.GroupTheory.Index
AddSubgroup.relIndex_comap : ∀ {G : Type u_1} {G' : Type u_2} [inst : AddGroup G] [inst_1 : AddGroup G'] (H : AddSubgroup G) (f : G' →+ G)
  (K : AddSubgroup G'), (AddSubgroup.comap f H).relIndex K = H.relIndex (AddSubgroup.map f K)
-- Mathlib.Data.List.Perm.Subperm
/-- **Alias** of the reverse direction of `List.subperm_cons`. -/
List.subperm.cons : ∀ {α : Type u_1} (a : α) {l₁ l₂ : List α}, l₁.Subperm l₂ → (a :: l₁).Subperm (a :: l₂)
-- Mathlib.Tactic.CategoryTheory.Bicategory.Normalize
Mathlib.Tactic.Bicategory.eval_of : ∀ {B : Type u} [inst : CategoryTheory.Bicategory B] {a b : B} {f g : a ⟶ b} (η : f ⟶ g),
  η =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.Iso.refl f).hom
      (CategoryTheory.CategoryStruct.comp η (CategoryTheory.Iso.refl g).hom)
-- Mathlib.Order.Filter.AtTopBot.Ring
Filter.tendsto_mul_self_atTop : ∀ {α : Type u_1} [inst : Semiring α] [inst_1 : PartialOrder α] [IsOrderedRing α],
  Filter.Tendsto (fun x => x * x) Filter.atTop Filter.atTop
-- Mathlib.AlgebraicGeometry.EllipticCurve.Weierstrass
WeierstrassCurve.twoTorsionPolynomial.eq_1 : ∀ {R : Type u} [inst : CommRing R] (W : WeierstrassCurve R),
  W.twoTorsionPolynomial = { a := 4, b := W.b₂, c := 2 * W.b₄, d := W.b₆ }
-- Mathlib.MeasureTheory.Measure.AEMeasurable
AEMeasurable.mono_ac : ∀ {α : Type u_2} {β : Type u_3} {m0 : MeasurableSpace α} [inst : MeasurableSpace β] {f : α → β}
  {μ ν : MeasureTheory.Measure α}, AEMeasurable f ν → μ.AbsolutelyContinuous ν → AEMeasurable f μ
-- Mathlib.Analysis.Calculus.LocalExtr.Basic
/-- If `f` has a local min on `s` at `a`, `f'` is the derivative of `f` at `a` within `s`, and
`y` belongs to the positive tangent cone of `s` at `a`, then `0 ≤ f' y`.  -/
IsLocalMinOn.hasFDerivWithinAt_nonneg : ∀ {E : Type u} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] {f : E → ℝ} {f' : StrongDual ℝ E} {s : Set E}
  {a y : E}, IsLocalMinOn f s a → HasFDerivWithinAt f f' s a → y ∈ posTangentConeAt s a → 0 ≤ f' y
-- Mathlib.NumberTheory.LSeries.Convergence
/-- If `f` is bounded, then the abscissa of absolute convergence of `f` is bounded above by `1`.  -/
LSeries.abscissaOfAbsConv_le_of_le_const : ∀ {f : ℕ → ℂ}, (∃ C, ∀ (n : ℕ), n ≠ 0 → ‖f n‖ ≤ C) → LSeries.abscissaOfAbsConv f ≤ 1
-- Mathlib.Analysis.Analytic.CPolynomialDef
/-- If a function admits a finite power series expansion on a disk, then it is continuous there.  -/
HasFiniteFPowerSeriesOnBall.continuousOn : ∀ {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [inst : NontriviallyNormedField 𝕜] [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F] {f : E → F}
  {p : FormalMultilinearSeries 𝕜 E F} {x : E} {r : ENNReal} {n : ℕ},
  HasFiniteFPowerSeriesOnBall f p x n r → ContinuousOn f (Metric.eball x r)
-- Mathlib.RingTheory.Ideal.Span
/-- The ideal generated by an arbitrary binary relation.  -/
Ideal.ofRel : {α : Type u} → [inst : Semiring α] → (α → α → Prop) → Ideal α
-- Std.Data.ExtDTreeMap.Lemmas
Std.ExtDTreeMap.getKey?_eq_some_getKeyD_of_contains : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t : Std.ExtDTreeMap α β cmp} [inst : Std.TransCmp cmp]
  {a fallback : α}, t.contains a = true → t.getKey? a = some (t.getKeyD a fallback)
-- Mathlib.Algebra.Group.Subgroup.ZPowers.Basic
Int.zmultiples_natAbs : ∀ (a : ℤ), AddSubgroup.zmultiples ↑a.natAbs = AddSubgroup.zmultiples a
-- Mathlib.RingTheory.MvPolynomial.WeightedHomogeneous
/-- 0 is weighted homogeneous of any degree.  -/
MvPolynomial.isWeightedHomogeneous_zero : ∀ (R : Type u_1) {M : Type u_2} [inst : CommSemiring R] {σ : Type u_3} [inst_1 : AddCommMonoid M] (w : σ → M) (m : M),
  MvPolynomial.IsWeightedHomogeneous w 0 m
-- Mathlib.InformationTheory.KullbackLeibler.KLFun
/-- `klFun` is continuous.  -/
InformationTheory.continuous_klFun : Continuous InformationTheory.klFun
-- Mathlib.Analysis.Calculus.BumpFunction.SmoothApprox
UniformContinuous.exists_contDiff_dist_le : ∀ {E : Type u_1} {F : Type u_2} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] [FiniteDimensional ℝ E]
  [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace ℝ F] [CompleteSpace F] {f : E → F} {ε : ℝ},
  UniformContinuous f → 0 < ε → ∃ g, ContDiff ℝ (↑⊤) g ∧ ∀ (a : E), dist (g a) (f a) < ε
-- Mathlib.CategoryTheory.Localization.HasLocalization
/-- the localization functor.  -/
CategoryTheory.MorphismProperty.HasLocalization.L : {C : Type u} →
  {inst : CategoryTheory.Category.{v, u} C} →
    {W : CategoryTheory.MorphismProperty C} →
      [self : W.HasLocalization] → CategoryTheory.Functor C (CategoryTheory.MorphismProperty.HasLocalization.D W)
-- Mathlib.RingTheory.Polynomial.Chebyshev
/-- ChebyshevT as a polynomial sequence.  -/
Polynomial.Chebyshev.chebyshevTsequence : (R : Type u_1) → [inst : CommRing R] → [IsDomain R] → [NeZero 2] → Polynomial.Sequence R
-- Mathlib.Topology.Order.Compact
CompactIccSpace.mk'' : ∀ {α : Type u_1} [inst : TopologicalSpace α] [inst_1 : PartialOrder α],
  (∀ {a b : α}, a < b → IsCompact (Set.Icc a b)) → CompactIccSpace α
-- Mathlib.RingTheory.Bialgebra.MonoidAlgebra
BialgEquiv.ofAlgEquiv.congr_simp : ∀ {R : Type u} {A : Type v} {B : Type w} [inst : CommSemiring R] [inst_1 : Semiring A] [inst_2 : Semiring B]
  [inst_3 : Bialgebra R A] [inst_4 : Bialgebra R B] (f f_1 : A ≃ₐ[R] B) (e_f : f = f_1)
  (counit_comp : (Bialgebra.counitAlgHom R B).comp ↑f = Bialgebra.counitAlgHom R A)
  (map_comp_comul :
    (Algebra.TensorProduct.map ↑f ↑f).comp (Bialgebra.comulAlgHom R A) = (Bialgebra.comulAlgHom R B).comp ↑f),
  BialgEquiv.ofAlgEquiv f counit_comp map_comp_comul = BialgEquiv.ofAlgEquiv f_1 ⋯ ⋯
-- Mathlib.Order.Hom.CompleteLattice
/-- Reinterpret an `⨅`-homomorphism as a `⨆`-homomorphism between the dual orders.  -/
sInfHom.dual : {α : Type u_2} → {β : Type u_3} → [inst : InfSet α] → [inst_1 : InfSet β] → sInfHom α β ≃ sSupHom αᵒᵈ βᵒᵈ
-- Aesop.Forward.Match
/-- Elaborate the term of a forward rule in the current goal.  -/
Aesop.elabForwardRuleTerm : Lean.MVarId → Aesop.RuleTerm → Lean.MetaM Lean.Expr
-- 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_17.splitter : (motive : (w : ℕ) → Std.Tactic.BVDecide.BVExpr w → Sort u_1) →
  (w : ℕ) →
    (expr : Std.Tactic.BVDecide.BVExpr w) →
      ((w a : ℕ) → motive w (Std.Tactic.BVDecide.BVExpr.var a)) →
        ((w : ℕ) → (val : BitVec w) → motive w (Std.Tactic.BVDecide.BVExpr.const val)) →
          ((w : ℕ) →
              (lhsExpr : Std.Tactic.BVDecide.BVExpr w) →
                (op : Std.Tactic.BVDecide.BVBinOp) →
                  (rhsExpr : Std.Tactic.BVDecide.BVExpr w) → motive w (lhsExpr.bin op rhsExpr)) →
            ((w : ℕ) →
                (op : Std.Tactic.BVDecide.BVUnOp) →
                  (expr : Std.Tactic.BVDecide.BVExpr w) → motive w (Std.Tactic.BVDecide.BVExpr.un op expr)) →
              ((w l r : ℕ) →
                  (lhs : Std.Tactic.BVDecide.BVExpr l) →
                    (rhs : Std.Tactic.BVDecide.BVExpr r) → (h : w = l + r) → motive w (lhs.append rhs h)) →
                ((w w_1 n : ℕ) →
                    (expr : Std.Tactic.BVDecide.BVExpr w_1) →
                      (h : w = w_1 * n) → motive w (Std.Tactic.BVDecide.BVExpr.replicate n expr h)) →
                  ((len w start : ℕ) →
                      (expr : Std.Tactic.BVDecide.BVExpr w) →
                        motive len (Std.Tactic.BVDecide.BVExpr.extract start len expr)) →
                    ((w n : ℕ) →
                        (lhs : Std.Tactic.BVDecide.BVExpr w) →
                          (rhs : Std.Tactic.BVDecide.BVExpr n) → motive w (lhs.shiftLeft rhs)) →
                      ((w n : ℕ) →
                          (lhs : Std.Tactic.BVDecide.BVExpr w) →
                            (rhs : Std.Tactic.BVDecide.BVExpr n) → motive w (lhs.shiftRight rhs)) →
                        ((w n : ℕ) →
                            (lhs : Std.Tactic.BVDecide.BVExpr w) →
                              (rhs : Std.Tactic.BVDecide.BVExpr n) → motive w (lhs.arithShiftRight rhs)) →
                          motive w expr
-- Lean.Declaration
Lean.instBEqDeclaration : BEq Lean.Declaration
-- Mathlib.CategoryTheory.WithTerminal.Basic
CategoryTheory.WithTerminal.opEquiv_unitIso_hom_app : ∀ (C : Type u) [inst : CategoryTheory.Category.{v, u} C] (X : (CategoryTheory.WithTerminal C)ᵒᵖ),
  (CategoryTheory.WithTerminal.opEquiv C).unitIso.hom.app X =
    (match Opposite.unop X with
      | CategoryTheory.WithTerminal.of x => CategoryTheory.Iso.refl (Opposite.op (CategoryTheory.WithTerminal.of x))
      | CategoryTheory.WithTerminal.star => CategoryTheory.Iso.refl (Opposite.op CategoryTheory.WithTerminal.star)).hom
-- Mathlib.Data.Seq.Basic
Stream'.Seq.append_nil : ∀ {α : Type u} (s : Stream'.Seq α), s.append Stream'.Seq.nil = s
-- Mathlib.MeasureTheory.MeasurableSpace.Embedding
MeasurableEquiv.refl_toEquiv : ∀ (α : Type u_6) [inst : MeasurableSpace α], (MeasurableEquiv.refl α).toEquiv = Equiv.refl α
-- Mathlib.Algebra.MvPolynomial.Basic
MvPolynomial.prod_X_pow : ∀ {R : Type u} {σ : Type u_1} [inst : CommSemiring R] (x : σ → ℕ) (t : Finset σ),
  ∏ y ∈ t, MvPolynomial.X y ^ x y = (MvPolynomial.monomial (Finsupp.indicator t fun i x_1 => x i)) 1
-- Init.Data.Fin.Lemmas
Fin.zero_le : ∀ {n : ℕ} [inst : NeZero n] (a : Fin n), 0 ≤ a
-- Mathlib.Algebra.Polynomial.Div
/-- See `divByMonic`.  -/
Polynomial.divModByMonicAux : {R : Type u} → [inst : Ring R] → Polynomial R → {q : Polynomial R} → q.Monic → Polynomial R × Polynomial R
-- Mathlib.CategoryTheory.Limits.Cones
/-- Cones on `F : J ⥤ Cᵒᵖ` are equivalent to cocones on `F.leftOp : Jᵒᵖ ⥤ C`.  -/
CategoryTheory.Limits.coconeLeftOpOfConeEquiv : {J : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} J] →
    {C : Type u₃} →
      [inst_1 : CategoryTheory.Category.{v₃, u₃} C] →
        {F : CategoryTheory.Functor J Cᵒᵖ} → (CategoryTheory.Limits.Cone F)ᵒᵖ ≌ CategoryTheory.Limits.Cocone F.leftOp
-- Mathlib.Algebra.Category.Grp.EnoughInjectives
AddCommGrpCat.enoughInjectives : CategoryTheory.EnoughInjectives AddCommGrpCat
-- Mathlib.Algebra.Group.Action.End
/-- The tautological action by `Equiv.Perm α` on `α`.

This generalizes `Function.End.applyMulAction`.  -/
Equiv.Perm.applyMulAction : (α : Type u_6) → MulAction (Equiv.Perm α) α
-- Mathlib.RingTheory.PowerSeries.WeierstrassPreparation
/-- If the ring is `I`-adic complete, then `g` can be used as a divisor in Weierstrass division.  -/
PowerSeries.IsWeierstrassDivisorAt.isWeierstrassDivisionAt_div_mod : ∀ {A : Type u_1} [inst : CommRing A] {g : PowerSeries A} {I : Ideal A} (H : g.IsWeierstrassDivisorAt I)
  (f : PowerSeries A) [inst_1 : IsAdicComplete I A], f.IsWeierstrassDivisionAt g (H.div f) (H.mod f) I
-- Mathlib.LinearAlgebra.Projectivization.PSL.PSL2
/-- `PSL ι F` is nontrivial whenever `ι` has at least two elements (and `F` is a field,
hence in particular nontrivial).  -/
SL2Simple.PSL_nontrivial : ∀ {ι : Type u_1} {F : Type u_2} [inst : Field F] [inst_1 : DecidableEq ι] [inst_2 : Fintype ι] [Nontrivial ι],
  Nontrivial (Matrix.ProjectiveSpecialLinearGroup ι F)
-- Mathlib.RingTheory.MvPowerSeries.LinearTopology
/-- If the ring `R` is endowed with a linear topology, then the sets `↑basis σ R (J, d)`,
for `J : TwoSidedIdeal R` which are neighborhoods of `0 : R` and `d : σ →₀ ℕ`,
constitute a basis of neighborhoods of `0 : MvPowerSeries σ R` for the product topology.  -/
MvPowerSeries.LinearTopology.hasBasis_nhds_zero : ∀ {σ : Type u_1} {R : Type u_2} [inst : Ring R] [inst_1 : TopologicalSpace R] [IsLinearTopology R R]
  [IsLinearTopology Rᵐᵒᵖ R],
  (nhds 0).HasBasis (fun Id => ↑Id.1 ∈ nhds 0) fun Id => ↑(MvPowerSeries.LinearTopology.basis σ R Id)
-- Mathlib.Order.ULift
ULift.down_sdiff : ∀ {α : Type u} [inst : SDiff α] (a b : ULift.{u_1, u} α), (a \ b).down = a.down \ b.down
-- Mathlib.SetTheory.Ordinal.FixedPointApproximants
OrdinalApprox.lfpApprox_mono_left : ∀ {α : Type u} [inst : CompleteLattice α], Monotone OrdinalApprox.lfpApprox
-- Mathlib.Algebra.Category.Semigrp.Basic
MagmaCat.Hom.ext_iff : ∀ {A B : MagmaCat} {x y : A.Hom B}, x = y ↔ x.hom' = y.hom'
-- Mathlib.Topology.MetricSpace.GromovHausdorff
GromovHausdorff.eq_toGHSpace_iff : ∀ {X : Type u} [inst : MetricSpace X] [inst_1 : CompactSpace X] [inst_2 : Nonempty X]
  {p : TopologicalSpace.NonemptyCompacts ↥(lp (fun n => ℝ) ⊤)},
  ⟦p⟧ = GromovHausdorff.toGHSpace X ↔ ∃ Ψ, Isometry Ψ ∧ Set.range Ψ = ↑p
-- Mathlib.RingTheory.Spectrum.Prime.ChevalleyComplexity
ChevalleyThm.MvPolynomialC.degBound_le_degBound : ∀ {k₁ k₂ : ℕ} {D₁ D₂ : ℕ → ℕ},
  k₁ ≤ k₂ →
    ∀ (n : ℕ),
      (∀ i < n, D₁ i ≤ D₂ i) → ChevalleyThm.MvPolynomialC.degBound k₁ D₁ n ≤ ChevalleyThm.MvPolynomialC.degBound k₂ D₂ n
-- Mathlib.RingTheory.Extension.Generators
Finsupp.sumFinsuppEquivProdFinsupp.eq_1 : ∀ {α : Type u_12} {β : Type u_13} {γ : Type u_14} [inst : Zero γ],
  Finsupp.sumFinsuppEquivProdFinsupp =
    { toFun := fun f => (Finsupp.comapDomain Sum.inl f ⋯, Finsupp.comapDomain Sum.inr f ⋯),
      invFun := fun fg => fg.1.sumElim fg.2, left_inv := ⋯, right_inv := ⋯ }
-- Mathlib.AlgebraicGeometry.Sites.Proetale
AlgebraicGeometry.Scheme.instIsStableUnderCompositionProetalePrecoverage : AlgebraicGeometry.Scheme.proetalePrecoverage.IsStableUnderComposition
-- Mathlib.CategoryTheory.Bicategory.Adjunction.Cat
CategoryTheory.Adjunction.ofCat_unit : ∀ {C D : CategoryTheory.Cat} {F : C ⟶ D} {G : D ⟶ C} (adj : CategoryTheory.Bicategory.Adjunction F G),
  (CategoryTheory.Adjunction.ofCat adj).unit = adj.unit.toNatTrans
-- Mathlib.Dynamics.PeriodicPts.Defs
Function.isPeriodicPt_minimalPeriod : ∀ {α : Type u_1} (f : α → α) (x : α), Function.IsPeriodicPt f (Function.minimalPeriod f x) x
-- Mathlib.Combinatorics.SimpleGraph.Clique
/-- The maximum number of vertices in a clique of a graph `G`.  -/
SimpleGraph.cliqueNum : {α : Type u_3} → SimpleGraph α → ℕ
-- Lean.Meta.Sym.DSimp.DSimpM
/-- Maximum number of steps that can be performed by the simplifier.  -/
Lean.Meta.Sym.DSimp.Config.maxSteps : Lean.Meta.Sym.DSimp.Config → ℕ
-- Init.Grind.Module.NatModuleNorm
Lean.Grind.Linarith.Poly.denoteN_mul' : ∀ {α : Type u_1} [inst : Lean.Grind.NatModule α] (ctx : Lean.Grind.Linarith.Context α) (p : Lean.Grind.Linarith.Poly)
  (k : ℕ),
  p.NonnegCoeffs → Lean.Grind.Linarith.Poly.denoteN ctx (p.mul' ↑k) = k • Lean.Grind.Linarith.Poly.denoteN ctx p
-- Mathlib.RingTheory.PowerSeries.Order
/-- The order of the monomial `a*X^n` is infinite if `a = 0` and `n` otherwise.  -/
PowerSeries.order_monomial : ∀ {R : Type u_1} [inst : Semiring R] (n : ℕ) (a : R) [inst_1 : Decidable (a = 0)],
  ((PowerSeries.monomial n) a).order = if a = 0 then ⊤ else ↑n
-- Mathlib.Order.CompleteBooleanAlgebra
Prod.instCompleteAtomicBooleanAlgebra : {α : Type u} →
  {β : Type v} →
    [CompleteAtomicBooleanAlgebra α] → [CompleteAtomicBooleanAlgebra β] → CompleteAtomicBooleanAlgebra (α × β)
-- Mathlib.SetTheory.Cardinal.NatCard
Set.Finite.ecard_strictMonoOn : ∀ {α : Type u_1}, StrictMonoOn (ENat.card ∘ Set.Elem) (Set.ofPred Set.Finite)
-- Mathlib.Geometry.Convex.Cone.Basic
/-- The **carrier set** underlying this cone: the set of points contained in it  -/
ConvexCone.carrier : {R : Type u_2} →
  {M : Type u_4} →
    [inst : Semiring R] →
      [inst_1 : PartialOrder R] → [inst_2 : AddCommMonoid M] → [inst_3 : SMul R M] → ConvexCone R M → Set M
-- Mathlib.Topology.DenseEmbedding
/-- ```
 γ -f→ α
g↓     ↓e
 δ -h→ β
```
 -/
IsDenseInducing.tendsto_comap_nhds_nhds : ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} {δ : Type u_4} [inst : TopologicalSpace α] [inst_1 : TopologicalSpace β]
  {i : α → β} [inst_2 : TopologicalSpace δ] {f : γ → α} {g : γ → δ} {h : δ → β} {d : δ} {a : α},
  IsDenseInducing i →
    Filter.Tendsto h (nhds d) (nhds (i a)) → h ∘ g = i ∘ f → Filter.Tendsto f (Filter.comap g (nhds d)) (nhds a)
-- Init.Data.SInt.Lemmas
Int64.lt_trans : ∀ {a b c : Int64}, a < b → b < c → a < c
-- Aesop.Forward.SlotIndex
Aesop.SlotIndex.mk.sizeOf_spec : ∀ (toNat : ℕ), sizeOf { toNat := toNat } = 1 + sizeOf toNat
-- Mathlib.RingTheory.IntegralClosure.Algebra.Basic
integralClosure.coe_smul : ∀ {G : Type u_1} {R : Type u_2} {K : Type u_3} [inst : CommRing R] [inst_1 : CommRing K] [inst_2 : Algebra R K]
  [inst_3 : Group G] [inst_4 : MulSemiringAction G K] [inst_5 : SMulCommClass G R K] (g : G)
  (k : ↥(integralClosure R K)), ↑(g • k) = g • ↑k
-- Mathlib.CategoryTheory.Bicategory.Basic
/-- Postcomposition of a 1-morphism as a functor.  -/
CategoryTheory.Bicategory.postcomp : {B : Type u} →
  [inst : CategoryTheory.Bicategory B] → {b c : B} → (a : B) → (b ⟶ c) → CategoryTheory.Functor (a ⟶ b) (a ⟶ c)
-- Std.Data.ExtDTreeMap.Lemmas
Std.ExtDTreeMap.maxKey?_eq_some_iff_getKey?_eq_self_and_forall : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t : Std.ExtDTreeMap α β cmp} [inst : Std.TransCmp cmp]
  {km : α}, t.maxKey? = some km ↔ t.getKey? km = some km ∧ ∀ k ∈ t, (cmp k km).isLE = true
-- Mathlib.AlgebraicTopology.SimplicialSet.HornColimits
/-- The morphism `Λ[3, 2] ⟶ X` which is obtained by gluing three
morphisms `Δ[2] ⟶ X`.  -/
SSet.horn₃₂.desc : {X : SSet} →
  (f₀ f₁ f₃ : SSet.stdSimplex.obj { len := 2 } ⟶ X) →
    CategoryTheory.CategoryStruct.comp (SSet.stdSimplex.δ 2) f₁ =
        CategoryTheory.CategoryStruct.comp (SSet.stdSimplex.δ 1) f₃ →
      CategoryTheory.CategoryStruct.comp (SSet.stdSimplex.δ 2) f₀ =
          CategoryTheory.CategoryStruct.comp (SSet.stdSimplex.δ 0) f₃ →
        CategoryTheory.CategoryStruct.comp (SSet.stdSimplex.δ 0) f₀ =
            CategoryTheory.CategoryStruct.comp (SSet.stdSimplex.δ 0) f₁ →
          ((SSet.horn 3 2).toSSet ⟶ X)
-- Mathlib.Topology.EMetricSpace.Defs
Metric.nhds_basis_closedEBall : ∀ {α : Type u} [inst : PseudoEMetricSpace α] {x : α}, (nhds x).HasBasis (fun ε => 0 < ε) (Metric.closedEBall x)
-- Mathlib.SetTheory.Ordinal.FixedPointApproximants
/-- There are distinct indices smaller than the successor of the domain's cardinality
yielding the same value  -/
OrdinalApprox.exists_lfpApprox_eq_lfpApprox : ∀ {α : Type u} [inst : CompleteLattice α] (f : α →o α) (x : α),
  ∃ a < (Order.succ (Cardinal.mk α)).ord,
    ∃ b < (Order.succ (Cardinal.mk α)).ord, a ≠ b ∧ OrdinalApprox.lfpApprox f x a = OrdinalApprox.lfpApprox f x b
-- Mathlib.LinearAlgebra.LinearIndependent.Basic
LinearIndependent.group_smul : ∀ {ι : Type u'} {R : Type u_2} {M : Type u_4} [inst : Semiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M]
  {G : Type u_6} [hG : Group G] [inst_3 : MulAction G R] [inst_4 : SMul G M] [IsScalarTower G R M] [SMulCommClass G R M]
  {v : ι → M}, LinearIndependent R v → ∀ (w : ι → G), LinearIndependent R (w • v)
-- Mathlib.Algebra.Group.Embedding
mulRightEmbedding_apply : ∀ {G : Type u_1} [inst : Mul G] [inst_1 : IsRightCancelMul G] (g h : G), (mulRightEmbedding g) h = h * g
-- Lean.DocString.Extension
Lean.ElabBlock.custom.injEq : ∀ (val val_1 : Dynamic), (Lean.ElabBlock.custom val = Lean.ElabBlock.custom val_1) = (val = val_1)
-- Mathlib.Analysis.Normed.Operator.NormedSpace
ContinuousLinearMap.norm_single_le_one : ∀ {ι : Type u_9} [inst : Fintype ι] [inst_1 : DecidableEq ι] (𝕜 : Type u_10) [inst_2 : NontriviallyNormedField 𝕜]
  (E : ι → Type u_11) [inst_3 : (i : ι) → SeminormedAddCommGroup (E i)] [inst_4 : (i : ι) → NormedSpace 𝕜 (E i)]
  (i : ι), ‖ContinuousLinearMap.single 𝕜 E i‖ ≤ 1
-- Mathlib.LinearAlgebra.TensorAlgebra.ToTensorPower
TensorAlgebra.toDirectSum.eq_1 : ∀ {R : Type u_1} {M : Type u_2} [inst : CommSemiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M],
  TensorAlgebra.toDirectSum =
    (TensorAlgebra.lift R)
      (DirectSum.lof R ℕ (fun n => TensorPower R n M) 1 ∘ₗ ↑(PiTensorProduct.subsingletonEquiv 0).symm)