mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Analysis.Normed.Operator.Bilinear
_private.Mathlib.Analysis.Normed.Operator.Bilinear.0.ContinuousLinearMap.le_norm_flip : ∀ {𝕜 : Type u_1} {𝕜₂ : Type u_2} {𝕜₃ : Type u_3} {E : Type u_4} {F : Type u_6} {G : Type u_8}
  [inst : SeminormedAddCommGroup E] [inst_1 : SeminormedAddCommGroup F] [inst_2 : SeminormedAddCommGroup G]
  [inst_3 : NontriviallyNormedField 𝕜] [inst_4 : NontriviallyNormedField 𝕜₂] [inst_5 : NontriviallyNormedField 𝕜₃]
  [inst_6 : NormedSpace 𝕜 E] [inst_7 : NormedSpace 𝕜₂ F] [inst_8 : NormedSpace 𝕜₃ G] {σ₂₃ : 𝕜₂ →+* 𝕜₃} {σ₁₃ : 𝕜 →+* 𝕜₃}
  [inst_9 : RingHomIsometric σ₂₃] [inst_10 : RingHomIsometric σ₁₃] (f : E →SL[σ₁₃] F →SL[σ₂₃] G), ‖f‖ ≤ ‖f.flip‖
-- Mathlib.Analysis.Calculus.Deriv.Basic
derivWithin_of_mem_nhdsWithin : ∀ {𝕜 : Type u} [inst : NontriviallyNormedField 𝕜] {F : Type v} [inst_1 : NormedAddCommGroup F]
  [inst_2 : NormedSpace 𝕜 F] {f : 𝕜 → F} {x : 𝕜} {s t : Set 𝕜},
  t ∈ nhdsWithin x s → UniqueDiffWithinAt 𝕜 s x → DifferentiableWithinAt 𝕜 f t x → derivWithin f s x = derivWithin f t x
-- Init.Meta.Defs
/-- Decodes macro hygiene information.
 -/
Lean.TSyntax.getHygieneInfo : Lean.HygieneInfo → Lean.Name
-- Mathlib.Data.ENat.Lattice
ENat.iInf_natCast_eq_top : ∀ {ι : Sort u_1} {f : ι → ℕ}, ⨅ i, ↑(f i) = ⊤ ↔ IsEmpty ι
-- Mathlib.RingTheory.Polynomial.Radical
divRadical_dvd_wronskian_left : ∀ {k : Type u_1} [inst : Field k] [inst_1 : DecidableEq k] (a b : Polynomial k),
  EuclideanDomain.divRadical a ∣ a.wronskian b
-- Mathlib.Data.Finset.Defs
Multiset.canLiftFinset : ∀ {α : Type u_4}, CanLift (Multiset α) (Finset α) Finset.val Multiset.Nodup
-- Mathlib.AlgebraicTopology.ModelCategory.FibrantObjectHomotopy
HomotopicalAlgebra.FibrantObject.instIsIsoFunctorWhiskerRightHoCatιCompResolutionNatTransOfIsLocalizationWeakEquivalences : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : HomotopicalAlgebra.ModelCategory C]
  {D : Type u_2} [inst_2 : CategoryTheory.Category.{v_2, u_2} D]
  (L : CategoryTheory.Functor (HomotopicalAlgebra.FibrantObject.HoCat C) D)
  [L.IsLocalization (HomotopicalAlgebra.weakEquivalences (HomotopicalAlgebra.FibrantObject.HoCat C))],
  CategoryTheory.IsIso
    (CategoryTheory.Functor.whiskerRight HomotopicalAlgebra.FibrantObject.HoCat.ιCompResolutionNatTrans L)
-- Mathlib.Algebra.Star.SelfAdjoint
IsSelfAdjoint.smul : ∀ {R : Type u_1} {A : Type u_2} [inst : Star R] [inst_1 : Star A] [inst_2 : SMul R A] [StarModule R A] {r : R},
  IsSelfAdjoint r → ∀ {x : A}, IsSelfAdjoint x → IsSelfAdjoint (r • x)
-- Std.Http.Data.Response
/-- The response status-line information.
 -/
Std.Http.Response.line : {t : Type} → Std.Http.Response t → Std.Http.Response.Head
-- Mathlib.Topology.Separation.Profinite
isTopologicalBasis_isClopen : ∀ {X : Type u_1} [inst : TopologicalSpace X] [T2Space X] [CompactSpace X] [TotallyDisconnectedSpace X],
  TopologicalSpace.IsTopologicalBasis {s | IsClopen s}
