mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Control.Traversable.Instances
_private.Mathlib.Control.Traversable.Instances.0.Sum.traverse.match_1.splitter : {σ : Type u_1} →
  {α : Type u_2} →
    (motive : σ ⊕ α → Sort u_3) →
      (x : σ ⊕ α) → ((x : σ) → motive (Sum.inl x)) → ((x : α) → motive (Sum.inr x)) → motive x
-- Mathlib.Analysis.CStarAlgebra.CStarMatrix
CStarMatrix.map_id' : ∀ {m : Type u_1} {n : Type u_2} {A : Type u_5} (M : CStarMatrix m n A), (M.map fun x => x) = M
-- Mathlib.RingTheory.Localization.FractionRing
IsFractionRing.inv_def : ∀ (A : Type u_6) [inst : CommRing A] {K : Type u_7} [inst_1 : CommRing K] [inst_2 : Algebra A K]
  [inst_3 : IsFractionRing A K] [inst_4 : IsDomain A] (z : K),
  IsFractionRing.inv A z =
    if h : z = 0 then 0
    else
      IsLocalization.mk' K ↑(IsLocalization.sec (nonZeroDivisors A) z).2
        ⟨(IsLocalization.sec (nonZeroDivisors A) z).1, ⋯⟩
-- Batteries.Tactic.Lint.Simp
/-- The data associated to a simp theorem.  -/
Batteries.Tactic.Lint.SimpTheoremInfo : Type
-- Mathlib.Algebra.Group.Submonoid.MulOpposite
/-- Bijection between an additive submonoid `H` and its opposite.  -/
AddSubmonoid.equivOp : {M : Type u_2} → [inst : AddZeroClass M] → (H : AddSubmonoid M) → ↥H ≃ ↥H.op
-- Init.Data.Int.Order
Int.le_of_sub_nonneg : ∀ {a b : ℤ}, 0 ≤ a - b → b ≤ a
-- Mathlib.CategoryTheory.Bicategory.EqToHom
CategoryTheory.Bicategory.eqToHomTransIso_refl_left : ∀ {B : Type u} [inst : CategoryTheory.Bicategory B] {x y : B} (e₁ : x = y),
  CategoryTheory.Bicategory.eqToHomTransIso ⋯ e₁ =
    (CategoryTheory.Bicategory.leftUnitor (CategoryTheory.eqToHom e₁)).symm
