mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Algebra.MonoidAlgebra.Support
MonoidAlgebra.support_coeff_one : ∀ {k : Type u₁} {G : Type u₂} [inst : Semiring k] [inst_1 : One G] [NeZero 1], (MonoidAlgebra.coeff 1).support = 1
-- Init.Data.Nat.Basic
Nat.succ_lt_of_lt_pred : ∀ {n : ℕ} {m : ℕ}, n < m.pred → n.succ < m
-- Mathlib.CategoryTheory.Monoidal.Category
CategoryTheory.MonoidalCategory.id_whiskerLeft_symm_assoc : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.MonoidalCategory C] {X X' : C}
  (f : X ⟶ X') {Z : C} (h : X' ⟶ Z),
  CategoryTheory.CategoryStruct.comp f h =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.leftUnitor X).inv
      (CategoryTheory.CategoryStruct.comp
        (CategoryTheory.MonoidalCategoryStruct.whiskerLeft (CategoryTheory.MonoidalCategoryStruct.tensorUnit C) f)
        (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.leftUnitor X').hom h))
-- Mathlib.Algebra.Order.Group.Pointwise.Interval
Set.image_affine_Ioc : ∀ {K : Type u_2} [inst : DivisionSemiring K] [inst_1 : PartialOrder K] [PosMulReflectLT K] [IsOrderedCancelAddMonoid K]
  [ExistsAddOfLE K] {a : K},
  0 < a → ∀ (b c d : K), (fun x => a * x + b) '' Set.Ioc c d = Set.Ioc (a * c + b) (a * d + b)
-- Mathlib.MeasureTheory.Integral.Lebesgue.Map
MeasureTheory.lintegral_subtype_comap : ∀ {α : Type u_1} [inst : MeasurableSpace α] {μ : MeasureTheory.Measure α} {s : Set α},
  MeasurableSet s →
    ∀ (f : α → ENNReal), ∫⁻ (x : ↑s), f ↑x ∂MeasureTheory.Measure.comap Subtype.val μ = ∫⁻ (x : α) in s, f x ∂μ
-- Std.Data.Internal.List.Associative
_private.Std.Data.Internal.List.Associative.0.List.getLast?.match_1.eq_2 : ∀ {α : Type u_1} (motive : List α → Sort u_2) (a : α) (as : List α) (h_1 : Unit → motive [])
  (h_2 : (a : α) → (as : List α) → motive (a :: as)),
  (match a :: as with
    | [] => h_1 ()
    | a :: as => h_2 a as) =
    h_2 a as
-- Init.Prelude
HMod.mk : {α : Type u} → {β : Type v} → {γ : outParam (Type w)} → (α → β → γ) → HMod α β γ
-- Std.Data.HashMap.Basic
/-- Transforms the hash map into an array of mappings in some order.  -/
Std.HashMap.toArray : {α : Type u} → {β : Type v} → {x : BEq α} → {x_1 : Hashable α} → Std.HashMap α β → Array (α × β)
-- Mathlib.AlgebraicGeometry.Sites.Fpqc
AlgebraicGeometry.Scheme.instHasIsosFpqcPrecoverage : AlgebraicGeometry.Scheme.fpqcPrecoverage.HasIsos
-- Mathlib.Algebra.EuclideanDomain.Basic
EuclideanDomain.mul_div_assoc : ∀ {R : Type u} [inst : EuclideanDomain R] (x : R) {y z : R}, z ∣ y → x * y / z = x * (y / z)
-- Mathlib.Topology.Instances.ENNReal.Lemmas
ENNReal.continuous_ofReal : Continuous ENNReal.ofReal
-- Mathlib.Tactic.ClickSuggestions.GRewrite
/-- The lemma  -/
Mathlib.Tactic.ClickSuggestions.GrwLemma.name : Mathlib.Tactic.ClickSuggestions.GrwLemma → Mathlib.Tactic.ClickSuggestions.Premise
-- Mathlib.Tactic.CategoryTheory.Monoidal.Normalize
Mathlib.Tactic.Monoidal.evalWhiskerRight_cons_of_of : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.MonoidalCategory C] {f g h i j : C}
  {α : f ≅ g} {η : g ⟶ h} {ηs : h ⟶ i}
  {ηs₁ : CategoryTheory.MonoidalCategoryStruct.tensorObj h j ⟶ CategoryTheory.MonoidalCategoryStruct.tensorObj i j}
  {η₁ : CategoryTheory.MonoidalCategoryStruct.tensorObj g j ⟶ CategoryTheory.MonoidalCategoryStruct.tensorObj h j}
  {η₂ : CategoryTheory.MonoidalCategoryStruct.tensorObj g j ⟶ CategoryTheory.MonoidalCategoryStruct.tensorObj i j}
  {η₃ : CategoryTheory.MonoidalCategoryStruct.tensorObj f j ⟶ CategoryTheory.MonoidalCategoryStruct.tensorObj i j},
  CategoryTheory.MonoidalCategoryStruct.whiskerRight ηs j = ηs₁ →
    CategoryTheory.MonoidalCategoryStruct.whiskerRight η j = η₁ →
      CategoryTheory.CategoryStruct.comp η₁ ηs₁ = η₂ →
        CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.whiskerRightIso α j).hom η₂ = η₃ →
          CategoryTheory.MonoidalCategoryStruct.whiskerRight
              (CategoryTheory.CategoryStruct.comp α.hom (CategoryTheory.CategoryStruct.comp η ηs)) j =
            η₃