-- Mathlib.Algebra.Homology.ShortComplex.QuasiIso
CategoryTheory.ShortComplex.quasiIso_iff_isIso_homologyMap' : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  {S₁ S₂ : CategoryTheory.ShortComplex C} [inst_2 : S₁.HasHomology] [inst_3 : S₂.HasHomology] (φ : S₁ ⟶ S₂)
  (h₁ : S₁.HomologyData) (h₂ : S₂.HomologyData),
  CategoryTheory.ShortComplex.QuasiIso φ ↔ CategoryTheory.IsIso (CategoryTheory.ShortComplex.homologyMap' φ h₁ h₂)
-- Mathlib.Data.Num.Basic
instDecidableEqNum.decEq : (x x_1 : Num) → Decidable (x = x_1)
-- Mathlib.Data.Int.Cast.Basic
Int.cast_sub : ∀ {R : Type u} [inst : AddGroupWithOne R] (m n : ℤ), ↑(m - n) = ↑m - ↑n
-- Std.Data.DHashMap.Lemmas
Std.DHashMap.Const.get!_alter : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} {β : Type v} {m : Std.DHashMap α fun x => β} [EquivBEq α]
  [LawfulHashable α] {k k' : α} [inst : Inhabited β] {f : Option β → Option β},
  Std.DHashMap.Const.get! (Std.DHashMap.Const.alter m k f) k' =
    if (k == k') = true then (f (Std.DHashMap.Const.get? m k)).get! else Std.DHashMap.Const.get! m k'
-- Mathlib.Algebra.Colimit.DirectLimit
DirectLimit.instSemifieldOfRingHomClass : {ι : 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 ι] →
                [Nonempty ι] →
                  [inst_5 : (i : ι) → Semifield (G i)] →
                    [∀ (i j : ι) (h : i ≤ j), RingHomClass (T h) (G i) (G j)] → Semifield (DirectLimit G f)
-- Mathlib.MeasureTheory.Integral.Lebesgue.Add
MeasureTheory.lintegral_const_mul'' : ∀ {α : Type u_1} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} (r : ENNReal) {f : α → ENNReal},
  AEMeasurable f μ → ∫⁻ (a : α), r * f a ∂μ = r * ∫⁻ (a : α), f a ∂μ
-- Lean.Data.Lsp.Extra
Lean.Lsp.RpcConnectParams.uri : Lean.Lsp.RpcConnectParams → Lean.Lsp.DocumentUri
-- Mathlib.MeasureTheory.Measure.Regular
Set.exists_isOpen_lt_add : ∀ {α : Type u_1} [inst : MeasurableSpace α] {μ : MeasureTheory.Measure α} [inst_1 : TopologicalSpace α] [μ.OuterRegular]
  (A : Set α), μ A ≠ ⊤ → ∀ {ε : ENNReal}, ε ≠ 0 → ∃ U ⊇ A, IsOpen U ∧ μ U < μ A + ε
-- Std.Data.HashSet.Raw
Std.HashSet.Raw.instUnionOfBEqOfHashable : {α : Type u} → [BEq α] → [Hashable α] → Union (Std.HashSet.Raw α)
-- Mathlib.CategoryTheory.MorphismProperty.Limits
CategoryTheory.MorphismProperty.colimitsOfShape.mk : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {W : CategoryTheory.MorphismProperty C} {J : Type u_1}
  [inst_1 : CategoryTheory.Category.{v_1, u_1} J] (X₁ X₂ : CategoryTheory.Functor J C)
  (c₁ : CategoryTheory.Limits.Cocone X₁) (c₂ : CategoryTheory.Limits.Cocone X₂)
  (h₁ : CategoryTheory.Limits.IsColimit c₁) (h₂ : CategoryTheory.Limits.IsColimit c₂) (f : X₁ ⟶ X₂),
  W.functorCategory J f → W.colimitsOfShape J (h₁.desc { pt := c₂.pt, ι := CategoryTheory.CategoryStruct.comp f c₂.ι })
-- Mathlib.MeasureTheory.Measure.MeasureSpace
MeasureTheory.Measure.eventually_cofinite : ∀ {α : Type u_1} {m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} {p : α → Prop},
  (∀ᶠ (x : α) in μ.cofinite, p x) ↔ μ {x | ¬p x} < ⊤
-- Mathlib.Logic.Basic
eq_iff_eq_cancel_right : ∀ {α : Sort u_1} {a b : α}, (∀ {c : α}, a = c ↔ b = c) ↔ a = b
-- Mathlib.NumberTheory.Dioph
Poly.neg_apply : ∀ {α : Type u_1} (f : Poly α) (x : α → ℕ), (-f) x = -f x
-- Mathlib.Algebra.Group.Pointwise.Finset.Basic
Finset.subtractionMonoid.eq_1 : ∀ {α : Type u_2} [inst : DecidableEq α] [inst_1 : SubtractionMonoid α],
  Finset.subtractionMonoid = Function.Injective.subtractionMonoid SetLike.coe ⋯ ⋯ ⋯ ⋯ ⋯ ⋯ ⋯
-- Batteries.Recycling.RBTree.Lemmas
_private.Batteries.Recycling.RBTree.Lemmas.0.RBTree.RBNode.setRed.match_1.eq_1 : ∀ {α : Type u_1} (motive : RBTree.RBNode α → Sort u_2) (c : RBTree.RBColor) (a : RBTree.RBNode α) (v : α)
  (b : RBTree.RBNode α)
  (h_1 :
    (c : RBTree.RBColor) →
      (a : RBTree.RBNode α) → (v : α) → (b : RBTree.RBNode α) → motive (RBTree.RBNode.node c a v b))
  (h_2 : Unit → motive RBTree.RBNode.nil),
  (match RBTree.RBNode.node c a v b with
    | RBTree.RBNode.node c a v b => h_1 c a v b
    | RBTree.RBNode.nil => h_2 ()) =
    h_1 c a v b
-- Mathlib.AlgebraicGeometry.IdealSheaf.Basic
AlgebraicGeometry.Scheme.ker_morphismRestrict_ideal : ∀ {X Y : AlgebraicGeometry.Scheme} (f : X.Hom Y) [AlgebraicGeometry.QuasiCompact f] (U : Y.Opens)
  (V : ↑(↑U).affineOpens),
  (AlgebraicGeometry.Scheme.Hom.ker (f ∣_ U)).ideal V =
    f.ker.ideal ⟨(AlgebraicGeometry.Scheme.Hom.opensFunctor U.ι).obj ↑V, ⋯⟩
-- Mathlib.Algebra.Group.Nat.Defs
Nat.nsmul_eq_mul : ∀ (m n : ℕ), m • n = m * n
-- Mathlib.NumberTheory.LSeries.Convolution
/-- The L-series of the (convolution) product of two `ℂ`-valued arithmetic functions `f` and `g`
equals the product of their L-series, assuming both L-series converge.  -/
ArithmeticFunction.LSeries_mul' : ∀ {f g : ArithmeticFunction ℂ} {s : ℂ},
  LSeriesSummable (fun n => f n) s →
    LSeriesSummable (fun n => g n) s →
      LSeries (fun n => (f * g) n) s = LSeries (fun n => f n) s * LSeries (fun n => g n) s
-- Mathlib.LinearAlgebra.AffineSpace.AffineSubspace.Defs
AffineSubspace.direction_sInf : ∀ {k : Type u_1} {V : Type u_2} {P : Type u_3} [inst : Ring k] [inst_1 : AddCommGroup V] [inst_2 : Module k V]
  [S : AddTorsor V P] (t : Set (AffineSubspace k P)), (sInf t).direction ≤ ⨅ s ∈ t, s.direction
-- Mathlib.Algebra.Category.MonCat.Limits
CommMonCat.forget_createsLimit : {J : Type v} →
  [inst : CategoryTheory.Category.{w, v} J] →
    (F : CategoryTheory.Functor J CommMonCat) →
      [Small.{u, max u v} ↑(F.comp (CategoryTheory.forget CommMonCat)).sections] →
        CategoryTheory.CreatesLimit F (CategoryTheory.forget CommMonCat)
-- Mathlib.Data.Nat.Choose.Multinomial
Multiset.multinomial_cons : ∀ (x : ℕ) (m : Multiset ℕ), (x ::ₘ m).multinomial = (x + m.sum).choose x * m.multinomial
-- Mathlib.Tactic.ComputeAsymptotics.Multiseries.Basis
Tactic.ComputeAsymptotics.BasisExtension.getBasis.eq_1 : Tactic.ComputeAsymptotics.BasisExtension.nil.getBasis = []
-- Mathlib.Algebra.Category.ModuleCat.Semi
LinearEquiv.toModuleIsoₛ_inv : ∀ {R : Type u} [inst : Semiring R] {X₁ X₂ : Type v} {g₁ : AddCommMonoid X₁} {g₂ : AddCommMonoid X₂} {m₁ : Module R X₁}
  {m₂ : Module R X₂} (e : X₁ ≃ₗ[R] X₂), e.toModuleIsoₛ.inv = SemimoduleCat.ofHom ↑e.symm
-- Mathlib.NumberTheory.Cyclotomic.CyclotomicCharacter
/-- Given a positive integer `n` and a field `L` containing `n` `n`th roots
of unity, `modularCyclotomicCharacter n` is a multiplicative homomorphism from the
automorphisms of `L` to `(ℤ/nℤ)ˣ`. It is uniquely characterised by the property that
`g(ζ)=ζ^(modularCyclotomicCharacter n g)` for `g` an automorphism of `L` and `ζ` any `n`th root
of unity.  -/
modularCyclotomicCharacter : (L : Type u) →
  [inst : CommRing L] → [IsDomain L] → {n : ℕ} → [NeZero n] → Nat.card ↥(rootsOfUnity n L) = n → (L ≃+* L) →* (ZMod n)ˣ
-- Init.Data.Nat.Control
_private.Init.Data.Nat.Control.0.Nat.allM.loop : {m : Type → Type u_1} → [Monad m] → (n : ℕ) → ((i : ℕ) → i < n → m Bool) → (i : ℕ) → i ≤ n → m Bool
-- Init.Grind.Order
Lean.Grind.Order.le_eq_true_k : ∀ {α : Type u_1} [inst : LE α] [inst_1 : LT α] [Std.LawfulOrderLT α] [inst_3 : Std.IsPreorder α]
  [inst_4 : Lean.Grind.Ring α] [Lean.Grind.OrderedRing α] {a : α} {k : ℤ}, Int.ble' 0 k = true → (a ≤ a + ↑k) = True
-- Mathlib.Analysis.BoxIntegral.Partition.Split
BoxIntegral.Box.splitUpper_def : ∀ {ι : Type u_1} {I : BoxIntegral.Box ι} [inst : DecidableEq ι] {i : ι} {x : ℝ}
  (h : x ∈ Set.Ioo (I.lower i) (I.upper i)) (h' : optParam (∀ (j : ι), Function.update I.lower i x j < I.upper j) ⋯),
  I.splitUpper i x = ↑{ lower := Function.update I.lower i x, upper := I.upper, lower_lt_upper := h' }
-- Mathlib.CategoryTheory.Limits.Shapes.BinaryBiproducts
/-- The associator isomorphism can be passed through a map by swapping the order.  -/
CategoryTheory.Limits.biprod.associator_natural_assoc : ∀ {C : Type uC} [inst : CategoryTheory.Category.{uC', uC} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  [inst_2 : CategoryTheory.Limits.HasBinaryBiproducts C] {U V W X Y Z : C} (f : U ⟶ X) (g : V ⟶ Y) (h : W ⟶ Z) {Z_1 : C}
  (h_1 : X ⊞ Y ⊞ Z ⟶ Z_1),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.biprod.map (CategoryTheory.Limits.biprod.map f g) h)
      (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.biprod.associator X Y Z).hom h_1) =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.biprod.associator U V W).hom
      (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.biprod.map f (CategoryTheory.Limits.biprod.map g h))
        h_1)
-- Mathlib.Analysis.Normed.Group.Defs
SeminormedAddCommGroup.ofAddDist.eq_1 : ∀ {E : Type u_5} [inst : Norm E] [inst_1 : AddCommGroup E] [inst_2 : PseudoMetricSpace E]
  (h₁ : ∀ (x : E), ‖x‖ = dist 0 x) (h₂ : ∀ (x y z : E), dist x y ≤ dist (z + x) (z + y)),
  SeminormedAddCommGroup.ofAddDist h₁ h₂ =
    { toNorm := (SeminormedAddGroup.ofAddDist h₁ h₂).toNorm,
      toAddGroup := (SeminormedAddGroup.ofAddDist h₁ h₂).toAddGroup, add_comm := ⋯,
      toPseudoMetricSpace := (SeminormedAddGroup.ofAddDist h₁ h₂).toPseudoMetricSpace, dist_eq := ⋯ }
-- Std.Data.DTreeMap.Internal.Lemmas
Std.DTreeMap.Internal.Impl.maxKeyD_insert! : ∀ {α : Type u} {β : α → Type v} {instOrd : Ord α} {t : Std.DTreeMap.Internal.Impl α β} [Std.TransOrd α],
  t.WF →
    ∀ {k : α} {v : β k} {fallback : α},
      (Std.DTreeMap.Internal.Impl.insert! k v t).maxKeyD fallback =
        t.maxKey?.elim k fun k' => if (compare k' k).isLE = true then k else k'