-- Std.Data.Iterators.Combinators.Monadic.Drop
/-- Internal implementation detail of the iterator library  -/
Std.Iterators.Types.Drop.inner : {α : Type w} → {m : Type w → Type w'} → {β : Type w} → Std.Iterators.Types.Drop α m β → Std.IterM m β
-- Mathlib.Algebra.Notation.Pi.Defs
Pi.instInv : {ι : Type u_1} → {G : ι → Type u_4} → [(i : ι) → Inv (G i)] → Inv ((i : ι) → G i)
-- Mathlib.Combinatorics.SetFamily.AhlswedeZhang
_private.Mathlib.Combinatorics.SetFamily.AhlswedeZhang.0.Finset.sup_aux : ∀ {α : Type u_1} [inst : SemilatticeSup α] {s : Finset α} {a : α} [inst_1 : DecidableLE α],
  a ∈ lowerClosure ↑s → {b ∈ s | a ≤ b}.Nonempty
-- Mathlib.Algebra.Order.Monoid.Unbundled.Basic
min_le_max_of_add_le_add : ∀ {α : Type u_1} [inst : Add α] [inst_1 : LinearOrder α] {a b c d : α} [AddLeftStrictMono α] [AddRightStrictMono α],
  a + b ≤ c + d → min a b ≤ max c d
-- Mathlib.Data.ZMod.Basic
ZMod.coprime_mod_iff_coprime : ∀ (m n : ℕ), (m % n).Coprime n ↔ m.Coprime n
-- Mathlib.Algebra.Divisibility.Prod
instDecompositionMonoidForall : ∀ {ι : Type u_1} {G : ι → Type u_4} [inst : (i : ι) → Semigroup (G i)] [∀ (i : ι), DecompositionMonoid (G i)],
  DecompositionMonoid ((i : ι) → G i)
-- Mathlib.CategoryTheory.Sites.Hypercover.Zero
CategoryTheory.PreZeroHypercover.inv_hom_h₀_comp_f : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {S : C} {E F : CategoryTheory.PreZeroHypercover S} (e : E ≅ F)
  (i : E.I₀), CategoryTheory.CategoryStruct.comp (CategoryTheory.inv (e.hom.h₀ i)) (E.f i) = F.f (e.hom.s₀ i)
-- Mathlib.AlgebraicGeometry.EllipticCurve.Jacobian.Formula
_private.Mathlib.AlgebraicGeometry.EllipticCurve.Jacobian.Formula.0.WeierstrassCurve.Jacobian.toAffine_addX_of_eq : ∀ {F : Type u} [inst : Field F] {W : WeierstrassCurve.Jacobian F} {P : Fin 3 → F},
  P 2 ≠ 0 →
    ∀ {n d : F},
      d ≠ 0 →
        W.toAffine.addX (P 0 / P 2 ^ 2) (P 0 / P 2 ^ 2) (-n / (P 2 * d)) =
          (n ^ 2 - W.a₁ * n * P 2 * d - W.a₂ * P 2 ^ 2 * d ^ 2 - 2 * P 0 * d ^ 2) / (P 2 * d) ^ 2
-- Mathlib.GroupTheory.Schreier
/-- A theorem of Schur: The size of the commutator subgroup is bounded in terms of the number of
commutators.  -/
Subgroup.card_commutator_le_of_finite_commutatorSet : ∀ (G : Type u_1) [inst : Group G] [Finite ↑(commutatorSet G)],
  Nat.card ↥(commutator G) ≤ Subgroup.cardCommutatorBound (Nat.card ↑(commutatorSet G))
-- Mathlib.Combinatorics.SimpleGraph.Clique
SimpleGraph.cliqueFreeOn_two : ∀ {α : Type u_1} (G : SimpleGraph α) {s : Set α}, G.CliqueFreeOn s 2 ↔ s.Pairwise G.Adjᶜ
-- Std.Http.Data.URI.Basic
Std.Http.URI.mk.sizeOf_spec : ∀ (scheme : Std.Http.URI.Scheme) (authority : Option Std.Http.URI.Authority) (path : Std.Http.URI.Path)
  (query : Std.Http.URI.Query) (fragment : Option String),
  sizeOf { scheme := scheme, authority := authority, path := path, query := query, fragment := fragment } =
    1 + sizeOf scheme + sizeOf authority + sizeOf path + sizeOf query + sizeOf fragment
-- Mathlib.Topology.FiberBundle.Constructions
Bundle.Trivialization.toPretrivialization.eq_1 : ∀ {B : Type u_1} {F : Type u_2} {Z : Type u_4} [inst : TopologicalSpace B] [inst_1 : TopologicalSpace F] {proj : Z → B}
  [inst_2 : TopologicalSpace Z] (e : Bundle.Trivialization F proj),
  e.toPretrivialization =
    { toPartialEquiv := e.toPartialEquiv, open_target := ⋯, baseSet := e.baseSet, open_baseSet := ⋯, source_eq := ⋯,
      target_eq := ⋯, proj_toFun := ⋯ }
-- Init.Data.SInt.Lemmas
Int32.sub_lt : ∀ {a b : Int32}, 0 < b → b ≤ a → a - b < a
-- Mathlib.MeasureTheory.Integral.Lebesgue.Basic
MeasureTheory.Measure.ext_iff_lintegral : ∀ {α : Type u_1} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} (ν : MeasureTheory.Measure α),
  μ = ν ↔ ∀ (f : α → ENNReal), Measurable f → ∫⁻ (a : α), f a ∂μ = ∫⁻ (a : α), f a ∂ν
-- Mathlib.CategoryTheory.Limits.HasLimits
/-- The colimit functor and constant functor are adjoint to each other
 -/
CategoryTheory.Limits.colimConstAdj : {J : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} J] →
    {C : Type u} →
      [inst_1 : CategoryTheory.Category.{v, u} C] →
        [inst_2 : CategoryTheory.Limits.HasColimitsOfShape J C] →
          CategoryTheory.Limits.colim ⊣ CategoryTheory.Functor.const J
-- Mathlib.CategoryTheory.Monoidal.Cartesian.Basic
CategoryTheory.CartesianMonoidalCategory.instNonemptyBraidedCategory : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.CartesianMonoidalCategory C],
  Nonempty (CategoryTheory.BraidedCategory C)