-- Mathlib.CategoryTheory.Adjunction.Limits
CategoryTheory.Functor.instPreservesColimitsOfShapeOfIsLeftAdjoint : ∀ {J : Type u_1} {C : Type u_2} {D : Type u_3} [inst : CategoryTheory.Category.{v_1, u_1} J]
  [inst_1 : CategoryTheory.Category.{v_2, u_2} C] [inst_2 : CategoryTheory.Category.{v_3, u_3} D]
  (F : CategoryTheory.Functor C D) [F.IsLeftAdjoint], CategoryTheory.Limits.PreservesColimitsOfShape J F
-- Init.Data.Int.DivMod.Basic
_private.Init.Data.Int.DivMod.Basic.0.Int.fdiv.match_1.eq_3 : ∀ (motive : ℤ → ℤ → Sort u_1) (m n : ℕ) (h_1 : (x : ℤ) → motive 0 x)
  (h_2 : (m n : ℕ) → motive (Int.ofNat m) (Int.ofNat n)) (h_3 : (m n : ℕ) → motive (Int.ofNat m.succ) (Int.negSucc n))
  (h_4 : (a : ℕ) → motive (Int.negSucc a) 0) (h_5 : (m n : ℕ) → motive (Int.negSucc m) (Int.ofNat n.succ))
  (h_6 : (m n : ℕ) → motive (Int.negSucc m) (Int.negSucc n)),
  (match Int.ofNat m.succ, Int.negSucc n with
    | 0, x => h_1 x
    | Int.ofNat m, Int.ofNat n => h_2 m n
    | Int.ofNat m.succ, Int.negSucc n => h_3 m n
    | Int.negSucc a, 0 => h_4 a
    | Int.negSucc m, Int.ofNat n.succ => h_5 m n
    | Int.negSucc m, Int.negSucc n => h_6 m n) =
    h_3 m n
