mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Analysis.BoxIntegral.Basic
BoxIntegral.Integrable.add : ∀ {ι : Type u} {E : Type v} {F : Type w} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E]
  [inst_2 : NormedAddCommGroup F] [inst_3 : NormedSpace ℝ F] {I : BoxIntegral.Box ι} [inst_4 : Fintype ι]
  {l : BoxIntegral.IntegrationParams} {f g : (ι → ℝ) → E} {vol : BoxIntegral.BoxAdditiveMap ι (E →L[ℝ] F) ⊤},
  BoxIntegral.Integrable I l f vol → BoxIntegral.Integrable I l g vol → BoxIntegral.Integrable I l (f + g) vol
-- Mathlib.Analysis.RCLike.TangentCone
UniqueDiffOn.of_real : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] [h𝕜 : IsRCLikeNormedField 𝕜] {E : Type u_2}
  [inst_1 : NormedAddCommGroup E] [inst_2 : NormedSpace 𝕜 E] [inst_3 : NormedSpace ℝ E] {s : Set E},
  UniqueDiffOn ℝ s → UniqueDiffOn 𝕜 s
-- Std.Tactic.BVDecide.LRAT.Parser
Std.Tactic.BVDecide.LRAT.Parser.Binary.parseRatHints : Std.Internal.Parsec.ByteArray.Parser (Array (ℕ × Array ℕ))
-- Mathlib.Analysis.CStarAlgebra.Module.Defs
CStarModule.inner_op_smul_right : ∀ {A : Type u_1} {E : Type u_2} {inst : NonUnitalSemiring A} {inst_1 : StarRing A} {inst_2 : Module ℂ A}
  {inst_3 : AddCommGroup E} {inst_4 : Module ℂ E} {inst_5 : PartialOrder A} {inst_6 : SMul A E} {inst_7 : Norm A}
  {inst_8 : Norm E} [self : CStarModule A E] {a : A} {x y : E}, inner A x (a • y) = a * inner A x y
-- Mathlib.MeasureTheory.Integral.SetToL1
MeasureTheory.L1.SimpleFunc.setToL1S_const : ∀ {α : Type u_1} {E : Type u_2} {F : Type u_3} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E]
  [inst_2 : NormedAddCommGroup F] [inst_3 : NormedSpace ℝ F] {m : MeasurableSpace α} {μ : MeasureTheory.Measure α}
  [inst_4 : MeasureTheory.IsFiniteMeasure μ] {T : Set α → E →L[ℝ] F},
  (∀ (s : Set α), MeasurableSet s → μ s = 0 → T s = 0) →
    MeasureTheory.FinMeasAdditive μ T →
      ∀ (x : E),
        MeasureTheory.L1.SimpleFunc.setToL1S T (MeasureTheory.Lp.simpleFunc.indicatorConst 1 ⋯ ⋯ x) = (T Set.univ) x