-- Mathlib.Algebra.Homology.HomotopyCategory.HomComplexSingle
CochainComplex.HomComplex.Cochain.toSingleMk_precomp : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Preadditive C]
  [inst_2 : CategoryTheory.Limits.HasZeroObject C] {X : C} {K : CochainComplex C ℤ} {p q : ℤ} (f : K.X p ⟶ X) {n : ℤ}
  (h : p + n = q) {L : CochainComplex C ℤ} (g : L ⟶ K),
  CochainComplex.HomComplex.Cochain.toSingleMk (CategoryTheory.CategoryStruct.comp (g.f p) f) h =
    (CochainComplex.HomComplex.Cochain.ofHom g).comp (CochainComplex.HomComplex.Cochain.toSingleMk f h) ⋯
-- Mathlib.Analysis.InnerProductSpace.Orthogonal
/-- The inf of a set of orthogonal subspaces equals the subspace orthogonal to the sup.  -/
ClosedSubmodule.sInf_orthogonal : ∀ {𝕜 : Type u_4} {E : Type u_5} [inst : RCLike 𝕜] [inst_1 : NormedAddCommGroup E] [inst_2 : InnerProductSpace 𝕜 E]
  (s : Set (ClosedSubmodule 𝕜 E)), ⨅ K ∈ s, Kᗮ = (sSup s)ᗮ
-- Std.Data.DTreeMap.Raw.Lemmas
Std.DTreeMap.Raw.size_filter_eq_size_iff : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t : Std.DTreeMap.Raw α β cmp} [Std.TransCmp cmp]
  [inst : Std.LawfulEqCmp cmp] {f : (a : α) → β a → Bool},
  t.WF → ((Std.DTreeMap.Raw.filter f t).size = t.size ↔ ∀ (k : α) (h : k ∈ t), f k (t.get k h) = true)
-- Mathlib.Algebra.Homology.ShortComplex.Basic
/-- The functor `ShortComplex C ⥤ ShortComplex D` induced by a functor `C ⥤ D` which
preserves zero morphisms.  -/
CategoryTheory.Functor.mapShortComplex : {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] →
        [inst_2 : CategoryTheory.Limits.HasZeroMorphisms C] →
          [inst_3 : CategoryTheory.Limits.HasZeroMorphisms D] →
            (F : CategoryTheory.Functor C D) →
              [F.PreservesZeroMorphisms] →
                CategoryTheory.Functor (CategoryTheory.ShortComplex C) (CategoryTheory.ShortComplex D)
-- Lean.Meta.Basic
/-- Execute `x` ensuring the transparency setting is at least `mode`.
Recall that `.none < .reducible < .instances < .implicit < .default < .all`.
 -/
Lean.Meta.withAtLeastTransparency : {n : Type → Type u_1} → [MonadControlT Lean.MetaM n] → [Monad n] → {α : Type} → Lean.Meta.TransparencyMode → n α → n α
-- Mathlib.Analysis.RCLike.Basic
/-- Given a normed field `𝕜` satisfying `IsRCLikeNormedField 𝕜`, build an associated `RCLike 𝕜`
structure on `𝕜` which is definitionally compatible with the given normed field structure.  -/
IsRCLikeNormedField.rclike : (𝕜 : Type u_3) → [hk : NormedField 𝕜] → [h : IsRCLikeNormedField 𝕜] → RCLike 𝕜
-- Init.Data.Option.Lemmas
Option.max_filter_right : ∀ {α : Type u_1} [inst : Max α] [Std.IdempotentOp max] {p : α → Bool} {o : Option α}, o ⊔ Option.filter p o = o
-- Mathlib.Tactic.TacticAnalysis
Mathlib.TacticAnalysis.Config.mk.sizeOf_spec : ∀ (run : Array Mathlib.TacticAnalysis.TacticNode → Lean.Elab.Command.CommandElabM Unit), sizeOf { run := run } = 1
-- Mathlib.Order.Antichain
Set.Subsingleton.isWeakAntichain : ∀ {ι : Type u_1} {α : ι → Type u_2} [inst : (i : ι) → Preorder (α i)] {s : Set ((i : ι) → α i)},
  s.Subsingleton → IsWeakAntichain s