-- Std.Data.ExtDHashMap.Lemmas
Std.ExtDHashMap.Const.get?_filter_of_getKey?_eq_some : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} {β : Type v} {m : Std.ExtDHashMap α fun x => β} [inst : EquivBEq α]
  [inst_1 : LawfulHashable α] {f : α → β → Bool} {k k' : α},
  m.getKey? k = some k' →
    Std.ExtDHashMap.Const.get? (Std.ExtDHashMap.filter f m) k =
      Option.filter (fun x => f k' x) (Std.ExtDHashMap.Const.get? m k)
-- Init.Data.Array.Find
Array.findFinIdx?_eq_pmap_findIdx? : ∀ {α : Type u_1} {xs : Array α} {p : α → Bool},
  Array.findFinIdx? p xs = Option.pmap (fun i m => ⟨i, ⋯⟩) (Array.findIdx? p xs) ⋯
-- Mathlib.Algebra.Ring.Equiv
RingEquiv.coe_toMulEquiv : ∀ {R : Type u_4} {S : Type u_5} [inst : Mul R] [inst_1 : Mul S] [inst_2 : Add R] [inst_3 : Add S] (f : R ≃+* S),
  ⇑↑f = ⇑f
-- Batteries.Data.String.Lemmas
Substring.Raw.ValidFor.all : ∀ {l m r : List Char} (f : Char → Bool) {s : Substring.Raw},
  Substring.Raw.ValidFor l m r s → Substring.Raw.Legacy.all s f = m.all f
-- Mathlib.Data.Fintype.Card
/-- We can inflate a set `s` to any bigger size.  -/
Finset.exists_superset_card_eq : ∀ {α : Type u_1} [inst : Fintype α] {n : ℕ} {s : Finset α}, s.card ≤ n → n ≤ Fintype.card α → ∃ t, s ⊆ t ∧ t.card = n
-- Mathlib.Analysis.Normed.Module.HahnBanach
/-- Variant of Hahn-Banach, eliminating the hypothesis that `x` be nonzero, but only ensuring that
the dual element has norm at most `1` (this cannot be improved for the trivial
vector space).  -/
exists_dual_vector'' : ∀ (𝕜 : Type v) [inst : RCLike 𝕜] {E : Type u} [inst_1 : SeminormedAddCommGroup E] [inst_2 : NormedSpace 𝕜 E] (x : E),
  ∃ g, ‖g‖ ≤ 1 ∧ g x = ↑‖x‖
-- Std.Data.ExtDTreeMap.Lemmas
Std.ExtDTreeMap.get_alter_self : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t : Std.ExtDTreeMap α β cmp} [inst : Std.TransCmp cmp]
  [inst_1 : Std.LawfulEqCmp cmp] {k : α} {f : Option (β k) → Option (β k)} {hc : k ∈ t.alter k f},
  (t.alter k f).get k hc = (f (t.get? k)).get ⋯
-- Mathlib.CategoryTheory.ComposableArrows.Four
CategoryTheory.ComposableArrows.fourδ₄Toδ₃_app_two : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] {i₀ i₁ i₂ i₃ i₄ : C} (f₁ : i₀ ⟶ i₁) (f₂ : i₁ ⟶ i₂)
  (f₃ : i₂ ⟶ i₃) (f₄ : i₃ ⟶ i₄) (f₃₄ : i₂ ⟶ i₄) (h₃₄ : CategoryTheory.CategoryStruct.comp f₃ f₄ = f₃₄),
  (CategoryTheory.ComposableArrows.fourδ₄Toδ₃ f₁ f₂ f₃ f₄ f₃₄ h₃₄).app 2 =
    CategoryTheory.CategoryStruct.id ((CategoryTheory.ComposableArrows.mk₃ f₁ f₂ f₃).obj 2)