-- Mathlib.Analysis.Complex.Circle
Circle.coe_exp : ∀ (t : ℝ), ↑(Circle.exp t) = Complex.exp (↑t * Complex.I)
-- Mathlib.Topology.Algebra.SeparationQuotient.Basic
SeparationQuotient.instGroup.eq_1 : ∀ {G : Type u_1} [inst : TopologicalSpace G] [inst_1 : Group G] [inst_2 : IsTopologicalGroup G],
  SeparationQuotient.instGroup =
    { toMonoid := SeparationQuotient.instMonoid, toInv := SeparationQuotient.instInv,
      toDiv := SeparationQuotient.instDiv, toZPow := ZPow.ofPow, div_eq_mul_inv := ⋯, zpow_zero' := ⋯, zpow_succ' := ⋯,
      zpow_neg' := ⋯, inv_mul_cancel := ⋯ }
-- Std.Time.Date.Basic
Std.Time.instHAddOffsetOffset_22 : HAdd Std.Time.Minute.Offset Std.Time.Day.Offset Std.Time.Minute.Offset
-- Mathlib.GroupTheory.GroupAction.MultiplePrimitivity
MulAction.isMultiplyPreprimitive_iff : ∀ (M : Type u_1) (α : Type u_2) [inst : Group M] [inst_1 : MulAction M α] (n : ℕ),
  MulAction.IsMultiplyPreprimitive M α n ↔
    MulAction.IsMultiplyPretransitive M α n ∧
      ∀ {s : Set α},
        s.encard + 1 = ↑n → MulAction.IsPreprimitive ↥(fixingSubgroup M s) ↥(SubMulAction.ofFixingSubgroup M s)
-- Init.NotationExtra
/-- Unexpander for the `{ x }` notation.  -/
Lean.singletonUnexpander : Lean.PrettyPrinter.Unexpander
-- Lean.Meta.Tactic.Grind.Arith.Cutsat.Types
/-- Next unique id for a constraint.  -/
Lean.Meta.Grind.Arith.Cutsat.State.nextCnstrId : Lean.Meta.Grind.Arith.Cutsat.State → ℕ
-- Mathlib.Data.Rel
SetRel.image_eq_biUnion : ∀ {α : Type u_1} {β : Type u_2} {R : SetRel α β} {s : Set α}, R.image s = ⋃ x ∈ s, {y | (x, y) ∈ R}
-- Lean.Data.JsonRpc
Lean.JsonRpc.RequestID.null : Lean.JsonRpc.RequestID
-- Std.Internal.Do.WP.Lemmas
Std.Internal.Do.WPMonad.le_wp_get_StateT_apply : ∀ {Pred : Type u_1} {EPred : Type u_2} {m : Type u → Type v} [inst : Monad m] [inst_1 : Std.Internal.Do.Assertion Pred]
  [inst_2 : Std.Internal.Do.Assertion EPred] [inst_3 : Std.Internal.Do.WPMonad m Pred EPred] {σ : Type u}
  (post : σ → σ → Pred) (epost : EPred),
  Lean.Order.PartialOrder.rel (fun s => post s s) (Std.Internal.Do.wp MonadStateOf.get post epost)
-- Mathlib.CategoryTheory.Join.Basic
CategoryTheory.Join.mapIsoWhiskerLeft_hom_app : ∀ {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] {E' : Type u₄}
  [inst_3 : CategoryTheory.Category.{v₄, u₄} E'] (H : CategoryTheory.Functor C E) {Fᵣ Gᵣ : CategoryTheory.Functor D E'}
  (α : Fᵣ ≅ Gᵣ) (x : CategoryTheory.Join C D),
  (CategoryTheory.Join.mapIsoWhiskerLeft H α).hom.app x =
    match x with
    | CategoryTheory.Join.left x => CategoryTheory.CategoryStruct.id (CategoryTheory.Join.left (H.obj x))
    | CategoryTheory.Join.right x => (CategoryTheory.Join.inclRight E E').map (α.hom.app x)
-- Mathlib.Algebra.Group.Submonoid.Units
AddSubgroup.addUnit_mem_of_mem_ofAddUnits : ∀ {M : Type u_1} [inst : AddMonoid M] (S : AddSubgroup (AddUnits M)) {x : M} {h₁ : IsAddUnit x},
  x ∈ S.ofAddUnits → h₁.addUnit ∈ S
-- Mathlib.Algebra.Order.BigOperators.Expect
Finset.exists_lt_of_lt_expect : ∀ {ι : Type u_1} {α : Type u_2} [inst : AddCommMonoid α] [inst_1 : LinearOrder α] [IsOrderedAddMonoid α]
  [inst_3 : Module ℚ≥0 α] [PosSMulMono ℚ≥0 α] {s : Finset ι} {f : ι → α} {a : α},
  s.Nonempty → (a < s.expect fun i => f i) → ∃ x ∈ s, a < f x
-- Std.Data.DHashMap.RawLemmas
Std.DHashMap.Raw.size_le_size_alter : ∀ {α : Type u} {β : α → Type v} [inst : BEq α] [inst_1 : Hashable α] {m : Std.DHashMap.Raw α β} [inst_2 : LawfulBEq α]
  {k : α} {f : Option (β k) → Option (β k)}, m.WF → m.size - 1 ≤ (m.alter k f).size
-- Lean.Environment
_private.Lean.Environment.0.Lean.readIRPartsOfMod.unsafe_impl_2 : System.FilePath → IO (Lean.ModuleData × Lean.CompactedRegion)
-- Lean.Meta.WrapInstance
Lean.Meta.backward.inferInstanceAs.wrap.instances : Lean.Option Bool
-- Mathlib.Algebra.Polynomial.Bivariate
Polynomial.aevalAevalEquiv_symm_apply : ∀ (R : Type u_1) (A : Type u_2) [inst : CommSemiring R] [inst_1 : CommSemiring A] [inst_2 : Algebra R A]
  (f : Polynomial (Polynomial R) →ₐ[R] A),
  (Polynomial.aevalAevalEquiv R A).symm f = (f (Polynomial.C Polynomial.X), f Polynomial.X)
-- Mathlib.Algebra.Lie.Subalgebra
/-- An `L`-equivariant map of Lie modules `M → N` is `L'`-equivariant for any Lie subalgebra
`L' ⊆ L`.  -/
LieModuleHom.restrictLie : {R : Type u} →
  {L : Type v} →
    [inst : CommRing R] →
      [inst_1 : LieRing L] →
        [inst_2 : LieAlgebra R L] →
          {M : Type w} →
            [inst_3 : AddCommGroup M] →
              [inst_4 : LieRingModule L M] →
                {N : Type w₁} →
                  [inst_5 : AddCommGroup N] →
                    [inst_6 : LieRingModule L N] →
                      [inst_7 : Module R N] →
                        [inst_8 : Module R M] → (M →ₗ⁅R,L⁆ N) → (L' : LieSubalgebra R L) → M →ₗ⁅R,↥L'⁆ N
-- Mathlib.CategoryTheory.Monoidal.CommGrp_
CategoryTheory.CommGrp.comp_hom : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.CartesianMonoidalCategory C]
  [inst_2 : CategoryTheory.BraidedCategory C] {R S T : CategoryTheory.CommGrp C} (f : R ⟶ S) (g : S ⟶ T),
  (CategoryTheory.CategoryStruct.comp f g).hom = CategoryTheory.CategoryStruct.comp f.hom g.hom
-- Mathlib.Algebra.Group.Pointwise.Finset.Basic
/-- Lift a `MulHom` to `Finset` via `image`.  -/
Finset.imageMulHom : {F : Type u_1} →
  {α : Type u_2} →
    {β : Type u_3} →
      [inst : DecidableEq α] →
        [inst_1 : Mul α] →
          [inst_2 : Mul β] →
            [inst_3 : FunLike F α β] → [MulHomClass F α β] → F → [inst_5 : DecidableEq β] → Finset α →ₙ* Finset β
-- Mathlib.Analysis.Complex.Cardinality
/-- The complex numbers are not countable.  -/
not_countable_complex : ¬Set.univ.Countable
-- Mathlib.RingTheory.Valuation.Discrete.Basic
/-- This is Chapter I, Section 1, Proposition 1 in Serre's Local Fields  -/
Valuation.valuationSubring_isDiscreteValuationRing : ∀ {Γ : Type u_1} [inst : LinearOrderedCommGroupWithZero Γ] {K : Type u_2} [inst_1 : Field K] (v : Valuation K Γ)
  [IsCyclic ↥(MonoidWithZeroHom.ofClass v).valueGroup] [Nontrivial ↥(MonoidWithZeroHom.ofClass v).valueGroup],
  IsDiscreteValuationRing ↥v.valuationSubring
-- Mathlib.CategoryTheory.Presentable.CardinalDirectedPoset
CategoryTheory.CardinalDirectedPoset.instNonemptySubtypeSetCarrierObjPartOrdEmbIsCardinalFilteredWithTopPropSetWithTop : ∀ {κ : Cardinal.{u}} [inst : Fact κ.IsRegular] (J : CategoryTheory.CardinalDirectedPoset κ) (κ' : Cardinal.{u})
  [inst_1 : Fact κ'.IsRegular], Nonempty (Subtype (J.PropSetWithTop κ'))
-- Mathlib.Order.CompleteLattice.MulticoequalizerDiagram
Lattice.BicartSq.inf_eq : ∀ {T : Type u} {x₁ x₂ x₃ x₄ : T} [inst : Lattice T], Lattice.BicartSq x₁ x₂ x₃ x₄ → x₂ ⊓ x₃ = x₁
-- Init.Data.Array.Monadic
Array.toList_flatMapM : ∀ {m : Type u_1 → Type u_2} {α : Type u_3} {β : Type u_1} [inst : Monad m] [LawfulMonad m] {xs : Array α}
  {f : α → m (Array β)}, Array.toList <$> Array.flatMapM f xs = List.flatMapM (fun a => Array.toList <$> f a) xs.toList
-- Mathlib.RingTheory.Ideal.Maps
Submodule.annihilator_bot : ∀ {R : Type u_1} {M : Type u_2} [inst : Semiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M], ⊥.annihilator = ⊤
-- Mathlib.AlgebraicTopology.SimplicialSet.Op
SSet.δ_opObjEquiv : ∀ (X : SSet) {n : ℕ} (i : Fin (n + 2)) (x : X.op.obj (Opposite.op { len := n + 1 })),
  (CategoryTheory.ConcreteCategory.hom (CategoryTheory.SimplicialObject.δ X i)) (SSet.opObjEquiv x) =
    SSet.opObjEquiv ((CategoryTheory.ConcreteCategory.hom (CategoryTheory.SimplicialObject.δ X.op i.rev)) x)
-- Mathlib.Data.Num.Basic
instReprZNum : Repr ZNum
-- Mathlib.CategoryTheory.Preadditive.Basic
CategoryTheory.Preadditive.smul_iso_hom : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Preadditive C] {X Y : C}
  (a : ℤˣ) (e : X ≅ Y), (a • e).hom = a • e.hom
-- Mathlib.Data.Seq.Basic
Stream'.Seq.destruct.eq_1 : ∀ {α : Type u} (s : Stream'.Seq α), s.destruct = (fun a' => (a', s.tail)) <$> s.get? 0
-- Mathlib.AlgebraicTopology.SimplicialObject.Basic
CategoryTheory.CosimplicialObject.whiskering_map_app_app : ∀ (C : Type u) [inst : CategoryTheory.Category.{v, u} C] (D : Type u_1) [inst_1 : CategoryTheory.Category.{v_1, u_1} D]
  {X Y : CategoryTheory.Functor C D} (τ : X ⟶ Y) (F : CategoryTheory.Functor SimplexCategory C) (c : SimplexCategory),
  (((CategoryTheory.CosimplicialObject.whiskering C D).map τ).app F).app c = τ.app (F.obj c)