-- Mathlib.Algebra.BigOperators.Group.List.Basic
List.prod_mul_prod_eq_prod_zipWith_of_length_eq : ∀ {M : Type u_4} [inst : CommMonoid M] (l l' : List M),
  l.length = l'.length → l.prod * l'.prod = (List.zipWith (fun x1 x2 => x1 * x2) l l').prod
-- Mathlib.Topology.Path
Path.source : ∀ {X : Type u_1} [inst : TopologicalSpace X] {x y : X} (γ : Path x y), γ 0 = x
-- Mathlib.RingTheory.Smooth.AdicCompletion
_private.Mathlib.RingTheory.Smooth.AdicCompletion.0.Algebra.FormallySmooth.liftAdicCompletionAux.eq_2 : ∀ {R : Type u_1} {A : Type u_2} [inst : CommRing R] [inst_1 : CommRing A] [inst_2 : Algebra R A] {S : Type u_3}
  [inst_3 : CommRing S] [inst_4 : Algebra R S] (I : Ideal S) (f : A →ₐ[R] S ⧸ I) [inst_5 : Algebra.FormallySmooth R A],
  Algebra.FormallySmooth.liftAdicCompletionAux✝ I f 1 = (↑(Ideal.quotientEquivAlgOfEq R ⋯)).comp f
-- Init.Grind.AC
Lean.Grind.AC.Seq.denote_concat : ∀ {α : Sort u_1} (ctx : Lean.Grind.AC.Context α) {inst₁ : Std.Associative ctx.op} (s₁ s₂ : Lean.Grind.AC.Seq),
  Lean.Grind.AC.Seq.denote ctx (s₁.concat s₂) =
    ctx.op (Lean.Grind.AC.Seq.denote ctx s₁) (Lean.Grind.AC.Seq.denote ctx s₂)
-- Mathlib.RingTheory.IntegralClosure.IsIntegralClosure.Basic
IsIntegral.inv_mem_adjoin : ∀ {R : Type u_1} {S : Type u_2} [inst : Field R] [inst_1 : DivisionRing S] [inst_2 : Algebra R S] {x : S},
  IsIntegral R x → x⁻¹ ∈ R[x]
-- Mathlib.Analysis.Convex.Deriv
/-- If `f` is convex on `S` and differentiable at all points of `S`, then its derivative is monotone
on `S`.  -/
StrictConvexOn.strictMonoOn_deriv : ∀ {S : Set ℝ} {f : ℝ → ℝ}, StrictConvexOn ℝ S f → (∀ x ∈ S, DifferentiableAt ℝ f x) → StrictMonoOn (deriv f) S
-- Std.Time.Zoned.Database.Windows
_private.Std.Time.Zoned.Database.Windows.0.Std.Time.Database.Windows.getZoneRules.toLocalTime : Std.Time.TimeZone → Std.Time.TimeZone.LocalTimeType
-- Mathlib.Algebra.Homology.Opposite
HomologicalComplex.instIsEquivalenceSymmOppositeUnopInverse : ∀ {ι : Type u_1} (V : Type u_2) [inst : CategoryTheory.Category.{v_1, u_2} V] (c : ComplexShape ι)
  [inst_1 : CategoryTheory.Limits.HasZeroMorphisms V], (HomologicalComplex.unopInverse V c).IsEquivalence
-- Init.Data.UInt.Basic
/-- Non-strict inequality of 32-bit unsigned integers, defined as inequality of the corresponding
natural numbers. Usually accessed via the `≤` operator.
 -/
UInt32.le : UInt32 → UInt32 → Prop
-- Mathlib.RingTheory.AdicCompletion.Basic
AdicCompletion.transitionMap_comp_eval : ∀ {R : Type u_1} [inst : CommRing R] (I : Ideal R) (M : Type u_4) [inst_1 : AddCommGroup M] [inst_2 : Module R M]
  {m n : ℕ} (hmn : m ≤ n), AdicCompletion.transitionMap I M hmn ∘ₗ AdicCompletion.eval I M n = AdicCompletion.eval I M m
-- Mathlib.Algebra.Colimit.DirectLimit
DirectLimit.inv₀_def : ∀ {ι : Type u_2} [inst : Preorder ι] {G : ι → Type u_3} {T : ⦃i j : ι⦄ → i ≤ j → Type u_6}
  {f : (x x_1 : ι) → (h : x ≤ x_1) → T h} [inst_1 : (i j : ι) → (h : i ≤ j) → FunLike (T h) (G i) (G j)]
  [inst_2 : DirectedSystem G fun x1 x2 x3 => ⇑(f x1 x2 x3)] [inst_3 : IsDirectedOrder ι] [inst_4 : Nonempty ι]
  [inst_5 : (i : ι) → GroupWithZero (G i)] [inst_6 : ∀ (i j : ι) (h : i ≤ j), MonoidWithZeroHomClass (T h) (G i) (G j)]
  (i : ι) (x : G i), (⟦⟨i, x⟩⟧)⁻¹ = ⟦⟨i, x⁻¹⟩⟧
-- Mathlib.Algebra.Order.GroupWithZero.Basic
posMulMono_iff_covariant_pos : ∀ {α : Type u_1} [inst : MulZeroClass α] [inst_1 : PartialOrder α],
  PosMulMono α ↔ CovariantClass { x // 0 < x } α (fun x y => ↑x * y) fun x1 x2 => x1 ≤ x2
-- Mathlib.LinearAlgebra.BilinearForm.Isometry
LinearMap.BilinForm.Isometry.toLinearMap_comp : ∀ {R : Type u_1} {M₁ : Type u_3} {M₂ : Type u_4} {M₃ : Type u_5} [inst : CommSemiring R] [inst_1 : AddCommMonoid M₁]
  [inst_2 : AddCommMonoid M₂] [inst_3 : AddCommMonoid M₃] [inst_4 : Module R M₁] [inst_5 : Module R M₂]
  [inst_6 : Module R M₃] {B₁ : LinearMap.BilinForm R M₁} {B₂ : LinearMap.BilinForm R M₂} {B₃ : LinearMap.BilinForm R M₃}
  (g : B₂ →bᵢ B₃) (f : B₁ →bᵢ B₂), (g.comp f).toLinearMap = g.toLinearMap ∘ₗ f.toLinearMap
-- Mathlib.Order.BooleanSubalgebra
BooleanSubalgebra.mem_bot : ∀ {α : Type u_2} [inst : BooleanAlgebra α] {a : α}, a ∈ ⊥ ↔ a = ⊥ ∨ a = ⊤
-- Mathlib.ModelTheory.Syntax
FirstOrder.Language.Term.relabelEquiv_apply : ∀ {L : FirstOrder.Language} {α : Type u'} {β : Type v'} (g : α ≃ β) (a : L.Term α),
  (FirstOrder.Language.Term.relabelEquiv g) a = FirstOrder.Language.Term.relabel (⇑g) a
-- Std.Sync.Channel
_private.Std.Sync.Channel.0.Std.Channel.mk : {α : Type} → Std.CloseableChannel α → Std.Channel α
-- Mathlib.Combinatorics.SimpleGraph.Regularity.Chunk
_private.Mathlib.Combinatorics.SimpleGraph.Regularity.Chunk.0.SzemerediRegularity.termM : Lean.ParserDescr
-- Mathlib.CategoryTheory.Limits.Presheaf
/-- The tautological cocone with point `P` is a colimit cocone, exhibiting `P` as a colimit of
representables. (In this version, we allow the presheaf `P` to have values in
a larger universe.)

Proposition 2.6.3(i) in [Kashiwara2006]  -/
CategoryTheory.Presheaf.isColimitTautologicalCocone' : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    (P : CategoryTheory.Functor Cᵒᵖ (Type (max w v₁))) →
      CategoryTheory.Limits.IsColimit (CategoryTheory.Presheaf.tautologicalCocone' P)
-- Mathlib.LinearAlgebra.LinearIndependent.Defs
/-- An indexed set of vectors is linearly dependent iff there are two distinct
`Finsupp.LinearCombination`s of the vectors with the same value.  -/
linearDepOn_iff'ₛ : ∀ {ι : Type u'} {R : Type u_2} {s : Set ι} {M : Type u_4} {v : ι → M} [inst : Semiring R] [inst_1 : AddCommMonoid M]
  [inst_2 : Module R M],
  ¬LinearIndepOn R v s ↔
    ∃ f g,
      f ∈ Finsupp.supported R R s ∧
        g ∈ Finsupp.supported R R s ∧ (Finsupp.linearCombination R v) f = (Finsupp.linearCombination R v) g ∧ f ≠ g
-- Mathlib.Topology.Algebra.Valued.NormedValued
Valued.toNormedField.norm_def : ∀ {L : Type u_1} [inst : Field L] {Γ₀ : Type u_2} [inst_1 : LinearOrderedCommGroupWithZero Γ₀] [val : Valued L Γ₀]
  [hv : Valued.v.RankOne] {x : L}, ‖x‖ = ↑((Valuation.RankOne.hom Valued.v) (Valued.v.restrict x))
-- Mathlib.Algebra.BigOperators.Finprod
Finset.mulSupport_of_fiberwise_prod_subset_image : ∀ {α : Type u_1} {β : Type u_2} {M : Type u_5} [inst : CommMonoid M] [inst_1 : DecidableEq β] (s : Finset α) (f : α → M)
  (g : α → β), (Function.mulSupport fun b => ∏ a ∈ s with g a = b, f a) ⊆ ↑(Finset.image g s)
-- Mathlib.RingTheory.GradedAlgebra.HomogeneousLocalization
HomogeneousLocalization.val_nsmul : ∀ {ι : Type u_1} {A : Type u_2} {σ : Type u_3} [inst : CommRing A] [inst_1 : SetLike σ A]
  [inst_2 : AddSubmonoidClass σ A] {𝒜 : ι → σ} (x : Submonoid A) (n : ℕ) (y : HomogeneousLocalization 𝒜 x),
  (n • y).val = n • y.val
-- Mathlib.NumberTheory.Zsqrtd.Basic
Zsqrtd.norm.eq_1 : ∀ {d : ℤ} (n : ℤ√d), n.norm = n.re * n.re - d * n.im * n.im
-- Init.System.IO
IO.instMonadLiftSTRealWorldBaseIO : MonadLift (ST IO.RealWorld) BaseIO
-- Mathlib.AlgebraicGeometry.EllipticCurve.Affine.Point
_private.Mathlib.AlgebraicGeometry.EllipticCurve.Affine.Point.0.WeierstrassCurve.Affine.Point.neg.match_1.eq_1 : ∀ {R : Type u_1} [inst : CommRing R] {W' : WeierstrassCurve.Affine R} (motive : W'.Point → Sort u_2)
  (h_1 : Unit → motive WeierstrassCurve.Affine.Point.zero)
  (h_2 : (x y : R) → (h : W'.Nonsingular x y) → motive (WeierstrassCurve.Affine.Point.some x y h)),
  (match WeierstrassCurve.Affine.Point.zero with
    | WeierstrassCurve.Affine.Point.zero => h_1 ()
    | WeierstrassCurve.Affine.Point.some x y h => h_2 x y h) =
    h_1 ()
-- Std.Data.DTreeMap.Internal.WF.Lemmas
Std.DTreeMap.Internal.Impl.minKey?_eq_minKey? : ∀ {α : Type u} {β : α → Type v} {x : Ord α} [Std.TransOrd α] {l : Std.DTreeMap.Internal.Impl α β},
  l.Ordered → l.minKey? = Std.Internal.List.minKey? l.toListModel
-- Init.Data.Range.Polymorphic.Instances
Std.Rxi.instIsAlwaysFiniteOfLawfulHasSize : ∀ {α : Type u_1} [LT α] [inst : Std.PRange.UpwardEnumerable α] [Std.PRange.LawfulUpwardEnumerable α]
  [inst_2 : Std.Rxi.HasSize α] [Std.Rxi.LawfulHasSize α], Std.Rxi.IsAlwaysFinite α
-- Mathlib.CategoryTheory.Monoidal.Free.Coherence
_private.Mathlib.CategoryTheory.Monoidal.Free.Coherence.0.CategoryTheory.FreeMonoidalCategory.normalizeMapAux.match_1.splitter : {C : Type u_1} →
  (motive : CategoryTheory.Discrete (CategoryTheory.FreeMonoidalCategory.NormalMonoidalObject C) → Sort u_2) →
    (x : CategoryTheory.Discrete (CategoryTheory.FreeMonoidalCategory.NormalMonoidalObject C)) →
      ((X : CategoryTheory.FreeMonoidalCategory.NormalMonoidalObject C) → motive { as := X }) → motive x
-- Mathlib.Probability.Combinatorics.BinomialRandomGraph.Defs
SimpleGraph.binomialRandom_apply' : ∀ {V : Type u_1} (p : ↑unitInterval) [Countable V] (S : Set (SimpleGraph V)),
  (SimpleGraph.binomialRandom V p) S = (ProbabilityTheory.setBernoulli Sym2.diagSetᶜ p) (SimpleGraph.edgeSet '' S)
-- Mathlib.AlgebraicGeometry.FunctionField
AlgebraicGeometry.IsAffineOpen.primeIdealOf_genericPoint : ∀ {X : AlgebraicGeometry.Scheme} [inst : AlgebraicGeometry.IsIntegral X] {U : X.Opens}
  (hU : AlgebraicGeometry.IsAffineOpen U) [h : Nonempty ↥↑U],
  hU.primeIdealOf ⟨genericPoint ↥X, ⋯⟩ = genericPoint ↥(AlgebraicGeometry.Spec (X.presheaf.obj (Opposite.op U)))
-- Lean.Meta.Tactic.Grind.PP
/-- Pretty print goal state for debugging purposes.  -/
Lean.Meta.Grind.Goal.ppState : Lean.Meta.Grind.Goal → Lean.MetaM Lean.MessageData
-- Mathlib.GroupTheory.Perm.Sign
Equiv.Perm.signAux_eq_signAux2 : ∀ {α : Type u} [inst : DecidableEq α] {n : ℕ} (l : List α) (f : Equiv.Perm α) (e : α ≃ Fin n),
  (∀ (x : α), f x ≠ x → x ∈ l) → Equiv.Perm.signAux ((e.symm.trans f).trans e) = Equiv.Perm.signAux2 l f
-- Mathlib.Analysis.Complex.Norm
Complex.sq_norm : ∀ (z : ℂ), ‖z‖ ^ 2 = Complex.normSq z
-- Mathlib.Analysis.SpecificLimits.Basic
hasSum_geometric_two : HasSum (fun n => (1 / 2) ^ n) 2
-- Mathlib.MeasureTheory.Integral.Bochner.Set
MeasureTheory.integral_piecewise : ∀ {X : Type u_1} {E : Type u_3} {mX : MeasurableSpace X} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E]
  {f g : X → E} {s : Set X} {μ : MeasureTheory.Measure X} [inst_2 : DecidablePred fun x => x ∈ s],
  MeasurableSet s →
    MeasureTheory.IntegrableOn f s μ →
      MeasureTheory.IntegrableOn g sᶜ μ →
        ∫ (x : X), s.piecewise f g x ∂μ = ∫ (x : X) in s, f x ∂μ + ∫ (x : X) in sᶜ, g x ∂μ
-- Mathlib.Algebra.Module.PointwisePi
smul_univ_pi : ∀ {K : Type u_1} {ι : Type u_2} {R : ι → Type u_3} [inst : (i : ι) → SMul K (R i)] (r : K) (t : (i : ι) → Set (R i)),
  r • Set.univ.pi t = Set.univ.pi (r • t)
-- Mathlib.Analysis.InnerProductSpace.LinearMap
/-- The inner product as a continuous sesquilinear map, with the two arguments flipped.  -/
innerSLFlip : (𝕜 : Type u_1) →
  {E : Type u_2} →
    [inst : RCLike 𝕜] → [inst_1 : SeminormedAddCommGroup E] → [inst_2 : InnerProductSpace 𝕜 E] → E →L[𝕜] E →L⋆[𝕜] 𝕜
-- Mathlib.AlgebraicGeometry.Morphisms.IsIso
AlgebraicGeometry.isIso_iff_isOpenImmersion_and_surjective : ∀ {X Y : AlgebraicGeometry.Scheme} (f : X ⟶ Y),
  CategoryTheory.IsIso f ↔ AlgebraicGeometry.IsOpenImmersion f ∧ AlgebraicGeometry.Surjective f
-- Mathlib.CategoryTheory.Square
CategoryTheory.Square.arrowArrowEquivalence'_counitIso : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C],
  CategoryTheory.Square.arrowArrowEquivalence'.counitIso =
    CategoryTheory.Iso.refl
      (CategoryTheory.Square.fromArrowArrowFunctor'.comp CategoryTheory.Square.toArrowArrowFunctor')
-- Mathlib.RingTheory.IsTensorProduct
Algebra.isPushout_iff : ∀ (R : Type u_1) (S : Type v₃) [inst : CommSemiring R] [inst_1 : CommSemiring S] [inst_2 : Algebra R S] (R' : Type u_6)
  (S' : Type u_7) [inst_3 : CommSemiring R'] [inst_4 : CommSemiring S'] [inst_5 : Algebra R R'] [inst_6 : Algebra S S']
  [inst_7 : Algebra R' S'] [inst_8 : Algebra R S'] [inst_9 : IsScalarTower R R' S'] [inst_10 : IsScalarTower R S S'],
  Algebra.IsPushout R S R' S' ↔ IsBaseChange S (IsScalarTower.toAlgHom R R' S').toLinearMap
-- Mathlib.Geometry.Manifold.HasGroupoid
mem_maximalAtlas_iff : ∀ {H : Type u} {M : Type u_2} [inst : TopologicalSpace H] [inst_1 : TopologicalSpace M] [inst_2 : ChartedSpace H M]
  {G : StructureGroupoid H} {e : OpenPartialHomeomorph M H},
  e ∈ StructureGroupoid.maximalAtlas M G ↔ ∀ e' ∈ atlas H M, e.symm.trans e' ∈ G ∧ e'.symm.trans e ∈ G
-- Mathlib.Analysis.Asymptotics.Defs
Asymptotics.IsLittleO.prod_left_fst : ∀ {α : Type u_1} {E' : Type u_6} {F' : Type u_7} {G' : Type u_8} [inst : SeminormedAddCommGroup E']
  [inst_1 : SeminormedAddCommGroup F'] [inst_2 : SeminormedAddCommGroup G'] {f' : α → E'} {g' : α → F'} {k' : α → G'}
  {l : Filter α}, (fun x => (f' x, g' x)) =o[l] k' → f' =o[l] k'
-- Mathlib.Geometry.RingedSpace.OpenImmersion
/-- The functor `Opens X ⥤ Opens Y` associated with an open immersion `f : X ⟶ Y`.  -/
AlgebraicGeometry.LocallyRingedSpace.IsOpenImmersion.opensFunctor : {X Y : AlgebraicGeometry.LocallyRingedSpace} →
  (f : X ⟶ Y) →
    [H : AlgebraicGeometry.LocallyRingedSpace.IsOpenImmersion f] →
      CategoryTheory.Functor (TopologicalSpace.Opens ↑X.toTopCat) (TopologicalSpace.Opens ↑Y.toTopCat)
-- Mathlib.Algebra.Order.Monoid.Unbundled.TypeTags
Additive.toMul_bot : ∀ {α : Type u_1} [inst : LE α] [inst_1 : OrderBot α], Additive.toMul ⊥ = ⊥
-- Mathlib.Analysis.Normed.Operator.BoundedLinearMaps
IsBoundedLinearMap.toIsLinearMap : ∀ {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [inst : Semiring 𝕜] [inst_1 : SeminormedAddCommGroup E]
  [inst_2 : Module 𝕜 E] [inst_3 : SeminormedAddCommGroup F] [inst_4 : Module 𝕜 F] {f : E → F},
  IsBoundedLinearMap 𝕜 f → IsLinearMap 𝕜 f
-- Mathlib.Order.Category.FinBoolAlg
FinBoolAlg.forgetToBoolAlgFaithful : (CategoryTheory.forget₂ FinBoolAlg BoolAlg).Faithful
-- Std.Time.Internal.Bounded
/-- Adjust the bounds of a `Bounded` by changing the higher bound if another value `j` satisfies the same
constraint.
 -/
Std.Time.Internal.Bounded.LE.truncateTop : {n m j : ℤ} → (bounded : Std.Time.Internal.Bounded.LE n m) → ↑bounded ≤ j → Std.Time.Internal.Bounded.LE n j
-- Lean.Meta.Basic
Lean.Meta.mkInfoCacheKey : Lean.Expr → Option ℕ → Lean.MetaM Lean.Meta.InfoCacheKey
-- Mathlib.Data.Nat.Size
Nat.size_le_size : ∀ {m n : ℕ}, m ≤ n → m.size ≤ n.size
-- Mathlib.Analysis.SpecialFunctions.Gamma.BohrMollerup
Real.BohrMollerup.f_add_nat_eq : ∀ {f : ℝ → ℝ} {x : ℝ},
  (∀ {y : ℝ}, 0 < y → f (y + 1) = f y + Real.log y) →
    0 < x → ∀ (n : ℕ), f (x + ↑n) = f x + ∑ m ∈ Finset.range n, Real.log (x + ↑m)
-- Mathlib.Topology.Sets.Opens
/-- The type of open subsets of a topological space.  -/
TopologicalSpace.Opens : (α : Type u_2) → [TopologicalSpace α] → Type u_2
-- Mathlib.GroupTheory.Index
Subgroup.isFiniteRelIndex_of_le_left : ∀ {G : Type u_1} [inst : Group G] {H K : Subgroup G} (L : Subgroup G) [H.IsFiniteRelIndex L],
  H ≤ K → K.IsFiniteRelIndex L
-- Mathlib.CategoryTheory.Monoidal.Mon
CategoryTheory.AddMon.Hom.ext : ∀ {C : Type u₁} {inst : CategoryTheory.Category.{v₁, u₁} C} {inst_1 : CategoryTheory.MonoidalCategory C}
  {M N : CategoryTheory.AddMon C} {x y : M.Hom N}, x.hom = y.hom → x = y
-- Mathlib.CategoryTheory.Center.Basic
CategoryTheory.CatCenter.ext_iff : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {x y : CategoryTheory.CatCenter C},
  x = y ↔ ∀ (X : C), x.app X = y.app X