-- Init.Data.Range.Polymorphic.PRange
Std.Rci.mk.injEq : ∀ {α : Type u} (lower lower_1 : α), (lower...* = lower_1...*) = (lower = lower_1)
-- Mathlib.Topology.Algebra.Algebra.Equiv
/-- `ContinuousAlgEquivClass F R A B` states that `F` is a type of topological algebra
structure-preserving equivalences. You should extend this class when you
extend `ContinuousAlgEquiv`.
 -/
ContinuousAlgEquivClass : (F : Type u_1) →
  (R : outParam (Type u_2)) →
    (A : outParam (Type u_3)) →
      (B : outParam (Type u_4)) →
        [inst : CommSemiring R] →
          [inst_1 : Semiring A] →
            [TopologicalSpace A] →
              [inst_3 : Semiring B] → [TopologicalSpace B] → [Algebra R A] → [Algebra R B] → [EquivLike F A B] → Prop
-- Mathlib.SetTheory.Ordinal.CantorNormalForm
_private.Mathlib.SetTheory.Ordinal.CantorNormalForm.0.Ordinal.CNF.eval.eq_1 : ∀ (b : Ordinal.{u_1}) (f : Ordinal.{u_1} →₀ Ordinal.{u_1}),
  Ordinal.CNF.eval b f = List.foldr (fun p r => b ^ p * f p + r) 0 (f.support.sort fun x1 x2 => x1 ≥ x2)
