mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.MeasureTheory.Function.LocallyIntegrable
MeasureTheory.LocallyIntegrableOn.mono_enorm : ∀ {X : Type u_1} {ε : Type u_3} {ε' : Type u_4} [inst : MeasurableSpace X] [inst_1 : TopologicalSpace X]
  [inst_2 : TopologicalSpace ε] [inst_3 : ContinuousENorm ε] [inst_4 : TopologicalSpace ε']
  [inst_5 : ContinuousENorm ε'] {f : X → ε} {μ : MeasureTheory.Measure X} {s : Set X},
  MeasureTheory.LocallyIntegrableOn f s μ →
    ∀ {g : X → ε'},
      MeasureTheory.AEStronglyMeasurable g μ →
        (∀ᵐ (x : X) ∂μ, ‖g x‖ₑ ≤ ‖f x‖ₑ) → MeasureTheory.LocallyIntegrableOn g s μ
-- Mathlib.Data.Set.Basic
Set.mem_dite_empty_left : ∀ {α : Type u} (p : Prop) [inst : Decidable p] (t : ¬p → Set α) (x : α),
  (x ∈ if h : p then ∅ else t h) ↔ ∃ (h : ¬p), x ∈ t h
-- Mathlib.Algebra.Order.CauSeq.Completion
/-- `CauSeq.Completion.ofRat` as a `RingHom`  -/
CauSeq.Completion.ofRatRingHom : {α : Type u_1} →
  [inst : Field α] →
    [inst_1 : LinearOrder α] →
      [inst_2 : IsStrictOrderedRing α] →
        {β : Type u_2} →
          [inst_3 : Ring β] → {abv : β → α} → [inst_4 : IsAbsoluteValue abv] → β →+* CauSeq.Completion.Cauchy abv
-- Init.Data.SInt.Basic
instAddISize : Add ISize
-- Mathlib.Data.NNReal.Defs
NNReal.sup_mul : ∀ (a b c : NNReal), max a b * c = max (a * c) (b * c)
-- Mathlib.Topology.Algebra.Valued.ValuationTopology
/-- The set `{ y : R | v y = v x }` is a neighbourhood of `x`.
This does not imply that `v` is locally constant everywhere (since `v ⁻¹' {0}` is not open),
but it is equivalent to the restriction of `v` to the complement of its support being
locally constant.  -/
Valued.locally_const : ∀ {R : Type u} [inst : Ring R] {Γ₀ : Type v} [inst_1 : LinearOrderedCommGroupWithZero Γ₀] [_i : Valued R Γ₀] {x : R},
  Valued.v x ≠ 0 → {y | Valued.v y = Valued.v x} ∈ nhds x
-- Mathlib.Probability.Independence.Basic
ProbabilityTheory.iIndepFun.indepFun_sub_left₀ : ∀ {Ω : Type u_1} {ι : Type u_2} {_mΩ : MeasurableSpace Ω} {μ : MeasureTheory.Measure Ω} {β : Type u_10}
  {m : MeasurableSpace β} [inst : Sub β] [MeasurableSub₂ β] {f : ι → Ω → β},
  ProbabilityTheory.iIndepFun f μ →
    (∀ (i : ι), AEMeasurable (f i) μ) → ∀ (i j k : ι), i ≠ k → j ≠ k → ProbabilityTheory.IndepFun (f i - f j) (f k) μ
-- Mathlib.NumberTheory.SmoothNumbers
/-- If `p` is positive and `n` is `p`-smooth, then every product `p^e * n` is `(p+1)`-smooth.  -/
Nat.pow_mul_mem_smoothNumbers : ∀ {p n : ℕ}, p ≠ 0 → ∀ (e : ℕ), n ∈ p.smoothNumbers → p ^ e * n ∈ p.succ.smoothNumbers
-- Std.Data.ExtTreeMap.Lemmas
Std.ExtTreeMap.minKey!_eq_iff_mem_and_forall : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Std.ExtTreeMap α β cmp} [inst : Std.TransCmp cmp]
  [Std.LawfulEqCmp cmp] [inst_2 : Inhabited α],
  t ≠ ∅ → ∀ {km : α}, t.minKey! = km ↔ km ∈ t ∧ ∀ k ∈ t, (cmp km k).isLE = true
-- Mathlib.Topology.Separation.Hausdorff
tendsto_nhds_unique_of_frequently_eq : ∀ {X : Type u_1} {Y : Type u_2} [inst : TopologicalSpace X] [T2Space X] {f g : Y → X} {l : Filter Y} {a b : X},
  Filter.Tendsto f l (nhds a) → Filter.Tendsto g l (nhds b) → (∃ᶠ (x : Y) in l, f x = g x) → a = b
-- Lean.Data.Lsp.InitShutdown
Lean.Lsp.instToJsonInitializationOptions.toJson : Lean.Lsp.InitializationOptions → Lean.Json
-- Mathlib.Computability.TuringMachine.StackTuringMachine
Turing.TM2.stmts_trans : ∀ {K : Type u_1} {Γ : K → Type u_2} {Λ : Type u_3} {σ : Type u_4} {M : Λ → Turing.TM2.Stmt Γ Λ σ} {S : Finset Λ}
  {q₁ q₂ : Turing.TM2.Stmt Γ Λ σ},
  q₁ ∈ Turing.TM2.stmts₁ q₂ → some q₂ ∈ Turing.TM2.stmts M S → some q₁ ∈ Turing.TM2.stmts M S
-- Mathlib.MeasureTheory.Integral.Bochner.Basic
/-- Monotone convergence theorem for real-valued functions and Bochner integrals  -/
MeasureTheory.integral_tendsto_of_tendsto_of_monotone : ∀ {α : Type u_1} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} {f : ℕ → α → ℝ} {F : α → ℝ},
  (∀ (n : ℕ), MeasureTheory.Integrable (f n) μ) →
    MeasureTheory.Integrable F μ →
      (∀ᵐ (x : α) ∂μ, Monotone fun n => f n x) →
        (∀ᵐ (x : α) ∂μ, Filter.Tendsto (fun n => f n x) Filter.atTop (nhds (F x))) →
          Filter.Tendsto (fun n => ∫ (x : α), f n x ∂μ) Filter.atTop (nhds (∫ (x : α), F x ∂μ))
-- Lean.Expr
Lean.Expr.bindingInfo! : Lean.Expr → Lean.BinderInfo
-- Mathlib.CategoryTheory.ObjectProperty.ContainsZero
CategoryTheory.ObjectProperty.instContainsZeroMapOfPreservesZeroMorphisms : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {D : Type u'} [inst_1 : CategoryTheory.Category.{v', u'} D]
  (P : CategoryTheory.ObjectProperty C) [P.ContainsZero] [inst_3 : CategoryTheory.Limits.HasZeroMorphisms C]
  [inst_4 : CategoryTheory.Limits.HasZeroMorphisms D] (F : CategoryTheory.Functor C D) [F.PreservesZeroMorphisms],
  (P.map F).ContainsZero
-- Init.Data.List.MinMaxIdx
List.minIdxOn_take_le : ∀ {β : Type u_1} {α : Type u_2} [inst : LE β] [inst_1 : DecidableLE β] [Std.IsLinearPreorder β] {xs : List α}
  {f : α → β} {i : ℕ} (h : List.take i xs ≠ []), List.minIdxOn f (List.take i xs) h ≤ List.minIdxOn f xs ⋯
-- Init.Data.String.Lemmas.FindPos
_private.Init.Data.String.Lemmas.FindPos.0.String.posLE.eq_1 : ∀ (s : String) (offset : String.Pos.Raw), s.posLE offset = String.Pos.ofToSlice (s.toSlice.posLE offset)
-- Mathlib.GroupTheory.CoprodI
_private.Mathlib.GroupTheory.CoprodI.0.Monoid.CoprodI.NeWord.toList.match_1.eq_2 : ∀ {ι : Type u_1} {M : ι → Type u_2} [inst : (i : ι) → Monoid (M i)]
  (motive : (x x_1 : ι) → Monoid.CoprodI.NeWord M x x_1 → Sort u_3) (x x_1 j k : ι) (w₁ : Monoid.CoprodI.NeWord M x j)
  (_hne : j ≠ k) (w₂ : Monoid.CoprodI.NeWord M k x_1)
  (h_1 : (i : ι) → (x : M i) → (a : x ≠ 1) → motive i i (Monoid.CoprodI.NeWord.singleton x a))
  (h_2 :
    (x x_2 j k : ι) →
      (w₁ : Monoid.CoprodI.NeWord M x j) →
        (_hne : j ≠ k) → (w₂ : Monoid.CoprodI.NeWord M k x_2) → motive x x_2 (w₁.append _hne w₂)),
  (match x, x_1, w₁.append _hne w₂ with
    | i, .(i), Monoid.CoprodI.NeWord.singleton x a => h_1 i x a
    | x, x_2, w₁.append _hne w₂ => h_2 x x_2 j k w₁ _hne w₂) =
    h_2 x x_1 j k w₁ _hne w₂
-- Init.Data.List.Sort.Impl
List.MergeSort.Internal.splitRevInTwo_fst : ∀ {α : Type u_1} {n : ℕ} (l : { l // l.length = n }),
  (List.MergeSort.Internal.splitRevInTwo l).1 = ⟨(↑(List.MergeSort.Internal.splitInTwo l).1).reverse, ⋯⟩
-- Init.Data.Vector.Zip
Vector.unzip_fst : ∀ {α : Type u_1} {β : Type u_2} {n : ℕ} {xs : Vector (α × β) n}, xs.unzip.1 = Vector.map Prod.fst xs
-- Std.Data.DTreeMap.Internal.Zipper
_private.Std.Data.DTreeMap.Internal.Zipper.0.Std.DTreeMap.Internal.Zipper.prependMapGE.eq_1 : ∀ {α : Type u} {β : α → Type v} [inst : Ord α] (lowerBound : α) (it : Std.DTreeMap.Internal.Zipper α β),
  Std.DTreeMap.Internal.Zipper.prependMapGE Std.DTreeMap.Internal.Impl.leaf lowerBound it = it
-- Mathlib.Data.Analysis.Topology
Ctop.mk.inj : ∀ {α : Type u_1} {σ : Type u_2} {f : σ → Set α} {top : α → σ} {top_mem : ∀ (x : α), x ∈ f (top x)}
  {inter : (a b : σ) → (x : α) → x ∈ f a ∩ f b → σ}
  {inter_mem : ∀ (a b : σ) (x : α) (h : x ∈ f a ∩ f b), x ∈ f (inter a b x h)}
  {inter_sub : ∀ (a b : σ) (x : α) (h : x ∈ f a ∩ f b), f (inter a b x h) ⊆ f a ∩ f b} {f_1 : σ → Set α} {top_1 : α → σ}
  {top_mem_1 : ∀ (x : α), x ∈ f_1 (top_1 x)} {inter_1 : (a b : σ) → (x : α) → x ∈ f_1 a ∩ f_1 b → σ}
  {inter_mem_1 : ∀ (a b : σ) (x : α) (h : x ∈ f_1 a ∩ f_1 b), x ∈ f_1 (inter_1 a b x h)}
  {inter_sub_1 : ∀ (a b : σ) (x : α) (h : x ∈ f_1 a ∩ f_1 b), f_1 (inter_1 a b x h) ⊆ f_1 a ∩ f_1 b},
  { f := f, top := top, top_mem := top_mem, inter := inter, inter_mem := inter_mem, inter_sub := inter_sub } =
      { f := f_1, top := top_1, top_mem := top_mem_1, inter := inter_1, inter_mem := inter_mem_1,
        inter_sub := inter_sub_1 } →
    f = f_1 ∧ top = top_1 ∧ inter ≍ inter_1
-- Mathlib.Probability.Process.Stopping
MeasureTheory.stronglyMeasurable_stoppedValue_of_le : ∀ {Ω : Type u_1} {β : Type u_2} {ι : Type u_3} {m : MeasurableSpace Ω} [inst : Nonempty ι] {u : ι → Ω → β}
  {τ : Ω → WithTop ι} [inst_1 : LinearOrder ι] [inst_2 : MeasurableSpace ι] [inst_3 : TopologicalSpace ι]
  [OrderTopology ι] [SecondCountableTopology ι] [BorelSpace ι] [inst_7 : TopologicalSpace β]
  {f : MeasureTheory.Filtration ι m},
  MeasureTheory.IsStronglyProgressive f u →
    MeasureTheory.IsStoppingTime f τ →
      ∀ {n : ι}, (∀ (ω : Ω), τ ω ≤ ↑n) → MeasureTheory.StronglyMeasurable (MeasureTheory.stoppedValue u τ)
-- Lean.Meta.Tactic.Grind.Extension
Lean.Meta.Grind.instInhabitedCasesTypes.default : Lean.Meta.Grind.CasesTypes
-- Mathlib.MeasureTheory.Measure.Map
MeasurableEmbedding.map_apply : ∀ {α : Type u_1} {β : Type u_2} {m0 : MeasurableSpace α} {m1 : MeasurableSpace β} {f : α → β},
  MeasurableEmbedding f → ∀ (μ : MeasureTheory.Measure α) (s : Set β), (MeasureTheory.Measure.map f μ) s = μ (f ⁻¹' s)
-- Mathlib.CategoryTheory.Monoidal.Cartesian.Basic
CategoryTheory.CartesianMonoidalCategory.whiskerLeft_toUnit_comp_rightUnitor_hom_assoc : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.CartesianMonoidalCategory C] (X Y : C)
  {Z : C} (h : X ⟶ Z),
  CategoryTheory.CategoryStruct.comp
      (CategoryTheory.MonoidalCategoryStruct.whiskerLeft X (CategoryTheory.SemiCartesianMonoidalCategory.toUnit Y))
      (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.rightUnitor X).hom h) =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.SemiCartesianMonoidalCategory.fst X Y) h
-- Mathlib.Order.Filter.Finite
Filter.iInf_sets_eq_finite : ∀ {α : Type u} {ι : Type u_2} (f : ι → Filter α), (⨅ i, f i).sets = ⋃ t, (⨅ i ∈ t, f i).sets
-- Mathlib.AlgebraicTopology.SimplexCategory.SemiSimplexCategory
SemiSimplexCategory.ext : ∀ {x y : SemiSimplexCategory}, x.len = y.len → x = y
-- Init.Grind.Ring.CommSolver
Lean.Grind.CommRing.Stepwise.core : ∀ {α : Type u_1} [inst : Lean.Grind.CommRing α] (ctx : Lean.Grind.CommRing.Context α)
  (lhs rhs : Lean.Grind.CommRing.Expr) (p : Lean.Grind.CommRing.Poly),
  Lean.Grind.CommRing.Stepwise.core_cert lhs rhs p = true →
    Lean.Grind.CommRing.Expr.denote ctx lhs = Lean.Grind.CommRing.Expr.denote ctx rhs →
      Lean.Grind.CommRing.Poly.denote ctx p = 0
-- Std.Internal.Do.Triple.SpecLemmas
_private.Std.Internal.Do.Triple.SpecLemmas.0.Lean.Loop.forIn.match_1.eq_2 : ∀ {β : Type u_1} (motive : ForInStep β → Sort u_2) (b' : β) (h_1 : (b' : β) → motive (ForInStep.done b'))
  (h_2 : (b' : β) → motive (ForInStep.yield b')),
  (match ForInStep.yield b' with
    | ForInStep.done b' => h_1 b'
    | ForInStep.yield b' => h_2 b') =
    h_2 b'
-- Init.Data.Vector.Lemmas
Vector.back_append_right : ∀ {α : Type u_1} {n m : ℕ} {xs : Vector α n} {ys : Vector α m} [inst : NeZero m], (xs ++ ys).back = ys.back
-- Std.Internal.Parsec.ByteArray
/-- Parse a single byte equal to `b`, fails if different.
 -/
Std.Internal.Parsec.ByteArray.pbyte : UInt8 → Std.Internal.Parsec.ByteArray.Parser UInt8
-- Mathlib.CategoryTheory.Idempotents.Biproducts
CategoryTheory.Idempotents.Karoubi.karoubi_hasFiniteBiproducts : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v, u_1} C] [inst_1 : CategoryTheory.Preadditive C]
  [CategoryTheory.Limits.HasFiniteBiproducts C],
  CategoryTheory.Limits.HasFiniteBiproducts (CategoryTheory.Idempotents.Karoubi C)
-- Mathlib.GroupTheory.GroupAction.Quotient
MulAction.orbitEquivQuotientStabilizer.eq_1 : ∀ (G : Type u) {X : Type v} [inst : Group G] [inst_1 : MulAction G X] (b : X),
  MulAction.orbitEquivQuotientStabilizer G b =
    (Equiv.ofBijective (fun g => ⟨MulAction.ofQuotientStabilizer G b g, ⋯⟩) ⋯).symm
-- Mathlib.Algebra.BigOperators.Finsupp.Basic
SubmonoidClass.finsuppProd_mem : ∀ {α : Type u_1} {M : Type u_8} {N : Type u_10} [inst : Zero M] [inst_1 : CommMonoid N] {S : Type u_16}
  [inst_2 : SetLike S N] [SubmonoidClass S N] (s : S) (f : α →₀ M) (g : α → M → N),
  (∀ (c : α), f c ≠ 0 → g c (f c) ∈ s) → f.prod g ∈ s
-- Batteries.Data.HashMap.Basic
/-- Given a key `a`, returns a key-value pair in the map whose key compares equal to `a`.
Note that the returned key may not be identical to the input, if `==` ignores some part
of the value.
```
def hashMap := ofList [("one", 1), ("two", 2)]
hashMap.findEntry? "one" = some ("one", 1)
hashMap.findEntry? "three" = none
```
 -/
Batteries.HashMap.findEntry? : {α : Type u_1} → {β : Type u_2} → [inst : BEq α] → [inst_1 : Hashable α] → Batteries.HashMap α β → α → Option (α × β)
-- Init.Core
EStateM.Result.error.injEq : ∀ {ε σ α : Type u} (a : ε) (a_1 : σ) (a_2 : ε) (a_3 : σ),
  (EStateM.Result.error a a_1 = EStateM.Result.error a_2 a_3) = (a = a_2 ∧ a_1 = a_3)
-- Mathlib.Algebra.Group.Conj
/-- The quotient type of conjugacy classes of a group.  -/
ConjClasses : (α : Type u_1) → [Monoid α] → Type u_1
-- Mathlib.Topology.Sets.Closeds
TopologicalSpace.Closeds.mk.inj : ∀ {α : Type u_4} {inst : TopologicalSpace α} {carrier : Set α} {isClosed' : IsClosed carrier} {carrier_1 : Set α}
  {isClosed'_1 : IsClosed carrier_1},
  { carrier := carrier, isClosed' := isClosed' } = { carrier := carrier_1, isClosed' := isClosed'_1 } →
    carrier = carrier_1
-- Mathlib.Data.List.Rotate
List.cyclicPermutations_eq_singleton_iff : ∀ {α : Type u} {l : List α} {x : α}, l.cyclicPermutations = [[x]] ↔ l = [x]
-- Std.Data.ExtHashMap.Lemmas
Std.ExtHashMap.getD.congr_simp : ∀ {α : Type u} {β : Type v} {x : BEq α} {x_1 : Hashable α} [inst : EquivBEq α] [inst_1 : LawfulHashable α]
  (m m_1 : Std.ExtHashMap α β),
  m = m_1 →
    ∀ (a a_1 : α),
      a = a_1 → ∀ (fallback fallback_1 : β), fallback = fallback_1 → m.getD a fallback = m_1.getD a_1 fallback_1
-- Mathlib.Data.Vector.Basic
List.Vector.get_zero : ∀ {α : Type u_1} {n : ℕ} (v : List.Vector α n.succ), v.get 0 = v.head
-- Init.Data.String.PosRaw
String.pos_add_char : ∀ (p : String.Pos.Raw) (c : Char), (p + c).byteIdx = p.byteIdx + c.utf8Size
-- Mathlib.Analysis.Calculus.FDeriv.Basic
HasFDerivAtFilter.isThetaTVS_sub : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : AddCommGroup E] [inst_2 : Module 𝕜 E]
  [inst_3 : TopologicalSpace E] {F : Type u_3} [inst_4 : NormedAddCommGroup F] [inst_5 : NormedSpace 𝕜 F] {f : E → F}
  {f' : E →L[𝕜] F} {L : Filter (E × E)},
  HasFDerivAtFilter f f' L → Topology.IsInducing ⇑f' → (fun p => f p.1 - f p.2) =Θ[𝕜; L] fun p => p.1 - p.2
-- Mathlib.CategoryTheory.Triangulated.Functor
CategoryTheory.Functor.IsTriangulated.mk : ∀ {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.HasShift C ℤ]
  [inst_3 : CategoryTheory.HasShift D ℤ] {F : CategoryTheory.Functor C D} [inst_4 : F.CommShift ℤ]
  [inst_5 : CategoryTheory.Limits.HasZeroObject C] [inst_6 : CategoryTheory.Limits.HasZeroObject D]
  [inst_7 : CategoryTheory.Preadditive C] [inst_8 : CategoryTheory.Preadditive D]
  [inst_9 : ∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive]
  [inst_10 : ∀ (n : ℤ), (CategoryTheory.shiftFunctor D n).Additive] [inst_11 : CategoryTheory.Pretriangulated C]
  [inst_12 : CategoryTheory.Pretriangulated D],
  (∀ T ∈ CategoryTheory.Pretriangulated.distinguishedTriangles,
      F.mapTriangle.obj T ∈ CategoryTheory.Pretriangulated.distinguishedTriangles) →
    F.IsTriangulated
-- Mathlib.RingTheory.HahnSeries.Multiplication
HahnSeries.instDistrib : {Γ : Type u_1} →
  {R : Type u_3} →
    [inst : AddCommMonoid Γ] →
      [inst_1 : PartialOrder Γ] →
        [IsOrderedCancelAddMonoid Γ] → [inst : NonUnitalNonAssocSemiring R] → Distrib (HahnSeries Γ R)
-- Mathlib.Probability.Independence.Integration
/-- Independence of functions `f` and `g` into arbitrary types is characterized by the relation
`E[(φ ∘ f) * (ψ ∘ g)] = E[φ ∘ f] * E[ψ ∘ g]` for all measurable `φ` and `ψ` with values in `ℝ`
satisfying appropriate integrability conditions.  -/
ProbabilityTheory.indepFun_iff_integral_comp_mul : ∀ {Ω : Type u_1} {mΩ : MeasurableSpace Ω} {μ : MeasureTheory.Measure Ω} [MeasureTheory.IsFiniteMeasure μ] {β : Type u_3}
  {β' : Type u_4} {mβ : MeasurableSpace β} {mβ' : MeasurableSpace β'} {f : Ω → β} {g : Ω → β'} {hfm : Measurable f}
  {hgm : Measurable g},
  ProbabilityTheory.IndepFun f g μ ↔
    ∀ {φ : β → ℝ} {ψ : β' → ℝ},
      Measurable φ →
        Measurable ψ →
          MeasureTheory.Integrable (φ ∘ f) μ →
            MeasureTheory.Integrable (ψ ∘ g) μ →
              MeasureTheory.integral μ (φ ∘ f * ψ ∘ g) =
                MeasureTheory.integral μ (φ ∘ f) * MeasureTheory.integral μ (ψ ∘ g)
-- Mathlib.Algebra.Group.Pi.Basic
Function.comp_ne_zero_iff : ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} [inst : Zero β] [inst_1 : Zero γ] (f : α → β) {g : β → γ},
  Function.Injective g → g 0 = 0 → (g ∘ f ≠ 0 ↔ f ≠ 0)
-- Mathlib.CategoryTheory.Limits.Constructions.ZeroObjects
CategoryTheory.Limits.inr_coprodZeroIso_hom : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Limits.HasZeroObject C]
  [inst_2 : CategoryTheory.Limits.HasZeroMorphisms C] (X : C),
  CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.coprod.inl (CategoryTheory.Limits.coprodZeroIso X).hom =
    CategoryTheory.CategoryStruct.id X
-- Mathlib.Algebra.Group.Subgroup.ZPowers.Basic
Subgroup.zpow_mem_zpowers : ∀ {G : Type u_1} [inst : Group G] (g : G) (k : ℤ), g ^ k ∈ Subgroup.zpowers g
-- Mathlib.CategoryTheory.Monoidal.Functor
CategoryTheory.Functor.Monoidal.whiskerLeft_μ_δ : ∀ {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]
  (F : CategoryTheory.Functor C D) [inst_4 : F.Monoidal] (X Y : C) (T : D),
  CategoryTheory.CategoryStruct.comp
      (CategoryTheory.MonoidalCategoryStruct.whiskerLeft T (CategoryTheory.Functor.LaxMonoidal.μ F X Y))
      (CategoryTheory.MonoidalCategoryStruct.whiskerLeft T (CategoryTheory.Functor.OplaxMonoidal.δ F X Y)) =
    CategoryTheory.CategoryStruct.id
      (CategoryTheory.MonoidalCategoryStruct.tensorObj T
        (CategoryTheory.MonoidalCategoryStruct.tensorObj (F.obj X) (F.obj Y)))
-- Batteries.Recycling.RBTree.WF
RBTree.RBNode.All.setRed : ∀ {α : Type u_1} {p : α → Prop} {t : RBTree.RBNode α}, RBTree.RBNode.All p t → RBTree.RBNode.All p t.setRed
-- Mathlib.RingTheory.IsAdjoinRoot
/-- Extensionality of the `IsAdjoinRoot` structure itself. See `IsAdjoinRootMonic.ext_elem`
for extensionality of the ring elements.  -/
IsAdjoinRoot.ext_map : ∀ {R : Type u} {S : Type v} [inst : CommRing R] [inst_1 : Ring S] {f : Polynomial R} [inst_2 : Algebra R S]
  (h h' : IsAdjoinRoot S f), (∀ (x : Polynomial R), h.map x = h'.map x) → h = h'
-- Mathlib.GroupTheory.CoprodI
Monoid.CoprodI.NeWord.singleton_head : ∀ {ι : Type u_1} {M : ι → Type u_2} [inst : (i : ι) → Monoid (M i)] {i : ι} (x : M i) (hne_one : x ≠ 1),
  (Monoid.CoprodI.NeWord.singleton x hne_one).head = x
-- Mathlib.Tactic.NormNum.Result
/-- `Result.toRawEq` but providing an integer. Given a `NormNum.Result e` for something known to be an
integer (which uses `IsNat` or `IsInt` to express equality to an integer numeral), converts it to
an equality `e = Nat.rawCast n` or `e = Int.rawCast n` to a raw cast expression, so it can be used
for rewriting. Gives `none` if not an integer.
 -/
Mathlib.Meta.NormNum.Result.toRawIntEq : {u : Lean.Level} →
  {α : Q(Type u)} → {e : Q(«$α»)} → Mathlib.Meta.NormNum.Result e → Option (ℤ × (e' : Q(«$α»)) × Q(«$e» = «$e'»))
-- Mathlib.Algebra.Order.Group.Action
smul_inf_le : ∀ {M : Type u_2} {α : Type u_3} [inst : SMul M α] [inst_1 : SemilatticeInf α] [CovariantClass M α HSMul.hSMul LE.le]
  (m : M) (a₁ a₂ : α), m • (a₁ ⊓ a₂) ≤ m • a₁ ⊓ m • a₂
-- Mathlib.Data.Multiset.AddSub
Multiset.instRightCommutativeErase : ∀ {α : Type u_1} [inst : DecidableEq α], RightCommutative Multiset.erase
-- Std.Data.DTreeMap.Raw.Lemmas
Std.DTreeMap.Raw.mem_of_mem_filter : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t : Std.DTreeMap.Raw α β cmp} [Std.TransCmp cmp]
  {f : (a : α) → β a → Bool} {k : α}, t.WF → k ∈ Std.DTreeMap.Raw.filter f t → k ∈ t
-- Mathlib.Data.List.Find
/-- If there is at most one element satisfying `p`, then `find?` agrees on permuted lists.  -/
List.find?_eq_find?_of_perm : ∀ {α : Type u_1} {p : α → Bool} {l₁ l₂ : List α},
  l₁.Perm l₂ → {x | x ∈ l₁ ∧ p x = true}.Subsingleton → List.find? p l₁ = List.find? p l₂
-- Mathlib.Topology.Semicontinuity.Basic
lowerSemicontinuousWithinAt_iSup : ∀ {α : Type u_1} [inst : TopologicalSpace α] {s : Set α} {x : α} {ι : Sort u_4} {δ : Type u_5}
  [inst_1 : CompleteLinearOrder δ] {f : ι → α → δ},
  (∀ (i : ι), LowerSemicontinuousWithinAt (f i) s x) → LowerSemicontinuousWithinAt (fun x' => ⨆ i, f i x') s x
-- Mathlib.RingTheory.Bialgebra.Hom
/-- Reinterpret a `BialgHom` as a `MonoidHom`  -/
BialgHom.toMonoidHom : {R : Type u_1} →
  {A : Type u_2} →
    {B : Type u_3} →
      [inst : CommSemiring R] →
        [inst_1 : Semiring A] →
          [inst_2 : Algebra R A] →
            [inst_3 : Semiring B] →
              [inst_4 : Algebra R B] →
                [inst_5 : CoalgebraStruct R A] → [inst_6 : CoalgebraStruct R B] → (A →ₐc[R] B) → A →* B
-- Mathlib.Algebra.Polynomial.Laurent
LaurentPolynomial.mk'_one_X : ∀ {R : Type u_1} [inst : CommSemiring R],
  IsLocalization.mk' (LaurentPolynomial R) 1 ⟨Polynomial.X, ⋯⟩ = LaurentPolynomial.T (-1)
-- Init.Data.Array.MinMax
Array.max?_singleton : ∀ {α : Type u_1} [inst : Max α] {x : α}, #[x].max? = some x
-- Mathlib.AlgebraicTopology.SimplicialSet.NerveAdjunction
SSet.Truncated.liftOfStrictSegal.f₂.congr_simp : ∀ {X Y : SSet.Truncated 2}
  (f₀ f₀_1 :
    X.obj (Opposite.op { obj := { len := 0 }, property := _proof_11✝ }) →
      Y.obj (Opposite.op { obj := { len := 0 }, property := _proof_11✝ }))
  (e_f₀ : f₀ = f₀_1)
  (f₁ f₁_1 :
    X.obj (Opposite.op { obj := { len := 1 }, property := _proof_12✝ }) →
      Y.obj (Opposite.op { obj := { len := 1 }, property := _proof_12✝ }))
  (e_f₁ : f₁ = f₁_1)
  (hδ₁ :
    ∀ (x : X.obj (Opposite.op { obj := { len := 1 }, property := _proof_12✝ })),
      f₀ ((CategoryTheory.ConcreteCategory.hom (X.map (SimplexCategory.Truncated.δ₂ 1 _proof_11✝ _proof_13✝).op)) x) =
        (CategoryTheory.ConcreteCategory.hom (Y.map (SimplexCategory.Truncated.δ₂ 1 _proof_11✝ _proof_13✝).op)) (f₁ x))
  (hδ₀ :
    ∀ (x : X.obj (Opposite.op { obj := { len := 1 }, property := _proof_12✝ })),
      f₀ ((CategoryTheory.ConcreteCategory.hom (X.map (SimplexCategory.Truncated.δ₂ 0 _proof_11✝ _proof_13✝).op)) x) =
        (CategoryTheory.ConcreteCategory.hom (Y.map (SimplexCategory.Truncated.δ₂ 0 _proof_11✝ _proof_13✝).op)) (f₁ x))
  (hY hY_1 : Y.StrictSegal),
  hY = hY_1 →
    ∀ (x x_1 : X.obj (Opposite.op { obj := { len := 2 }, property := _proof_14✝ })),
      x = x_1 →
        SSet.Truncated.liftOfStrictSegal.f₂ f₀ f₁ hδ₁ hδ₀ hY x =
          SSet.Truncated.liftOfStrictSegal.f₂ f₀_1 f₁_1 ⋯ ⋯ hY_1 x_1
-- Lean.Attributes
/-- Given a list `[a₁, ..., a_n]` of elements of type `α`, `EnumAttributes` provides an attribute `Attr_i` for
associating a value `a_i` with an declaration. `α` is usually an enumeration type.
Note that whenever we register an `EnumAttributes`, we create `n` attributes, but only one environment extension.  -/
Lean.EnumAttributes : Type → Type
-- Mathlib.Algebra.Category.CommAlgCat.Monoidal
CommAlgCat.toUnit_unop_hom : ∀ {R : Type u} [inst : CommRing R] (A : (CommAlgCat R)ᵒᵖ),
  CommAlgCat.Hom.hom (CategoryTheory.SemiCartesianMonoidalCategory.toUnit A).unop = Algebra.ofId R ↑(Opposite.unop A)
-- Mathlib.RingTheory.IsTensorProduct
IsTensorProduct.lift.eq_1 : ∀ {R : Type u_1} [inst : CommSemiring R] {M₁ : Type u_2} {M₂ : Type u_3} {M : Type u_4} {M' : Type u_5}
  [inst_1 : AddCommMonoid M₁] [inst_2 : AddCommMonoid M₂] [inst_3 : AddCommMonoid M] [inst_4 : AddCommMonoid M']
  [inst_5 : Module R M₁] [inst_6 : Module R M₂] [inst_7 : Module R M] [inst_8 : Module R M'] {f : M₁ →ₗ[R] M₂ →ₗ[R] M}
  (h : IsTensorProduct f) (f' : M₁ →ₗ[R] M₂ →ₗ[R] M'), h.lift f' = TensorProduct.lift f' ∘ₗ ↑h.equiv.symm
-- Mathlib.Algebra.Group.Submonoid.Defs
Submonoid.ext_iff : ∀ {M : Type u_1} [inst : MulOneClass M] {S T : Submonoid M}, S = T ↔ ∀ (x : M), x ∈ S ↔ x ∈ T
-- Mathlib.RingTheory.DividedPowers.Basic
DividedPowers.dpow_comp : ∀ {A : Type u_1} [inst : CommSemiring A] {I : Ideal A} (self : DividedPowers I) {m n : ℕ} {x : A},
  n ≠ 0 → x ∈ I → self.dpow m (self.dpow n x) = ↑(m.uniformBell n) * self.dpow (m * n) x