-- Lean.Elab.InfoTree.Types
Lean.Elab.instInhabitedInfoState.default : Lean.Elab.InfoState
-- Init.Data.BitVec.Lemmas
BitVec.udiv.eq_1 : ∀ {n : ℕ} (x y : BitVec n), x.udiv y = (x.toNat / y.toNat)#'⋯
-- Mathlib.MeasureTheory.Measure.Restrict
MeasureTheory.Measure.restrict_univ : ∀ {α : Type u_2} {m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α}, μ.restrict Set.univ = μ
-- Mathlib.Order.Filter.Defs
Filter.mp_mem : ∀ {α : Type u_1} {f : Filter α} {s t : Set α}, s ∈ f → {x | x ∈ s → x ∈ t} ∈ f → t ∈ f
-- Mathlib.Probability.Martingale.Convergence
MeasureTheory.Submartingale.upcrossings_ae_lt_top : ∀ {Ω : Type u_1} {m0 : MeasurableSpace Ω} {μ : MeasureTheory.Measure Ω} {ℱ : MeasureTheory.Filtration ℕ m0}
  {f : ℕ → Ω → ℝ} {R : NNReal} [MeasureTheory.IsFiniteMeasure μ],
  MeasureTheory.Submartingale f ℱ μ →
    (∀ (n : ℕ), MeasureTheory.eLpNorm (f n) 1 μ ≤ ↑R) →
      ∀ᵐ (ω : Ω) ∂μ, ∀ (a b : ℚ), a < b → MeasureTheory.upcrossings (↑a) (↑b) f ω < ⊤