-- Mathlib.Algebra.Category.AlgCat.Basic
AlgCat.comp_apply : ∀ (R : Type u) [inst : CommRing R] {A B C : AlgCat R} (f : A ⟶ B) (g : B ⟶ C) (a : ↑A),
  (CategoryTheory.ConcreteCategory.hom (CategoryTheory.CategoryStruct.comp f g)) a =
    (CategoryTheory.ConcreteCategory.hom g) ((CategoryTheory.ConcreteCategory.hom f) a)
-- Mathlib.Algebra.Group.Equiv.Defs
AddMonoidHom.toAddEquiv_apply : ∀ {M : Type u_4} {N : Type u_5} [inst : AddZeroClass M] [inst_1 : AddZeroClass N] (f : M →+ N) (g : N →+ M)
  (h₁ : g.comp f = AddMonoidHom.id M) (h₂ : f.comp g = AddMonoidHom.id N), ⇑(f.toAddEquiv g h₁ h₂) = ⇑f
-- Mathlib.Probability.IdentDistrib
ProbabilityTheory.IdentDistrib.ae_snd : ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} [inst : MeasurableSpace α] [inst_1 : MeasurableSpace β]
  [inst_2 : MeasurableSpace γ] {μ : MeasureTheory.Measure α} {ν : MeasureTheory.Measure β} {f : α → γ} {g : β → γ},
  ProbabilityTheory.IdentDistrib f g μ ν →
    ∀ {p : γ → Prop}, MeasurableSet {x | p x} → (∀ᵐ (x : α) ∂μ, p (f x)) → ∀ᵐ (x : β) ∂ν, p (g x)