-- Mathlib.CategoryTheory.Sums.Associator
CategoryTheory.sum.inverseAssociator_obj_inr_inr : ∀ (C : Type u₁) [inst : CategoryTheory.Category.{v₁, u₁} C] (D : Type u₂) [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  (E : Type u₃) [inst_2 : CategoryTheory.Category.{v₃, u₃} E] (X : E),
  (CategoryTheory.sum.inverseAssociator C D E).obj (Sum.inr (Sum.inr X)) = Sum.inr X
-- Lean.Server.CodeActions.Basic
Lean.Server.CodeActionResolveData.mk : Lean.Lsp.CodeActionParams → Lean.Name → ℕ → Lean.Server.CodeActionResolveData
-- Mathlib.Tactic.NormNum.Result
Mathlib.Meta.NormNum.Result'.isNNRat.injEq : ∀ (inst : Lean.Expr) (q : ℚ) (n d proof inst_1 : Lean.Expr) (q_1 : ℚ) (n_1 d_1 proof_1 : Lean.Expr),
  (Mathlib.Meta.NormNum.Result'.isNNRat inst q n d proof =
      Mathlib.Meta.NormNum.Result'.isNNRat inst_1 q_1 n_1 d_1 proof_1) =
    (inst = inst_1 ∧ q = q_1 ∧ n = n_1 ∧ d = d_1 ∧ proof = proof_1)
-- Std.Data.DTreeMap.Internal.Model
_private.Std.Data.DTreeMap.Internal.Model.0.Std.DTreeMap.Internal.Impl.applyPartition.go.match_1.splitter : (motive : Ordering → Sort u_1) →
  (x : Ordering) →
    (x = Ordering.lt → motive Ordering.lt) →
      (x = Ordering.eq → motive Ordering.eq) → (x = Ordering.gt → motive Ordering.gt) → motive x
-- Mathlib.GroupTheory.GroupAction.MultipleTransitivity
/-- The `alternatingGroup` on `α` is `(Nat.card α - 2)`-pretransitive.  -/
alternatingGroup.isMultiplyPretransitive : ∀ (α : Type u_1) [inst : Fintype α] [inst_1 : DecidableEq α],
  MulAction.IsMultiplyPretransitive (↥(alternatingGroup α)) α (Nat.card α - 2)
-- Mathlib.CategoryTheory.Adjunction.Triple
/-- For an adjoint triple `F ⊣ G ⊣ H` where `G` is fully faithful, whiskering the natural
transformation `H ⟶ F` with `G` yields the composition of the counit of the second adjunction with
the unit of the first adjunction.  -/
CategoryTheory.Adjunction.Triple.whiskerRight_rightToLeft : ∀ {C : Type u_1} {D : Type u_2} [inst : CategoryTheory.Category.{v_1, u_1} C]
  [inst_1 : CategoryTheory.Category.{v_2, u_2} D] {F : CategoryTheory.Functor C D} {G : CategoryTheory.Functor D C}
  {H : CategoryTheory.Functor C D} (t : CategoryTheory.Adjunction.Triple F G H) [inst_2 : G.Full] [inst_3 : G.Faithful],
  CategoryTheory.Functor.whiskerRight t.rightToLeft G = CategoryTheory.CategoryStruct.comp t.adj₂.counit t.adj₁.unit
-- Mathlib.Analysis.Normed.Group.Defs
/-- Construct a normed group from a translation-invariant pseudodistance.  -/
NormedAddCommGroup.ofAddDist' : {E : Type u_5} →
  [inst : Norm E] →
    [inst_1 : AddCommGroup E] →
      [inst_2 : MetricSpace E] →
        (∀ (x : E), ‖x‖ = dist 0 x) → (∀ (x y z : E), dist (z + x) (z + y) ≤ dist x y) → NormedAddCommGroup E
-- Mathlib.Analysis.SpecialFunctions.Trigonometric.DerivHyp
Real.sinh_eq_zero : ∀ {x : ℝ}, Real.sinh x = 0 ↔ x = 0
-- Mathlib.CategoryTheory.Monoidal.Functor
CategoryTheory.Equivalence.instMonoidalInverseTrans : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    [inst_1 : CategoryTheory.MonoidalCategory C] →
      {D : Type u₂} →
        [inst_2 : CategoryTheory.Category.{v₂, u₂} D] →
          [inst_3 : CategoryTheory.MonoidalCategory D] →
            {E : Type u₃} →
              [inst_4 : CategoryTheory.Category.{v₃, u₃} E] →
                [inst_5 : CategoryTheory.MonoidalCategory E] →
                  (e : C ≌ D) →
                    [e.inverse.Monoidal] → (e' : D ≌ E) → [e'.inverse.Monoidal] → (e.trans e').inverse.Monoidal
-- Mathlib.RingTheory.PowerSeries.Substitution
/-- **Alias** of `PowerSeries.rescale_eq`. -/
MvPowerSeries.rescaleUnit : ∀ {R : Type u_2} [inst : CommRing R] (r : R) (f : PowerSeries R),
  (PowerSeries.rescale r) f = (MvPowerSeries.rescale fun x => r) f
-- Mathlib.Analysis.SpecificLimits.Basic
/-- If `dist (f n) (f (n+1))` is bounded by `(C / 2) / 2^n`, then the distance from
`f 0` to the limit of `f` is bounded above by `C`.  -/
dist_le_of_le_geometric_two_of_tendsto₀ : ∀ {α : Type u_1} [inst : PseudoMetricSpace α] {C : ℝ} {f : ℕ → α},
  (∀ (n : ℕ), dist (f n) (f (n + 1)) ≤ C / 2 / 2 ^ n) →
    ∀ {a : α}, Filter.Tendsto f Filter.atTop (nhds a) → dist (f 0) a ≤ C
-- Mathlib.Analysis.SpecialFunctions.Trigonometric.Angle
Real.Angle.sin_coe : ∀ (x : ℝ), (↑x).sin = Real.sin x
-- Mathlib.GroupTheory.Coprod.Basic
Monoid.Coprod.mrange_lift : ∀ {M : Type u_1} {N : Type u_2} {P : Type u_3} [inst : MulOneClass M] [inst_1 : MulOneClass N] [inst_2 : Monoid P]
  (f : M →* P) (g : N →* P), MonoidHom.mrange (Monoid.Coprod.lift f g) = MonoidHom.mrange f ⊔ MonoidHom.mrange g
-- Mathlib.Analysis.Calculus.FDeriv.Mul
/-- Eta-expanded form of `Differentiable.mul` -/
Differentiable.fun_mul : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {𝔸 : Type u_5} [inst_3 : NormedRing 𝔸] [inst_4 : NormedAlgebra 𝕜 𝔸] {a b : E → 𝔸},
  Differentiable 𝕜 a → Differentiable 𝕜 b → Differentiable 𝕜 fun i => a i * b i
-- Mathlib.Data.TypeVec
TypeVec.dropFun_from_append1_drop_last : ∀ {n : ℕ} {α : TypeVec.{u_1} (n + 1)}, TypeVec.dropFun TypeVec.fromAppend1DropLast = TypeVec.id
-- Lean.Elab.Match
/-- Given the `stx` of a single match alternative, return a corresponding `TermMatchAltView`.  -/
Lean.Elab.Term.getMatchAlt : (k : Lean.SyntaxNodeKinds) → Lean.Syntax → Option (Lean.Elab.Term.MatchAltView k)
-- Mathlib.Topology.Algebra.Ring.Real
instIsUniformAddGroupReal : IsUniformAddGroup ℝ
-- Std.Data.TreeSet.Raw.Lemmas
Std.TreeSet.Raw.min?_eq_some_iff_mem_and_forall : ∀ {α : Type u} {cmp : α → α → Ordering} {t : Std.TreeSet.Raw α cmp} [Std.TransCmp cmp] [Std.LawfulEqCmp cmp],
  t.WF → ∀ {km : α}, t.min? = some km ↔ km ∈ t ∧ ∀ k ∈ t, (cmp km k).isLE = true
-- Mathlib.Topology.Algebra.InfiniteSum.Order
/-- **Alias** of the reverse direction of `summable_abs_iff`. -/
Summable.abs : ∀ {ι : Type u_1} {α : Type u_3} [inst : AddCommGroup α] [inst_1 : LinearOrder α] [IsOrderedAddMonoid α]
  [inst_3 : UniformSpace α] [IsUniformAddGroup α] [CompleteSpace α] {f : ι → α}, Summable f → Summable fun x => |f x|
-- Lean.Meta.Tactic.Grind.Types
Lean.Meta.Grind.EvalTactic : Type
-- Mathlib.CategoryTheory.Adjunction.PartialAdjoint
/-- Given `F : D ⥤ C`, this is the canonical bijection
`(F.partialLeftAdjointObj X ⟶ Y) ≃ (X.obj ⟶ F.obj Y)`
for all `X : F.PartialLeftAdjointSource` and `Y : D`.  -/
CategoryTheory.Functor.partialLeftAdjointHomEquiv : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    {D : Type u₂} →
      [inst_1 : CategoryTheory.Category.{v₂, u₂} D] →
        (F : CategoryTheory.Functor D C) →
          {X : F.PartialLeftAdjointSource} → {Y : D} → (F.partialLeftAdjointObj X ⟶ Y) ≃ (X.obj ⟶ F.obj Y)
-- Mathlib.CategoryTheory.Galois.Basic
/-- Arbitrarily choose a fiber functor for a Galois category using choice.  -/
CategoryTheory.PreGaloisCategory.GaloisCategory.getFiberFunctor : (C : Type u₁) →
  [inst : CategoryTheory.Category.{u₂, u₁} C] → [CategoryTheory.GaloisCategory C] → CategoryTheory.Functor C FintypeCat
-- Mathlib.Data.Set.Prod
Set.prod_insert : ∀ {α : Type u_1} {β : Type u_2} {s : Set α} {t : Set β} {b : β}, s ×ˢ insert b t = (fun a => (a, b)) '' s ∪ s ×ˢ t
-- Mathlib.Topology.Perfect
/-- A set `C` is called perfect if it is closed and all of its
points are accumulation points of itself.
Note that we do not require `C` to be nonempty.  -/
Perfect : {α : Type u_1} → [TopologicalSpace α] → Set α → Prop
-- Mathlib.RepresentationTheory.Homological.GroupHomology.Functoriality
groupHomology.chainsMap_f_single : ∀ {k G H : Type u} [inst : CommRing k] [inst_1 : Group G] [inst_2 : Group H] {A : Rep.{u, u, u} k G}
  {B : Rep.{u, u, u} k H} (f : G →* H) (φ : A ⟶ Rep.res f B) (n : ℕ) (x : Fin n → G) (a : ↑A),
  ((CategoryTheory.ConcreteCategory.hom ((groupHomology.chainsMap f φ).f n)) fun₀ | x => a) =
    fun₀ | ⇑f ∘ x => (Rep.Hom.hom φ) a
-- Mathlib.Data.Finset.Image
Finset.image_comm : ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} [inst : DecidableEq β] {s : Finset α} {β' : Type u_4}
  [inst_1 : DecidableEq β'] [inst_2 : DecidableEq γ] {f : β → γ} {g : α → β} {f' : α → β'} {g' : β' → γ},
  (∀ (a : α), f (g a) = g' (f' a)) → Finset.image f (Finset.image g s) = Finset.image g' (Finset.image f' s)
-- Batteries.Data.Array.Pairwise
Array.pairwise_singleton : ∀ {α : Type u_1} (R : α → α → Prop) (a : α), Array.Pairwise R #[a]
-- Std.Tactic.BVDecide.Bitblast.BVExpr.Circuit.Impl.Operations.Add
Std.Tactic.BVDecide.BVExpr.bitblast.blastAdd.go_le_size : ∀ {α : Type} [inst : Hashable α] [inst_1 : DecidableEq α] {w : ℕ} (aig : Std.Sat.AIG α) (curr : ℕ) (hcurr : curr ≤ w)
  (cin : aig.Ref) (s : aig.RefVec curr) (lhs rhs : aig.RefVec w),
  aig.decls.size ≤ (Std.Tactic.BVDecide.BVExpr.bitblast.blastAdd.go aig lhs rhs curr hcurr cin s).aig.decls.size
-- Mathlib.CategoryTheory.Limits.Shapes.Pullback.Categorical.Basic
/-- the first component element  -/
CategoryTheory.Limits.CategoricalPullback.fst : {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} → CategoryTheory.Limits.CategoricalPullback F G → A
-- Mathlib.Order.Booleanisation
Booleanisation.lift_sdiff_lift : ∀ {α : Type u_1} [inst : GeneralizedBooleanAlgebra α] (a b : α),
  Booleanisation.lift a \ Booleanisation.lift b = Booleanisation.lift (a \ b)
-- Mathlib.Analysis.Distribution.ContDiffMapSupportedIn
ContDiffMapSupportedIn.tsupport_subset : ∀ {E : Type u_2} {F : Type u_3} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] [inst_2 : NormedAddCommGroup F]
  [inst_3 : NormedSpace ℝ F] {n : ℕ∞} {K : TopologicalSpace.Compacts E} (f : ContDiffMapSupportedIn E F n K),
  tsupport ⇑f ⊆ ↑K
-- Mathlib.Algebra.MonoidAlgebra.Module
AddMonoidAlgebra.coeffLinearEquiv.eq_1 : ∀ (R : Type u_1) {S : Type u_2} {M : Type u_3} [inst : Semiring R] [inst_1 : Semiring S] [inst_2 : Module R S],
  AddMonoidAlgebra.coeffLinearEquiv R = Equiv.linearEquiv R AddMonoidAlgebra.coeffEquiv
-- Mathlib.LinearAlgebra.Projectivization.Independence
Projectivization.Independent.mk : ∀ {ι : Type u_1} {K : Type u_2} {V : Type u_3} [inst : DivisionRing K] [inst_1 : AddCommGroup V] [inst_2 : Module K V]
  (f : ι → V) (hf : ∀ (i : ι), f i ≠ 0),
  LinearIndependent K f → Projectivization.Independent fun i => Projectivization.mk K (f i) ⋯
-- Mathlib.Topology.Algebra.ConstMulAction
Filter.Tendsto.const_smul_zero : ∀ {M : Type u_1} {α : Type u_2} {β : Type u_3} [inst : TopologicalSpace α] [inst_1 : Zero α]
  [inst_2 : SMulZeroClass M α] [ContinuousConstSMul M α] {g : β → α} {l : Filter β} (c : M),
  Filter.Tendsto g l (nhds 0) → Filter.Tendsto (fun x => c • g x) l (nhds 0)
-- Std.Data.DTreeMap.Lemmas
Std.DTreeMap.Const.get!_insertMany_list_of_mem : ∀ {α : Type u} {cmp : α → α → Ordering} {β : Type v} {t : Std.DTreeMap α (fun x => β) cmp} [Std.TransCmp cmp]
  [inst : Inhabited β] {l : List (α × β)} {k k' : α},
  cmp k k' = Ordering.eq →
    ∀ {v : β},
      List.Pairwise (fun a b => ¬cmp a.1 b.1 = Ordering.eq) l →
        (k, v) ∈ l → Std.DTreeMap.Const.get! (Std.DTreeMap.Const.insertMany t l) k' = v
-- Mathlib.CategoryTheory.Triangulated.TStructure.TruncLTGE
CategoryTheory.Triangulated.TStructure.natTransTruncLTOfLE_refl : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} 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) (a : ℤ),
  t.natTransTruncLTOfLE a a ⋯ = CategoryTheory.CategoryStruct.id (t.truncLT a)