-- Mathlib.MeasureTheory.Function.L1Space.Integrable
/-- A non-quantitative version of Markov inequality for integrable functions: the measure of points
where `‖f x‖ₑ ≥ ε` is finite for all positive `ε`.  -/
MeasureTheory.Integrable.measure_enorm_ge_lt_top : ∀ {α : Type u_1} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} {E : Type u_8} [inst : TopologicalSpace E]
  [inst_1 : ContinuousENorm E] {f : α → E},
  MeasureTheory.Integrable f μ → ∀ {ε : ENNReal}, 0 < ε → ε ≠ ⊤ → μ {x | ε ≤ ‖f x‖ₑ} < ⊤
-- Mathlib.NumberTheory.ArithmeticFunction.Defs
ArithmeticFunction.instCommRing : {R : Type u_1} → [inst : CommRing R] → CommRing (ArithmeticFunction R)
-- Lean.Meta.Tactic.Grind.Arith.Linear.Types
Lean.Meta.Grind.Arith.Linear.UnsatProof.lt.sizeOf_spec : ∀ (c : Lean.Meta.Grind.Arith.Linear.IneqCnstr), sizeOf (Lean.Meta.Grind.Arith.Linear.UnsatProof.lt c) = 1 + sizeOf c
-- Mathlib.RingTheory.Derivation.Lie
Derivation.instLieRingModule : {R : Type u_1} →
  [inst : CommRing R] →
    {A : Type u_2} → [inst_1 : CommRing A] → [inst_2 : Algebra R A] → LieRingModule (Derivation R A A) A