-- Lean.Elab.PreDefinition.EqnsUtils
Lean.Elab.Eqns.simpMatch? : Lean.MVarId → Lean.MetaM (Option Lean.MVarId)
-- Mathlib.CategoryTheory.Bicategory.Free
CategoryTheory.FreeBicategory.Rel.below.whisker_exchange : ∀ {B : Type u} [inst : Quiver B]
  {motive :
    {a b : CategoryTheory.FreeBicategory B} →
      {f g : a ⟶ b} →
        (a_1 a_2 : CategoryTheory.FreeBicategory.Hom₂ f g) → CategoryTheory.FreeBicategory.Rel a_1 a_2 → Prop}
  {a b c : B} {f g : CategoryTheory.FreeBicategory.Hom a b} {h i : CategoryTheory.FreeBicategory.Hom b c}
  (η : CategoryTheory.FreeBicategory.Hom₂ f g) (θ : CategoryTheory.FreeBicategory.Hom₂ h i),
  CategoryTheory.FreeBicategory.Rel.below ⋯
-- Mathlib.Algebra.Polynomial.Degree.TrailingDegree
Polynomial.trailingDegree_eq_zero : ∀ {R : Type u} [inst : Semiring R] {p : Polynomial R}, p.trailingDegree = 0 ↔ p.coeff 0 ≠ 0
-- Lean.Elab.PreDefinition.Structural.Basic
/-- The number of indices in the array.
 -/