-- Mathlib.Algebra.Order.Floor.Defs
/-- `FloorRing.ceil` is the lower adjoint of the coercion `↑ : ℤ → α`.  -/
FloorRing.gc_ceil_coe : ∀ {α : Type u_4} {inst : Ring α} {inst_1 : LinearOrder α} [self : FloorRing α], GaloisConnection FloorRing.ceil Int.cast
-- Mathlib.Analysis.SpecialFunctions.Complex.Arg
Complex.arg_conj_coe_angle : ∀ (x : ℂ), ↑((starRingEnd ℂ) x).arg = -↑x.arg
-- Mathlib.Analysis.InnerProductSpace.Basic
inner_self_eq_one_of_norm_eq_one : ∀ {𝕜 : Type u_1} {E : Type u_2} [inst : RCLike 𝕜] [inst_1 : NormedAddCommGroup E] [inst_2 : InnerProductSpace 𝕜 E]
  {x : E}, ‖x‖ = 1 → inner 𝕜 x x = 1
-- Init.Data.List.Impl
List.eraseIdx_eq_eraseIdxTR : @List.eraseIdx = @List.eraseIdxTR
-- Init.Grind.Ring.CommSolver
Lean.Grind.CommRing.Expr.sub.sizeOf_spec : ∀ (a b : Lean.Grind.CommRing.Expr), sizeOf (a.sub b) = 1 + sizeOf a + sizeOf b
-- Mathlib.AlgebraicTopology.EilenbergSteenrod
TopPair.HomologyPretheory.comp_homₚ : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  {ι : Type u_2} {c : ComplexShape ι} {X Y Z : TopPair.HomologyPretheory C c} (f : X.Hom Y) (g : Y.Hom Z) (x : ι),
  (CategoryTheory.CategoryStruct.comp f g).homₚ x = CategoryTheory.CategoryStruct.comp (f.homₚ x) (g.homₚ x)