-- Mathlib.Probability.Independence.Conditional
ProbabilityTheory.iCondIndep_iff : ∀ {Ω : Type u_1} {ι : Type u_2} (m' : MeasurableSpace Ω) {mΩ : MeasurableSpace Ω} [inst : StandardBorelSpace Ω]
  (hm' : m' ≤ mΩ) (m : ι → MeasurableSpace Ω),
  (∀ (i : ι), m i ≤ mΩ) →
    ∀ (μ : MeasureTheory.Measure Ω) [inst_1 : MeasureTheory.IsFiniteMeasure μ],
      ProbabilityTheory.iCondIndep m' hm' m μ ↔
        ∀ (s : Finset ι) {f : ι → Set Ω},
          (∀ i ∈ s, MeasurableSet (f i)) →
            μ[(⋂ i ∈ s, f i).indicator fun ω => 1 | m'] =ᵐ[μ] ∏ i ∈ s, μ[(f i).indicator fun ω => 1 | m']
-- Mathlib.Tactic.Translate.Core
/-- If `allowAutoName` is `false` (default) then
we check whether the given name can be auto-generated.  -/
Mathlib.Tactic.Translate.Config.allowAutoName : Mathlib.Tactic.Translate.Config → Bool
-- Mathlib.RepresentationTheory.Homological.GroupCohomology.LowDegree
groupCohomology.π_comp_H0Iso_hom_assoc : ∀ {k G : Type u} [inst : CommRing k] [inst_1 : Group G] (A : Rep.{u, u, u} k G) {Z : ModuleCat k}
  (h : ModuleCat.of k ↥A.ρ.invariants ⟶ Z),
  CategoryTheory.CategoryStruct.comp (groupCohomology.π A 0)
      (CategoryTheory.CategoryStruct.comp (groupCohomology.H0Iso A).hom h) =
    CategoryTheory.CategoryStruct.comp (groupCohomology.cocyclesIso₀ A).hom h
-- Mathlib.Topology.Algebra.ContinuousMonoidHom
ContinuousAddMonoidHom.add.eq_1 : ∀ (E : Type u_6) [inst : AddCommMonoid E] [inst_1 : TopologicalSpace E] [inst_2 : ContinuousAdd E],
  ContinuousAddMonoidHom.add E = { toAddMonoidHom := addAddMonoidHom, continuous_toFun := ⋯ }
-- Init.Data.Ord.UInt
UInt8.instOrd : Ord UInt8
-- Mathlib.Topology.Homotopy.HSpaces
/-- The binary operation `hmul` on an `H`-space  -/
HSpaces.«term_⋀_» : Lean.TrailingParserDescr
-- Mathlib.Data.Multiset.Defs
/-- Another way of expressing `strongInductionOn`: the `(<)` relation is well-founded.  -/
Multiset.instWellFoundedLT : ∀ {α : Type u_1}, WellFoundedLT (Multiset α)
-- Mathlib.CategoryTheory.Linear.Basic
CategoryTheory.Linear.mk : {R : Type w} →
  [inst : Semiring R] →
    {C : Type u} →
      [inst_1 : CategoryTheory.Category.{v, u} C] →
        [inst_2 : CategoryTheory.Preadditive C] →
          (homModule : autoParam ((X Y : C) → Module R (X ⟶ Y)) CategoryTheory.Linear.homModule._autoParam) →
            autoParam
                (∀ (X Y Z : C) (r : R) (f : X ⟶ Y) (g : Y ⟶ Z),
                  CategoryTheory.CategoryStruct.comp (r • f) g = r • CategoryTheory.CategoryStruct.comp f g)
                CategoryTheory.Linear.smul_comp._autoParam →
              autoParam
                  (∀ (X Y Z : C) (f : X ⟶ Y) (r : R) (g : Y ⟶ Z),
                    CategoryTheory.CategoryStruct.comp f (r • g) = r • CategoryTheory.CategoryStruct.comp f g)
                  CategoryTheory.Linear.comp_smul._autoParam →
                CategoryTheory.Linear R C
-- Mathlib.Data.Pi.Interval
Pi.Icc_eq : ∀ {ι : Type u_1} {α : ι → Type u_2} [inst : Fintype ι] [inst_1 : DecidableEq ι] [inst_2 : (i : ι) → DecidableEq (α i)]
  [inst_3 : (i : ι) → PartialOrder (α i)] [inst_4 : (i : ι) → LocallyFiniteOrder (α i)] (a b : (i : ι) → α i),
  Finset.Icc a b = Fintype.piFinset fun i => Finset.Icc (a i) (b i)
-- Batteries.Lean.Except
instDecidableEqExcept_batteries : {ε : Type u_1} → {α : Type u_2} → [DecidableEq ε] → [DecidableEq α] → DecidableEq (Except ε α)
-- Std.Data.DTreeMap.Raw.Lemmas
Std.DTreeMap.Raw.getKey_union_of_not_mem_left : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t₁ t₂ : Std.DTreeMap.Raw α β cmp} [inst : Std.TransCmp cmp]
  (h₁ : t₁.WF) (h₂ : t₂.WF) {k : α} (not_mem : k ∉ t₁) {h' : k ∈ t₁ ∪ t₂}, (t₁ ∪ t₂).getKey k h' = t₂.getKey k ⋯
-- Mathlib.MeasureTheory.Function.AEEqFun
MeasureTheory.AEEqFun.toGerm_eq : ∀ {α : Type u_1} {β : Type u_2} [inst : MeasurableSpace α] {μ : MeasureTheory.Measure α} [inst_1 : TopologicalSpace β]
  (f : α →ₘ[μ] β), f.toGerm = ↑↑f
-- Std.Data.DHashMap.Raw
/-- Removes the mapping for the given key if it exists.  -/
Std.DHashMap.Raw.erase : {α : Type u} → {β : α → Type v} → [BEq α] → [Hashable α] → Std.DHashMap.Raw α β → α → Std.DHashMap.Raw α β
-- Mathlib.Computability.Language
Language.add_self : ∀ {α : Type u_1} (l : Language α), l + l = l
-- Mathlib.Combinatorics.SimpleGraph.Acyclic
SimpleGraph.isTree_iff : ∀ {V : Type u_1} (G : SimpleGraph V), G.IsTree ↔ G.Connected ∧ G.IsAcyclic
-- Mathlib.Order.Interval.Finset.SuccPred
Finset.insert_Ico_left_eq_Ico_pred : ∀ {α : Type u_1} [inst : LinearOrder α] [inst_1 : LocallyFiniteOrder α] [inst_2 : PredOrder α] {a b : α} [NoMinOrder α],
  a ≤ b → insert (Order.pred a) (Finset.Ico a b) = Finset.Ico (Order.pred a) b
-- Mathlib.Order.Preorder.Chain
Flag.coe_mk : ∀ {α : Type u_1} [inst : LE α] (s : Set α) (h₁ : IsChain (fun x1 x2 => x1 ≤ x2) s)
  (h₂ : ∀ ⦃s_1 : Set α⦄, IsChain (fun x1 x2 => x1 ≤ x2) s_1 → s ⊆ s_1 → s = s_1),
  ↑{ carrier := s, Chain' := h₁, max_chain' := h₂ } = s
-- Lean.Meta.Tactic.Simp.BuiltinSimprocs.Nat
Nat.reduceMul : Lean.Meta.Simp.DSimproc
-- Mathlib.Algebra.Ring.Divisibility.Basic
/-- **Alias** of the reverse direction of `neg_dvd`.

---

The negation of an element `a` of a semigroup with a distributive negation divides another
element `b` iff `a` divides `b`.  -/
Dvd.dvd.neg_left : ∀ {α : Type u_1} [inst : Semigroup α] [inst_1 : HasDistribNeg α] {a b : α}, a ∣ b → -a ∣ b
-- Mathlib.Algebra.Ring.Divisibility.Lemmas
dvd_mul_sub_mul_mul_gcd_of_dvd : ∀ {R : Type u_1} [inst : CommRing R] {p a b c d x y : R} [inst_1 : GCDMonoid R],
  p ∣ a * x + b * y → p ∣ c * x + d * y → p ∣ (a * d - b * c) * gcd x y
-- Mathlib.Topology.FiberBundle.Basic
FiberBundleCore.mem_localTrivAt_source : ∀ {ι : Type u_1} {B : Type u_2} {F : Type u_3} [inst : TopologicalSpace B] [inst_1 : TopologicalSpace F]
  (Z : FiberBundleCore ι B F) (p : Z.TotalSpace) (b : B),
  p ∈ (Z.localTrivAt b).source ↔ p.proj ∈ (Z.localTrivAt b).baseSet
-- Std.Data.TreeMap.Lemmas
Std.TreeMap.getKey!_inter_of_not_mem_left : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t₁ t₂ : Std.TreeMap α β cmp} [Std.TransCmp cmp]
  [inst : Inhabited α] {k : α}, k ∉ t₁ → (t₁ ∩ t₂).getKey! k = default