Lean.Elab.Structural.Positions.numIndices : Lean.Elab.Structural.Positions → ℕ
-- Mathlib.CategoryTheory.ObjectProperty.Local
CategoryTheory.MorphismProperty.isColocal_single_iff_bijective : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {X Y : C} (f : X ⟶ Y) (Z : C),
  (CategoryTheory.MorphismProperty.single f).isColocal Z ↔
    Function.Bijective fun g => CategoryTheory.CategoryStruct.comp g f
-- Mathlib.RingTheory.MvPowerSeries.Order
MvPowerSeries.ne_zero_iff_order_finite : ∀ {σ : Type u_1} {R : Type u_2} [inst : Semiring R] {f : MvPowerSeries σ R}, f ≠ 0 ↔ ↑f.order.toNat = f.order
-- Mathlib.Algebra.Group.Submonoid.Operations
AddSubmonoid.inclusion_injective : ∀ {M : Type u_1} [inst : AddZeroClass M] {S T : AddSubmonoid M} (h : S ≤ T),
  Function.Injective ⇑(AddSubmonoid.inclusion h)
-- Mathlib.Data.Nat.ModEq
/-- **Alias** of the forward direction of `Nat.modEq_iff_dvd`. -/
Nat.ModEq.dvd : ∀ {n a b : ℕ}, a ≡ b [MOD n] → ↑n ∣ ↑b - ↑a
-- Std.Data.ExtDHashMap.Lemmas
Std.ExtDHashMap.Const.getKey!_ofList_of_contains_eq_false : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} {β : Type v} [inst : EquivBEq α] [inst_1 : LawfulHashable α]
  [inst_2 : Inhabited α] {l : List (α × β)} {k : α},
  (List.map Prod.fst l).contains k = false → (Std.ExtDHashMap.Const.ofList l).getKey! k = default
-- Mathlib.Geometry.Convex.ConvexSpace.Defs
/-- Take a convex combination with the given probability distribution over points.  -/
Convexity.ConvexSpace.sConvexComb : {R : Type u} →
  {M : Type v} →
    [inst₁ : PartialOrder R] →
      [inst₂ : Semiring R] →
        [inst₃ : IsStrictOrderedRing R] → [self : Convexity.ConvexSpace R M] → Convexity.StdSimplex R M → M