-- Mathlib.Probability.Moments.Basic
ProbabilityTheory.centralMoment.eq_1 : ∀ {Ω : Type u_1} {m : MeasurableSpace Ω} (X : Ω → ℝ) (p : ℕ) (μ : MeasureTheory.Measure Ω),
  ProbabilityTheory.centralMoment X p μ = ∫ (x : Ω), ((X - fun x => ∫ (x : Ω), X x ∂μ) ^ p) x ∂μ
-- Batteries.Data.Fin.Coding
/-- Encode `{ i : Fin n // P i }` into `Fin (Fin.countP P)` where `P` is a decidable predicate.  -/
Fin.encodeSubtype : {n : ℕ} → (P : Fin n → Prop) → [inst : DecidablePred P] → { i // P i } → Fin (Fin.countP fun x => decide (P x))
-- Mathlib.NumberTheory.NumberField.InfinitePlace.Ramification
NumberField.InfinitePlace.IsUnramified.liesOver_isReal_over : ∀ {K : Type u_4} {L : Type u_5} [inst : Field K] [inst_1 : Field L] [inst_2 : Algebra K L]
  (w : NumberField.InfinitePlace L) (v : NumberField.InfinitePlace K) [w.LiesOver v],
  NumberField.InfinitePlace.IsUnramified K w → v.IsReal → w.IsReal
-- Mathlib.Analysis.InnerProductSpace.PiL2
EuclideanSpace.edist_single_same : ∀ {ι : Type u_1} {𝕜 : Type u_3} [inst : RCLike 𝕜] [inst_1 : DecidableEq ι] [inst_2 : Fintype ι] (i : ι) (a b : 𝕜),
  edist (EuclideanSpace.single i a) (EuclideanSpace.single i b) = edist a b
-- Lean.Data.Json.Basic
Lean.JsonNumber.instNeg : Neg Lean.JsonNumber
-- Mathlib.LinearAlgebra.Finsupp.LinearCombination
Finsupp.span_image_eq_map_linearCombination : ∀ {α : Type u_1} {M : Type u_2} (R : Type u_5) [inst : Semiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M]
  {v : α → M} (s : Set α),
  Submodule.span R (v '' s) = Submodule.map (Finsupp.linearCombination R v) (Finsupp.supported R R s)
-- Mathlib.GroupTheory.Congruence.Defs
/-- The map sending a binary relation to the smallest congruence relation in which it is
contained is idempotent.  -/
Con.conGen_idem : ∀ {M : Type u_1} [inst : Mul M] (r : M → M → Prop), conGen ⇑(conGen r) = conGen r
-- Mathlib.RingTheory.DedekindDomain.Ideal.Lemmas
IsDedekindDomain.one_le_primesOver_ncard : ∀ {A : Type u_4} [inst : CommRing A] (p : Ideal A) [hpm : p.IsMaximal] (B : Type u_5) [inst_1 : CommRing B]
  [IsDedekindDomain B] [inst_3 : Algebra A B] [IsDomain A] [Module.IsTorsionFree A B] [Algebra.IsIntegral A B],
  1 ≤ (p.primesOver B).ncard
-- Mathlib.Order.Defs.LinearOrder
gt_or_lt_of_ne : ∀ {α : Type u_1} [inst : LinearOrder α] {a b : α}, a ≠ b → b < a ∨ a < b
-- Init.Data.ByteArray.Extra
/-- Interprets a `ByteArray` of size 8 as a big-endian `UInt64`.

Panics if the array's size is not 8.
 -/
ByteArray.toUInt64BE! : ByteArray → UInt64
-- Mathlib.Probability.Distributions.Gaussian.HasGaussianLaw.Basic
/-- A Gaussian random variable has moments of all orders.  -/
ProbabilityTheory.HasGaussianLaw.memLp : ∀ {Ω : Type u_1} {E : Type u_2} {mΩ : MeasurableSpace Ω} {P : MeasureTheory.Measure Ω} [inst : NormedAddCommGroup E]
  [inst_1 : MeasurableSpace E] [BorelSpace E] {X : Ω → E} [inst_3 : NormedSpace ℝ E] [CompleteSpace E]
  [SecondCountableTopology E], ProbabilityTheory.HasGaussianLaw X P → ∀ {p : ENNReal}, p ≠ ⊤ → MeasureTheory.MemLp X p P
-- Mathlib.Tactic.ITauto
/-- `(p: B) ⊢ A ∨ B`  -/
Mathlib.Tactic.ITauto.Proof.orInR : Mathlib.Tactic.ITauto.Proof → Mathlib.Tactic.ITauto.Proof
-- Mathlib.AlgebraicTopology.DoldKan.SplitSimplicialObject
CategoryTheory.SimplicialObject.Splitting.fromNondegComplex_toNondegComplex_assoc : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] {X : CategoryTheory.SimplicialObject C} (s : X.Splitting)
  [inst_1 : CategoryTheory.Preadditive C] {Z : ChainComplex C ℕ} (h : s.nondegComplex ⟶ Z),
  CategoryTheory.CategoryStruct.comp s.fromNondegComplex (CategoryTheory.CategoryStruct.comp s.toNondegComplex h) = h