-- Mathlib.Algebra.Algebra.Spectrum.Quasispectrum
PreQuasiregular.instMonoid : {R : Type u_1} → [NonUnitalSemiring R] → Monoid (PreQuasiregular R)
-- Mathlib.Analysis.RCLike.Basic
RCLike.div_I : ∀ {K : Type u_1} [inst : RCLike K] (z : K), z / RCLike.I = -(z * RCLike.I)
-- Mathlib.MeasureTheory.Function.LpSeminorm.LpNorm
MeasureTheory.lpNorm_fun_neg : ∀ {α : Type u_1} {E : Type u_2} {m : MeasurableSpace α} [inst : NormedAddCommGroup E] (f : α → E) (p : ENNReal)
  (μ : MeasureTheory.Measure α), MeasureTheory.lpNorm (fun x => -f x) p μ = MeasureTheory.lpNorm f p μ
-- Mathlib.MeasureTheory.Measure.MeasureSpace
/-- If `s ⊆ t`, `μ t ≤ μ s`, `μ t ≠ ∞`, and `s` is measurable, then `s =ᵐ[μ] t`.  -/
MeasureTheory.ae_eq_of_subset_of_measure_ge : ∀ {α : Type u_1} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} {s t : Set α},
  s ⊆ t → μ t ≤ μ s → MeasureTheory.NullMeasurableSet s μ → μ t ≠ ⊤ → s =ᵐ[μ] t