-- Init.Data.Format.Syntax
Lean.Syntax.instToStringTSyntax : {k : Lean.SyntaxNodeKinds} → ToString (Lean.TSyntax k)
-- Std.Data.DTreeMap.Internal.WF.Lemmas
Std.DTreeMap.Internal.Impl.size_eq_length : ∀ {α : Type u} {β : α → Type v} (t : Std.DTreeMap.Internal.Impl α β), t.Balanced → t.size = t.toListModel.length
-- Mathlib.Order.BourbakiWitt
NonemptyChain.mk.injEq : ∀ {α : Type u_4} [inst : LE α] (carrier : Set α) (Nonempty' : carrier.Nonempty)
  (isChain' : IsChain (fun x1 x2 => x1 ≤ x2) carrier) (carrier_1 : Set α) (Nonempty'_1 : carrier_1.Nonempty)
  (isChain'_1 : IsChain (fun x1 x2 => x1 ≤ x2) carrier_1),
  ({ carrier := carrier, Nonempty' := Nonempty', isChain' := isChain' } =
      { carrier := carrier_1, Nonempty' := Nonempty'_1, isChain' := isChain'_1 }) =
    (carrier = carrier_1)
-- Mathlib.Analysis.Distribution.TemperedDistribution
TemperedDistribution.instFourierTransform : {E : Type u_3} →
  {F : Type u_4} →
    [inst : NormedAddCommGroup E] →
      [inst_1 : InnerProductSpace ℝ E] →
        [FiniteDimensional ℝ E] →
          [inst_3 : MeasurableSpace E] →
            [BorelSpace E] →
              [inst_5 : AddCommGroup F] →
                [inst_6 : Module ℂ F] →
                  [inst_7 : TopologicalSpace F] →
                    [IsTopologicalAddGroup F] →
                      [ContinuousConstSMul ℂ F] → FourierTransform (TemperedDistribution E F) (TemperedDistribution E F)
-- Mathlib.MeasureTheory.Function.UnifTight
MeasureTheory.UnifTight.neg : ∀ {α : Type u_1} {β : Type u_2} {ι : Type u_3} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α}
  [inst : NormedAddCommGroup β] {f : ι → α → β} {p : ENNReal},
  MeasureTheory.UnifTight f p μ → MeasureTheory.UnifTight (-f) p μ
-- Mathlib.FieldTheory.RatFunc.Luroth
_private.Mathlib.FieldTheory.RatFunc.Luroth.0.RatFunc.Luroth.m_le_swap_Φ_natDegree : ∀ {K : Type u_1} [inst : Field K] {E : IntermediateField K (RatFunc K)},
  E ≠ ⊥ → RatFunc.Luroth.m✝ E ≤ (Polynomial.Bivariate.swap (RatFunc.Luroth.Φ✝ E)).natDegree
-- Mathlib.Algebra.Order.Floor.Semifield
Nat.ceil_lt_mul : ∀ {K : Type u_2} [inst : Field K] [inst_1 : LinearOrder K] [IsOrderedRing K] [inst_3 : FloorSemiring K] {a b : K},
  1 < b → ↑⌈(b - 1)⁻¹⌉₊ / b < a → ↑⌈a⌉₊ < b * a
-- Mathlib.CategoryTheory.Limits.Final
CategoryTheory.Functor.Final.coconesEquiv_functor : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  (F : CategoryTheory.Functor C D) [inst_2 : F.Final] {E : Type u₃} [inst_3 : CategoryTheory.Category.{v₃, u₃} E]
  (G : CategoryTheory.Functor D E),
  (CategoryTheory.Functor.Final.coconesEquiv F G).functor = CategoryTheory.Functor.Final.extendCocone
-- Mathlib.Algebra.Group.Hom.Defs
/-- The monoid of endomorphisms.  -/
AddMonoid.End : (M : Type u_4) → [AddZero M] → Type u_4
-- Mathlib.AlgebraicGeometry.EllipticCurve.VariableChange
WeierstrassCurve.VariableChange.ext : ∀ {R : Type u} {inst : CommRing R} {x y : WeierstrassCurve.VariableChange R},
  x.u = y.u → x.r = y.r → x.s = y.s → x.t = y.t → x = y
-- Std.Data.DTreeMap.Internal.Model
_private.Std.Data.DTreeMap.Internal.Model.0.Std.DTreeMap.Internal.Cell.get?.match_1.eq_2 : ∀ {α : Type u_2} {β : α → Type u_1} (motive : Option ((a : α) × β a) → Sort u_3) (p : (a : α) × β a)
  (h_1 : some p = none → motive none) (h_2 : (p_1 : (a : α) × β a) → some p = some p_1 → motive (some p_1)),
  (match h : some p with
    | none => h_1 h
    | some p_1 => h_2 p_1 h) =
    h_2 p ⋯
-- Mathlib.MeasureTheory.Integral.Pi
MeasureTheory.integral_comp_eval : ∀ {ι : Type u_2} [inst : Fintype ι] {X : ι → Type u_3} {mX : (i : ι) → MeasurableSpace (X i)}
  {μ : (i : ι) → MeasureTheory.Measure (X i)} {E : Type u_4} [inst_1 : NormedAddCommGroup E] [inst_2 : NormedSpace ℝ E]
  [∀ (i : ι), MeasureTheory.IsProbabilityMeasure (μ i)] {i : ι} {f : X i → E},
  MeasureTheory.AEStronglyMeasurable f (μ i) →
    ∫ (x : (i : ι) → X i), f (x i) ∂MeasureTheory.Measure.pi μ = ∫ (x : X i), f x ∂μ i
-- Mathlib.Data.Finset.Pi
Finset.Pi.cons_same : ∀ {α : Type u_1} {δ : α → Sort v} [inst : DecidableEq α] (s : Finset α) (a : α) (b : δ a) (f : (a : α) → a ∈ s → δ a)
  (h : a ∈ insert a s), Finset.Pi.cons s a b f a h = b
-- Std.Sat.AIG.Basic
Std.Sat.AIG.Fanin.ofRaw.inj : ∀ {val val_1 : ℕ}, { val := val } = { val := val_1 } → val = val_1
-- Mathlib.Order.Max
/-- For each term `a`, there is some strictly smaller `b`.  -/
NoMinOrder.exists_lt : ∀ {α : Type u_3} {inst : LT α} [self : NoMinOrder α] (a : α), ∃ b, b < a