-- Mathlib.Order.Interval.Finset.Defs
Set.finite_iff_bddAbove : ∀ {α : Type u_3} {s : Set α} [inst : SemilatticeSup α] [LocallyFiniteOrder α] [OrderBot α], s.Finite ↔ BddAbove s
-- Mathlib.RepresentationTheory.Intertwining
Representation.Equiv.trans_apply : ∀ {A : Type u_1} {G : Type u_2} {V : Type u_3} {W : Type u_4} {U : Type u_5} [inst : Semiring A] [inst_1 : Monoid G]
  [inst_2 : AddCommMonoid V] [inst_3 : AddCommMonoid W] [inst_4 : AddCommMonoid U] [inst_5 : Module A V]
  [inst_6 : Module A W] [inst_7 : Module A U] {ρ : Representation A G V} {σ : Representation A G W}
  {τ : Representation A G U} (φ : ρ.Equiv σ) (ψ : σ.Equiv τ) (v : V), (φ.trans ψ) v = ψ (φ v)
-- Mathlib.Analysis.Normed.Operator.BanachSteinhaus
/-- This version of Banach-Steinhaus is stated in terms of suprema of `↑‖·‖₊ : ℝ≥0∞`
for convenience.  -/
banach_steinhaus_iSup_nnnorm : ∀ {E : Type u_1} {F : Type u_2} {𝕜 : Type u_3} {𝕜₂ : Type u_4} [inst : SeminormedAddCommGroup E]
  [inst_1 : SeminormedAddCommGroup F] [inst_2 : NontriviallyNormedField 𝕜] [inst_3 : NontriviallyNormedField 𝕜₂]
  [inst_4 : NormedSpace 𝕜 E] [inst_5 : NormedSpace 𝕜₂ F] {σ₁₂ : 𝕜 →+* 𝕜₂} [inst_6 : RingHomIsometric σ₁₂] {ι : Type u_5}
  [CompleteSpace E] {g : ι → E →SL[σ₁₂] F}, (∀ (x : E), ⨆ i, ↑‖(g i) x‖₊ < ⊤) → ⨆ i, ↑‖g i‖₊ < ⊤