-- Mathlib.Analysis.InnerProductSpace.Defs
InnerProductSpace.Core.inner_add_right : ∀ {𝕜 : Type u_1} {F : Type u_3} [inst : RCLike 𝕜] [inst_1 : AddCommGroup F] [inst_2 : Module 𝕜 F]
  [c : PreInnerProductSpace.Core 𝕜 F] (x y z : F), inner 𝕜 x (y + z) = inner 𝕜 x y + inner 𝕜 x z
-- Std.Data.Iterators.Combinators.Monadic.Drop
Std.Iterators.Types.Drop.PlausibleStep : {α : Type w} →
  {m : Type w → Type w'} → {β : Type w} → [Std.Iterator α m β] → Std.IterM m β → Std.IterStep (Std.IterM m β) β → Prop
-- Mathlib.Algebra.Polynomial.Div
Polynomial.modByMonic_eq_zero_iff_dvd : ∀ {R : Type u} [inst : Ring R] {p q : Polynomial R}, q.Monic → (p %ₘ q = 0 ↔ q ∣ p)
-- Mathlib.Topology.MetricSpace.Contracting
ContractingWith.one_sub_K_pos' : ∀ {α : Type u_1} [inst : EMetricSpace α] {K : NNReal} {f : α → α}, ContractingWith K f → 0 < 1 - ↑K
-- Init.Data.Range.Polymorphic.IntLemmas
Int.map_add_toList_roo' : ∀ {m n k : ℤ}, List.map (fun x => k + x) (m<...n).toList = ((k + m)<...k + n).toList
-- Mathlib.Data.Set.Finite.Basic
Set.finite_of_finite_preimage : ∀ {α : Type u} {β : Type v} {f : α → β} {s : Set β}, (f ⁻¹' s).Finite → s ⊆ Set.range f → s.Finite
-- Std.Net.Addr
/-- The kinds of address families supported by Lean, currently only IP variants.
 -/
Std.Net.AddressFamily : Type
-- Mathlib.GroupTheory.OrderOfElement
/-- The additive submonoid generated by an element is
an additive group if that element has finite order.  -/
IsOfFinAddOrder.addGroupMultiples : {G : Type u_1} → [inst : AddMonoid G] → {x : G} → IsOfFinAddOrder x → AddGroup ↥(AddSubmonoid.multiples x)
-- Mathlib.Analysis.Normed.Unbundled.SeminormFromBounded
/-- The real-valued function sending `x ∈ R` to the supremum of  `f(x*y)/f(y)`, where `y` runs over
the elements of `R`.  -/
seminormFromBounded' : {R : Type u_1} → [CommRing R] → (R → ℝ) → R → ℝ
-- Mathlib.Tactic.Sat.FromLRAT
/-- The fundamental relationship between `mk` and `implies`:
`(mk ps).implies p ps 0` is equivalent to `p`.  -/
Sat.Valuation.mk_implies : ∀ {p : Prop} {as ps : List Prop} (as₁ : List Prop),
  as = as₁.reverseAux ps → (Sat.Valuation.mk as).implies p ps as₁.length → p
-- Mathlib.GroupTheory.Commutator.Finite
Subgroup.finiteIndex_center : ∀ {G : Type u_1} [inst : Group G] [Finite ↑(commutatorSet G)] [Group.FG G], (Subgroup.center G).FiniteIndex
-- Mathlib.SetTheory.Cardinal.NatCard
Set.Finite.card_strictMonoOn : ∀ {α : Type u_1}, StrictMonoOn (Nat.card ∘ Set.Elem) (Set.ofPred Set.Finite)
-- Mathlib.CategoryTheory.ObjectProperty.Retract
CategoryTheory.ObjectProperty.IsStableUnderRetracts.of_binaryBicone_left : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] (P : CategoryTheory.ObjectProperty C) [P.IsStableUnderRetracts]
  [inst_2 : CategoryTheory.Limits.HasZeroMorphisms C] {X Y : C} (c : CategoryTheory.Limits.BinaryBicone X Y),
  P c.pt → P X
-- Mathlib.Algebra.Category.Grp.Basic
/-- An alias for `AddCommGrpCat.{max u v}`, to deal around unification issues.  -/
AddCommGrpMax : Type ((max u1 u2) + 1)
-- Mathlib.FieldTheory.IsRealClosed.Basic
IsRealClosed.mk : ∀ {R : Type u_1} [inst : Field R] [toIsSemireal : IsSemireal R],
  (∀ (x : R), IsSquare x ∨ IsSquare (-x)) → (∀ {f : Polynomial R}, Odd f.natDegree → ∃ x, f.IsRoot x) → IsRealClosed R
-- Mathlib.Data.Fintype.Defs
Finset.mem_univ_val : ∀ {α : Type u_1} [inst : Fintype α] (x : α), x ∈ Finset.univ.val
-- Mathlib.Order.InitialSeg
/-- An order isomorphism is an initial segment  -/
OrderIso.toInitialSeg : {α : Type u_1} → {β : Type u_2} → [inst : Preorder α] → [inst_1 : Preorder β] → α ≃o β → α ≤i β
-- Std.Data.DHashMap.Internal.RawLemmas
Std.DHashMap.Internal.Raw₀.getD_union_of_contains_eq_false_left : ∀ {α : Type u} {β : α → Type v} [inst : BEq α] [inst_1 : Hashable α] {m₁ m₂ : Std.DHashMap.Internal.Raw₀ α β}
  [inst_2 : LawfulBEq α],
  (↑m₁).WF →
    (↑m₂).WF → ∀ {k : α} {fallback : β k}, m₁.contains k = false → (m₁.union m₂).getD k fallback = m₂.getD k fallback
-- Std.Do.SPred.Laws
/-- Relates a stateful value to a pure value, lifting equality through the state layers.  -/
Std.Do.SVal.evalsTo : {α : Type u} → {σs : List (Type u)} → Std.Do.SVal σs α → α → Std.Do.SPred σs
-- Init.Data.UInt.Lemmas
UInt32.le_iff_lt_or_eq : ∀ {a b : UInt32}, a ≤ b ↔ a < b ∨ a = b
-- Lean.Declaration
Lean.DefinitionSafety.unsafe : Lean.DefinitionSafety
-- Mathlib.Order.Filter.IsBounded
Monotone.isBoundedUnder_le_comp_iff : ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} [Nonempty β] [inst : LinearOrder β] [inst_1 : Preorder γ] [NoMaxOrder γ]
  {g : β → γ} {f : α → β} {l : Filter α},
  Monotone g →
    Filter.Tendsto g Filter.atTop Filter.atTop →
      (Filter.IsBoundedUnder (fun x1 x2 => x1 ≤ x2) l (g ∘ f) ↔ Filter.IsBoundedUnder (fun x1 x2 => x1 ≤ x2) l f)