-- Mathlib.LinearAlgebra.RootSystem.Finite.G2
/-- The short root `3α + β`.  -/
RootPairing.EmbeddedG2.threeShortAddLongRoot : {ι : Type u_1} →
  {R : Type u_2} →
    {M : Type u_3} →
      {N : Type u_4} →
        [inst : CommRing R] →
          [inst_1 : AddCommGroup M] →
            [inst_2 : Module R M] →
              [inst_3 : AddCommGroup N] → [inst_4 : Module R N] → (P : RootPairing ι R M N) → [P.EmbeddedG2] → M
-- Mathlib.Algebra.Star.LinearMap
/-- The involutive intrinsic star structure on linear maps.  -/
LinearMap.intrinsicInvolutiveStar : {R : Type u_1} →
  {E : Type u_2} →
    {F : Type u_3} →
      [inst : Semiring R] →
        [inst_1 : InvolutiveStar R] →
          [inst_2 : AddCommMonoid E] →
            [inst_3 : Module R E] →
              [inst_4 : StarAddMonoid E] →
                [StarModule R E] →
                  [inst_6 : AddCommMonoid F] →
                    [inst_7 : Module R F] →
                      [inst_8 : StarAddMonoid F] → [StarModule R F] → InvolutiveStar (WithConv (E →ₗ[R] F))