mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Order.Std
Preorder.OfStdArgs.mk.inj : ∀ {α : Type u_1} {le : autoParam (LE α) Preorder.OfStdArgs.le._autoParam}
  {lt :
    autoParam
      (let this := le;
      LT α)
      Preorder.OfStdArgs.lt._autoParam}
  {lawfulOrderLT :
    autoParam
      (let this := le;
      let this_1 := lt;
      Std.LawfulOrderLT α)
      Preorder.OfStdArgs.lawfulOrderLT._autoParam}
  {isPreorder :
    autoParam
      (let this := le;
      Std.IsPreorder α)
      Preorder.OfStdArgs.isPreorder._autoParam}
  {le_1 : autoParam (LE α) Preorder.OfStdArgs.le._autoParam}
  {lt_1 :
    autoParam
      (let this := le_1;
      LT α)
      Preorder.OfStdArgs.lt._autoParam}
  {lawfulOrderLT_1 :
    autoParam
      (let this := le_1;
      let this_1 := lt_1;
      Std.LawfulOrderLT α)
      Preorder.OfStdArgs.lawfulOrderLT._autoParam}
  {isPreorder_1 :
    autoParam
      (let this := le_1;
      Std.IsPreorder α)
      Preorder.OfStdArgs.isPreorder._autoParam},
  { le := le, lt := lt, lawfulOrderLT := lawfulOrderLT, isPreorder := isPreorder } =
      { le := le_1, lt := lt_1, lawfulOrderLT := lawfulOrderLT_1, isPreorder := isPreorder_1 } →
    le = le_1 ∧ lt = lt_1
-- Lean.Elab.MutualDef
_private.Lean.Elab.MutualDef.0.Lean.Elab.Term.registerFailedToInferDefTypeInfo : Lean.Expr → Lean.Elab.DefView → Lean.Elab.TermElabM Unit
-- Mathlib.Probability.Process.LocalProperty
ProbabilityTheory.Locally.right : ∀ {ι : Type u_1} {Ω : Type u_2} {E : Type u_3} {mΩ : MeasurableSpace Ω} {P : MeasureTheory.Measure Ω}
  [inst : LinearOrder ι] {𝓕 : MeasureTheory.Filtration ι mΩ} {X : ι → Ω → E} {p q : (ι → Ω → E) → Prop}
  [inst_1 : OrderBot ι] [inst_2 : TopologicalSpace ι] [inst_3 : OrderTopology ι] [inst_4 : Zero E],
  ProbabilityTheory.Locally (fun Y => p Y ∧ q Y) 𝓕 X P → ProbabilityTheory.Locally q 𝓕 X P
-- Init.Data.Range.Polymorphic.SInt
Int8.instRxiHasSize.eq_1 : Int8.instRxiHasSize = { size := fun lo => (2 ^ 7 - lo.toInt).toNat }
-- Mathlib.Combinatorics.SimpleGraph.Connectivity.Subgraph
SimpleGraph.Subgraph.connected_iff_forall_exists_walk_subgraph : ∀ {V : Type u} {G : SimpleGraph V} (H : G.Subgraph),
  H.Connected ↔ H.verts.Nonempty ∧ ∀ {u v : V}, u ∈ H.verts → v ∈ H.verts → ∃ p, p.toSubgraph ≤ H
-- Init.Control.Lawful.Instances
OptionT.mk.eq_1 : ∀ {m : Type u → Type v} {α : Type u} (x : m (Option α)), OptionT.mk x = x
-- Mathlib.Topology.PartialHomeomorph.Defs
PartialHomeomorph.coe_toPartialEquiv_symm : ∀ {X : Type u_1} {Y : Type u_3} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y] (e : PartialHomeomorph X Y),
  ↑e.symm = ↑e.symm
-- Mathlib.RingTheory.Localization.FractionRing
IsFractionRing.mul_inv_cancel : ∀ (A : Type u_4) [inst : CommRing A] {K : Type u_5} [inst_1 : CommRing K] [inst_2 : Algebra A K]
  [inst_3 : IsFractionRing A K] [inst_4 : IsDomain A] (x : K), x ≠ 0 → x * IsFractionRing.inv A x = 1
-- Lean.Compiler.IR.Basic
Lean.IR.Decl.fdecl : Lean.IR.FunId → Array Lean.IR.Param → Lean.IR.IRType → Lean.IR.FnBody → Lean.IR.DeclInfo → Lean.IR.Decl
-- Batteries.Data.List.Basic
/-- Right-biased version of `List.zipWith`. `zipWithRight' f as bs` applies `f` to each
pair of elements `aᵢ ∈ as` and `bᵢ ∈ bs`. If `as` is shorter than `bs`, `f` is
applied to `none` for the remaining `bᵢ`. Returns the results of the `f`
applications and the remaining `as`.
```
zipWithRight' prod.mk [1] ['a', 'b'] = ([(some 1, 'a'), (none, 'b')], [])
zipWithRight' prod.mk [1, 2] ['a'] = ([(some 1, 'a')], [2])
```
 -/
List.zipWithRight' : {α : Type u_1} → {β : Type u_2} → {γ : Type u_3} → (Option α → β → γ) → List α → List β → List γ × List α
-- Mathlib.MeasureTheory.Function.StronglyMeasurable.AEStronglyMeasurable
MeasureTheory.StronglyMeasurable.aestronglyMeasurable : ∀ {α : Type u_1} {β : Type u_2} [inst : TopologicalSpace β] {m m₀ : MeasurableSpace α} {μ : MeasureTheory.Measure α}
  {f : α → β}, MeasureTheory.StronglyMeasurable f → MeasureTheory.AEStronglyMeasurable f μ
-- Mathlib.AlgebraicTopology.DoldKan.GammaCompN
/-- The counit isomorphism of the Dold-Kan equivalence for additive categories.  -/
AlgebraicTopology.DoldKan.N₂Γ₂ : {C : Type u_1} →
  [inst : CategoryTheory.Category.{v_1, u_1} C] →
    [inst_1 : CategoryTheory.Preadditive C] →
      [inst_2 : CategoryTheory.Limits.HasFiniteCoproducts C] →
        AlgebraicTopology.DoldKan.Γ₂.comp AlgebraicTopology.DoldKan.N₂ ≅
          CategoryTheory.Functor.id (CategoryTheory.Idempotents.Karoubi (ChainComplex C ℕ))
-- Lean.Meta.Tactic.TryThis
_private.Lean.Meta.Tactic.TryThis.0.Lean.Meta.Tactic.TryThis.addExactSuggestionCore : Bool →
  Option Lean.Elab.Tactic.SavedState →
    Lean.Expr → Lean.Elab.Tactic.TacticM (Lean.Meta.Tactic.TryThis.Suggestion ⊕ Lean.MessageData)
-- Init.Data.Array.Lemmas
_private.Init.Data.Array.Lemmas.0.Array.isEqvAux.match_1.eq_1 : ∀ {α : Type u_1} (xs : Array α) (motive : (x : ℕ) → x ≤ xs.size → Sort u_2) (x : 0 ≤ xs.size)
  (h_1 : (x : 0 ≤ xs.size) → motive 0 x) (h_2 : (i : ℕ) → (h : i + 1 ≤ xs.size) → motive i.succ h),
  (match 0, x with
    | 0, x => h_1 x
    | i.succ, h => h_2 i h) =
    h_1 x
-- Mathlib.SetTheory.Cardinal.Basic
Cardinal.ofNat_le_aleph0 : ∀ {n : ℕ} [inst : n.AtLeastTwo], OfNat.ofNat n ≤ Cardinal.aleph0
-- Mathlib.Combinatorics.SimpleGraph.Sum
SimpleGraph.Embedding.sumInr_apply : ∀ {V : Type u_3} {W : Type u_5} {G : SimpleGraph V} {H : SimpleGraph W} (u : W),
  SimpleGraph.Embedding.sumInr u = Sum.inr u
-- Std.Data.ExtTreeMap.Lemmas
Std.ExtTreeMap.getKey_insertManyIfNewUnit_list_of_not_mem_of_mem : ∀ {α : Type u} {cmp : α → α → Ordering} {t : Std.ExtTreeMap α Unit cmp} [inst : Std.TransCmp cmp] {l : List α}
  {k k' : α},
  cmp k k' = Ordering.eq →
    ∀ {h' : k' ∈ t.insertManyIfNewUnit l},
      k ∉ t → List.Pairwise (fun a b => ¬cmp a b = Ordering.eq) l → k ∈ l → (t.insertManyIfNewUnit l).getKey k' h' = k
-- Mathlib.Algebra.SkewMonoidAlgebra.Basic
SkewMonoidAlgebra.instRing : {k : Type u_1} →
  {G : Type u_2} → [inst : Ring k] → [inst_1 : Monoid G] → [MulSemiringAction G k] → Ring (SkewMonoidAlgebra k G)
-- Aesop.Search.Expansion.Norm
Aesop.NormM.State.mk.sizeOf_spec : ∀ (forwardState : Aesop.ForwardState) (forwardRuleMatches : Aesop.ForwardRuleMatches),
  sizeOf { forwardState := forwardState, forwardRuleMatches := forwardRuleMatches } =
    1 + sizeOf forwardState + sizeOf forwardRuleMatches
-- Lean.Compiler.InlineAttrs
Lean.Compiler.instInhabitedInlineAttributeKind : Inhabited Lean.Compiler.InlineAttributeKind
-- Lean.Elab.Term
Lean.Elab.builtinIncrementalElabs : IO.Ref Lean.NameSet
-- Mathlib.Algebra.Lie.Nilpotent
LieModule.nontrivial_max_triv_of_isNilpotent : ∀ (R : Type u) (L : Type v) (M : Type w) [inst : CommRing R] [inst_1 : LieRing L] [inst_2 : LieAlgebra R L]
  [inst_3 : AddCommGroup M] [inst_4 : Module R M] [inst_5 : LieRingModule L M] [inst_6 : LieModule R L M] [Nontrivial M]
  [LieModule.IsNilpotent L M], Nontrivial ↥(LieModule.maxTrivSubmodule R L M)
-- Std.Data.HashMap.Lemmas
Std.HashMap.Equiv.size_eq : ∀ {α : Type u} {β : Type v} {x : BEq α} {x_1 : Hashable α} {m₁ m₂ : Std.HashMap α β} [EquivBEq α] [LawfulHashable α],
  m₁.Equiv m₂ → m₁.size = m₂.size
-- Mathlib.Data.ENNReal.Basic
ENNReal.natCast_lt_coe : ∀ {r : NNReal} {n : ℕ}, ↑n < ↑r ↔ ↑n < r
-- Mathlib.Analysis.Calculus.ContDiff.FaaDiBruno
OrderedFinpartition.instUniqueZero : Unique (OrderedFinpartition 0)
-- Mathlib.MeasureTheory.Measure.TightNormed
MeasureTheory.isTightMeasureSet_range_of_tendsto_limsup_inner_of_norm_eq_one : ∀ {E : Type u_1} {mE : MeasurableSpace E} [inst : NormedAddCommGroup E] (𝕜 : Type u_2) [inst_1 : RCLike 𝕜]
  [inst_2 : InnerProductSpace 𝕜 E] [FiniteDimensional 𝕜 E] [BorelSpace E] {μ : ℕ → MeasureTheory.Measure E}
  [∀ (i : ℕ), MeasureTheory.IsFiniteMeasure (μ i)],
  (∀ (y : E),
      ‖y‖ = 1 →
        Filter.Tendsto (fun r => Filter.limsup (fun n => (μ n) {x | r < ‖inner 𝕜 y x‖}) Filter.atTop) Filter.atTop
          (nhds 0)) →
    MeasureTheory.IsTightMeasureSet (Set.range μ)
-- Mathlib.Computability.Ackermann
Nat.Partrec.Code.primrec_pappAck_step : Primrec Nat.Partrec.Code.pappAck.step
-- Lean.Elab.PreDefinition.FixedParams
/-- This data structure stores the result of the fixed parameter analysis. See `FixedParams.Info` for
details on the analysis.
 -/
Lean.Elab.FixedParamPerms : Type
-- Mathlib.CategoryTheory.Limits.Preserves.Shapes.AbelianImages
CategoryTheory.Abelian.PreservesImage.iso_hom_ι_assoc : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  {D : Type u₂} [inst_2 : CategoryTheory.Category.{v₂, u₂} D] [inst_3 : CategoryTheory.Limits.HasZeroMorphisms D]
  (F : CategoryTheory.Functor C D) [inst_4 : F.PreservesZeroMorphisms] {X Y : C} (f : X ⟶ Y)
  [inst_5 : CategoryTheory.Limits.HasCokernel f]
  [inst_6 : CategoryTheory.Limits.HasKernel (CategoryTheory.Limits.cokernel.π f)]
  [inst_7 : CategoryTheory.Limits.PreservesColimit (CategoryTheory.Limits.parallelPair f 0) F]
  [inst_8 :
    CategoryTheory.Limits.PreservesLimit (CategoryTheory.Limits.parallelPair (CategoryTheory.Limits.cokernel.π f) 0) F]
  [inst_9 : CategoryTheory.Limits.HasCokernel (F.map f)]
  [inst_10 : CategoryTheory.Limits.HasKernel (CategoryTheory.Limits.cokernel.π (F.map f))] {Z : D} (h : F.obj Y ⟶ Z),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.Abelian.PreservesImage.iso F f).hom
      (CategoryTheory.CategoryStruct.comp (CategoryTheory.Abelian.image.ι (F.map f)) h) =
    CategoryTheory.CategoryStruct.comp (F.map (CategoryTheory.Abelian.image.ι f)) h
-- Mathlib.Algebra.Group.Defs
InvOneClass.toOne : {G : Type u_2} → [self : InvOneClass G] → One G
-- Lean.Parser.Do
Lean.Parser.Term.notFollowedByRedefinedTermToken : Lean.Parser.Parser
-- Mathlib.MeasureTheory.Integral.Lebesgue.Basic
MeasureTheory.lintegral_mono' : ∀ {α : Type u_1} {m : MeasurableSpace α} ⦃μ ν : MeasureTheory.Measure α⦄,
  μ ≤ ν → ∀ ⦃f g : α → ENNReal⦄, f ≤ g → ∫⁻ (a : α), f a ∂μ ≤ ∫⁻ (a : α), g a ∂ν
-- Plausible.Sampleable
Plausible.arbitraryProxy : {α : Type u_1} → [inst : Plausible.SampleableExt α] → Plausible.Arbitrary (Plausible.SampleableExt.proxy α)
-- Mathlib.CategoryTheory.Limits.Indization.Category
CategoryTheory.instPreservesLimitsIndYoneda : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C],
  CategoryTheory.Limits.PreservesLimits CategoryTheory.Ind.yoneda
-- Mathlib.AlgebraicGeometry.AffineScheme
AlgebraicGeometry.IsAffineOpen.stalkMap_injective : ∀ {X Y : AlgebraicGeometry.Scheme} (f : X ⟶ Y) {U : TopologicalSpace.Opens ↥Y},
  AlgebraicGeometry.IsAffineOpen U →
    ∀ (x : ↥X) (hx : f x ∈ U),
      (∀ (g : ↑(Y.presheaf.obj (Opposite.op U))),
          (CategoryTheory.ConcreteCategory.hom (AlgebraicGeometry.Scheme.Hom.stalkMap f x))
                ((CategoryTheory.ConcreteCategory.hom (Y.presheaf.germ U (f x) hx)) g) =
              0 →
            (CategoryTheory.ConcreteCategory.hom (Y.presheaf.germ U (f x) hx)) g = 0) →
        Function.Injective ⇑(CategoryTheory.ConcreteCategory.hom (AlgebraicGeometry.Scheme.Hom.stalkMap f x))
-- Mathlib.CategoryTheory.WithTerminal.Basic
_private.Mathlib.CategoryTheory.WithTerminal.Basic.0.CategoryTheory.WithInitial.opEquiv.match_15.eq_2 : ∀ (C : Type u_1) [inst : CategoryTheory.Category.{u_2, u_1} C]
  (motive : (x y : CategoryTheory.WithTerminal Cᵒᵖ) → (x ⟶ y) → Sort u_3) (unop : C)
  (x : CategoryTheory.WithTerminal.of (Opposite.op unop) ⟶ CategoryTheory.WithTerminal.star)
  (h_1 :
    (x y : C) →
      (f : CategoryTheory.WithTerminal.of (Opposite.op x) ⟶ CategoryTheory.WithTerminal.of (Opposite.op y)) →
        motive (CategoryTheory.WithTerminal.of (Opposite.op x)) (CategoryTheory.WithTerminal.of (Opposite.op y)) f)
  (h_2 :
    (unop : C) →
      (x : CategoryTheory.WithTerminal.of (Opposite.op unop) ⟶ CategoryTheory.WithTerminal.star) →
        motive (CategoryTheory.WithTerminal.of (Opposite.op unop)) CategoryTheory.WithTerminal.star x)
  (h_3 :
    (x : CategoryTheory.WithTerminal.star ⟶ CategoryTheory.WithTerminal.star) →
      motive CategoryTheory.WithTerminal.star CategoryTheory.WithTerminal.star x),
  (match CategoryTheory.WithTerminal.of (Opposite.op unop), CategoryTheory.WithTerminal.star, x with
    | CategoryTheory.WithTerminal.of (Opposite.op x), CategoryTheory.WithTerminal.of (Opposite.op y), f => h_1 x y f
    | CategoryTheory.WithTerminal.of (Opposite.op unop), CategoryTheory.WithTerminal.star, x => h_2 unop x
    | CategoryTheory.WithTerminal.star, CategoryTheory.WithTerminal.star, x => h_3 x) =
    h_2 unop x
-- Mathlib.Data.Finset.Dedup
List.coe_toFinset : ∀ {α : Type u_1} [inst : DecidableEq α] (l : List α), ↑l.toFinset = {a | a ∈ l}
-- Mathlib.CategoryTheory.Limits.Constructions.Filtered
CategoryTheory.Limits.CoproductsFromFiniteFiltered.liftToFinset_obj_obj : ∀ (C : Type u) [inst : CategoryTheory.Category.{v, u} C] (α : Type w)
  [inst_1 : CategoryTheory.Limits.HasFiniteCoproducts C] (F : CategoryTheory.Functor (CategoryTheory.Discrete α) C)
  (s : Finset (CategoryTheory.Discrete α)),
  ((CategoryTheory.Limits.CoproductsFromFiniteFiltered.liftToFinset C α).obj F).obj s = ∐ fun x => F.obj ↑x
-- Mathlib.MeasureTheory.Order.Group.Lattice
measurable_abs : ∀ {α : Type u_1} [inst : Lattice α] [inst_1 : AddGroup α] [inst_2 : MeasurableSpace α] [MeasurableNeg α]
  [MeasurableSup₂ α], Measurable abs
-- Lean.Server.Completion.CompletionItemCompression
_private.Lean.Server.Completion.CompletionItemCompression.0.Lean.Lsp.ResolvableCompletionList.compressRangeFast : String → Lean.Lsp.Range → String
-- Mathlib.Algebra.Order.Ring.IsNonarchimedean
/-- If `f` is a nonarchimedean additive group seminorm on `α` with `f 1 = 1`, then for every `n : ℤ`
we have `f n ≤ 1`.  -/
IsNonarchimedean.apply_intCast_le_one : ∀ {R : Type u_1} [inst : Semiring R] [inst_1 : LinearOrder R] [IsStrictOrderedRing R] {F : Type u_2} {α : Type u_3}
  [inst_3 : AddGroupWithOne α] [inst_4 : FunLike F α R] [AddGroupSeminormClass F α R] [OneHomClass F α R] {f : F},
  IsNonarchimedean ⇑f → ∀ {n : ℤ}, f ↑n ≤ 1
-- Mathlib.Probability.Martingale.BorelCantelli
MeasureTheory.tendsto_sum_indicator_atTop_iff' : ∀ {Ω : Type u_2} {m0 : MeasurableSpace Ω} {μ : MeasureTheory.Measure Ω} {ℱ : MeasureTheory.Filtration ℕ m0}
  [MeasureTheory.IsFiniteMeasure μ] {s : ℕ → Set Ω},
  (∀ (n : ℕ), MeasurableSet (s n)) →
    ∀ᵐ (ω : Ω) ∂μ,
      Filter.Tendsto (fun n => ∑ k ∈ Finset.range n, (s (k + 1)).indicator 1 ω) Filter.atTop Filter.atTop ↔
        Filter.Tendsto (fun n => ∑ k ∈ Finset.range n, μ[(s (k + 1)).indicator 1 | ↑ℱ k] ω) Filter.atTop Filter.atTop
-- Init.Data.List.Basic
List.mem_of_elem_eq_true : ∀ {α : Type u} [inst : BEq α] [LawfulBEq α] {a : α} {as : List α}, List.elem a as = true → a ∈ as
-- Init.Data.SInt.Lemmas
instLawfulOrderLTInt8 : Std.LawfulOrderLT Int8
-- Mathlib.Analysis.SpecialFunctions.Gamma.BohrMollerup
Real.doublingGamma.eq_1 : ∀ (s : ℝ), s.doublingGamma = Real.Gamma (s / 2) * Real.Gamma (s / 2 + 1 / 2) * 2 ^ (s - 1) / √Real.pi
-- Lean.Meta.Tactic.Grind.Arith.Cutsat.ToInt
_private.Lean.Meta.Tactic.Grind.Arith.Cutsat.ToInt.0.Lean.Meta.Grind.Arith.Cutsat.toInt'.processPow : Lean.Expr → Lean.Expr → Lean.Expr → Lean.Meta.Grind.Arith.Cutsat.ToIntM (Lean.Expr × Lean.Expr)
-- Init.Data.UInt.Lemmas
UInt8.neg_one_eq : -1 = 255
-- Mathlib.CategoryTheory.Enriched.Limits.HasConicalProducts
CategoryTheory.Enriched.HasConicalProducts.mk : ∀ {V : outParam (Type u')} [inst : CategoryTheory.Category.{v', u'} V] [inst_1 : CategoryTheory.MonoidalCategory V]
  {C : Type u} [inst_2 : CategoryTheory.Category.{v, u} C] [inst_3 : CategoryTheory.EnrichedOrdinaryCategory V C],
  autoParam (∀ (J : Type w), CategoryTheory.Enriched.HasConicalLimitsOfShape (CategoryTheory.Discrete J) V C)
      CategoryTheory.Enriched.HasConicalProducts.hasConicalLimitsOfShape._autoParam →
    CategoryTheory.Enriched.HasConicalProducts V C
-- Mathlib.GroupTheory.Coxeter.Inversion
CoxeterSystem.IsReflection.odd_length : ∀ {B : Type u_1} {W : Type u_2} [inst : Group W] {M : CoxeterMatrix B} {cs : CoxeterSystem M W} {t : W},
  cs.IsReflection t → Odd (cs.length t)
-- Mathlib.Algebra.Group.Submonoid.Support
isMulPointed_iff_mulSupport_eq_bot : ∀ {G : Type u_1} [inst : Group G] {M : Submonoid G}, M.IsMulPointed ↔ M.mulSupport = ⊥
-- Mathlib.Analysis.Calculus.DerivativeTest
/-- If `f` is continuous at `a, b` and differentiable on `Ioo a b`, then `f` is continuous on
`Icc a b`.  -/
_private.Mathlib.Analysis.Calculus.DerivativeTest.0.continuousOn_Icc : ∀ {f : ℝ → ℝ} {a b : ℝ},
  ContinuousAt f a → ContinuousAt f b → DifferentiableOn ℝ f (Set.Ioo a b) → ContinuousOn f (Set.Icc a b)
-- Mathlib.Topology.Sets.Compacts
TopologicalSpace.Compacts.instPartialOrder : {α : Type u_1} → [inst : TopologicalSpace α] → PartialOrder (TopologicalSpace.Compacts α)
-- Mathlib.GroupTheory.OrderOfElement
exists_pow_eq_self_of_coprime : ∀ {G : Type u_1} [inst : Monoid G] {x : G} {n : ℕ}, n.Coprime (orderOf x) → ∃ m, (x ^ n) ^ m = x
-- Mathlib.Order.Interval.Set.InitialSeg
/-- If `i ≤ j`, then `Iic i` is an initial segment of `Iic j`.  -/
Set.initialSegIicIicOfLE : {α : Type u_1} → [inst : Preorder α] → {i j : α} → i ≤ j → ↑(Set.Iic i) ≤i ↑(Set.Iic j)
-- Mathlib.Algebra.Algebra.Subalgebra.Basic
AlgHom.mem_range_self : ∀ {R : Type u} {A : Type v} {B : Type w} [inst : CommSemiring R] [inst_1 : Semiring A] [inst_2 : Algebra R A]
  [inst_3 : Semiring B] [inst_4 : Algebra R B] (φ : A →ₐ[R] B) (x : A), φ x ∈ φ.range
-- Mathlib.CategoryTheory.Triangulated.TStructure.ETrunc
CategoryTheory.Triangulated.TStructure.eTruncGE_obj_coe : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Preadditive C]
  [inst_2 : CategoryTheory.Limits.HasZeroObject C] [inst_3 : CategoryTheory.HasShift C ℤ]
  [inst_4 : ∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive] [inst_5 : CategoryTheory.Pretriangulated C]
  (t : CategoryTheory.Triangulated.TStructure C) (n : ℤ), t.eTruncGE.obj (WithBotTop.coe n) = t.truncGE n
-- Mathlib.GroupTheory.Perm.Cycle.Factors
/-- `f.cycleOf x` is the cycle of the permutation `f` to which `x` belongs.  -/
Equiv.Perm.cycleOf : {α : Type u_2} → (f : Equiv.Perm α) → [DecidableRel f.SameCycle] → α → Equiv.Perm α
-- Lean.Meta.Tactic.Grind.Types
Lean.Meta.Grind.Split.State.mk : ℕ →
  List Lean.Meta.Grind.SplitInfo →
    Std.HashSet Lean.Meta.Grind.SplitInfo →
      Lean.PHashSet Lean.Meta.Sym.ExprPtr →
        List Lean.Meta.Grind.CaseTrace →
          List Lean.Meta.Grind.SplitInfo →
            Std.HashMap (Lean.Expr × Lean.Expr) (List ℕ) →
              Lean.PHashMap (Lean.Expr × ℕ) (List Lean.Meta.Grind.SplitArg) → Lean.Meta.Grind.Split.State
-- Mathlib.Algebra.Polynomial.Degree.Operations
Polynomial.ne_zero_of_natDegree_gt : ∀ {R : Type u} [inst : Semiring R] {p : Polynomial R} {n : ℕ}, n < p.natDegree → p ≠ 0
-- Mathlib.CategoryTheory.Monoidal.Cartesian.Normal
/-- A morphism `φ : H ⟶ G` of additive group objects is a normal monoid homomorphism if it is a
monoid homomorphism that is mono and such that the conjugation map `(g, h) ↦ g + h - g`
factors through `φ`.  -/
CategoryTheory.IsAddMonHom.Normal : {C : Type u_1} →
  [inst : CategoryTheory.Category.{v_1, u_1} C] →
    [inst_1 : CategoryTheory.CartesianMonoidalCategory C] →
      {G H : C} → [CategoryTheory.AddGrpObj G] → [CategoryTheory.AddGrpObj H] → (H ⟶ G) → Prop
-- Mathlib.MeasureTheory.Function.JacobianOneDim
/-- Change of variable formula for differentiable functions, set version: if a real function `f` is
antitone and differentiable on a measurable set `s`, then the measure of `f '' s` is given by the
integral of `-f' x` on `s` .
Note that the measurability of `f '' s` is given by `MeasurableSet.image_of_antitoneOn`.  -/
MeasureTheory.lintegral_deriv_eq_volume_image_of_antitoneOn : ∀ {s : Set ℝ} {f f' : ℝ → ℝ},
  MeasurableSet s →
    (∀ x ∈ s, HasDerivWithinAt f (f' x) s x) →
      AntitoneOn f s → ∫⁻ (x : ℝ) in s, ENNReal.ofReal (-f' x) = MeasureTheory.volume (f '' s)
-- Mathlib.CategoryTheory.Functor.EpiMono
CategoryTheory.Adjunction.strongMono_map_of_strongMono : ∀ {C : Type u_1} {D : Type u_2} [inst : CategoryTheory.Category.{v_1, u_1} C]
  [inst_1 : CategoryTheory.Category.{v_2, u_2} D] {F : CategoryTheory.Functor C D} {F' : CategoryTheory.Functor D C}
  {A B : C} (adj : F' ⊣ F) (f : B ⟶ A) [F'.PreservesEpimorphisms] [F.PreservesMonomorphisms]
  [CategoryTheory.StrongMono f], CategoryTheory.StrongMono (F.map f)
-- Mathlib.Order.RelIso.Basic
RelIso.trans_refl : ∀ {α : Type u_1} {β : Type u_2} {r : α → α → Prop} {s : β → β → Prop} (e : r ≃r s), e.trans (RelIso.refl s) = e
-- Init.Data.Range.Polymorphic.Lemmas
Std.Rcc.forIn'_eq_forIn'_toArray : ∀ {α : Type u} {r : Std.Rcc α} [inst : LE α] [inst_1 : DecidableLE α] [inst_2 : Std.PRange.UpwardEnumerable α]
  [inst_3 : Std.PRange.LawfulUpwardEnumerableLE α] [inst_4 : Std.Rxc.IsAlwaysFinite α]
  [inst_5 : Std.PRange.LawfulUpwardEnumerable α] {γ : Type u} {init : γ} {m : Type u → Type w} [inst_6 : Monad m]
  [LawfulMonad m] {f : (a : α) → a ∈ r → γ → m (ForInStep γ)},
  forIn' r init f = forIn' r.toArray init fun a ha acc => f a ⋯ acc
-- Mathlib.RingTheory.DividedPowers.SubDPIdeal
DividedPowers.Quotient.OfSurjective.dpow_apply : ∀ {A : Type u_1} [inst : CommRing A] {I : Ideal A} (hI : DividedPowers I) {B : Type u_2} [inst_1 : CommRing B]
  {f : A →+* B} {J : Ideal B} (hf : Function.Surjective ⇑f) (hIJ : J = Ideal.map f I)
  (hIf : hI.IsSubDPIdeal (RingHom.ker f ⊓ I)) {n : ℕ} {a : A},
  a ∈ I → (DividedPowers.Quotient.OfSurjective.dividedPowers hI hf hIJ hIf).dpow n (f a) = f (hI.dpow n a)
-- Mathlib.Topology.Compactness.Compact
/-- A locally bounded function maps a compact set to a bounded set.  -/
Bornology.isBounded_image_of_isLocallyBounded_of_isCompact : ∀ {X : Type u} [inst : TopologicalSpace X] {Y : Type u_2} [inst_1 : Bornology Y] {s : Set X},
  IsCompact s → ∀ {f : X → Y}, (∀ (x : X), ∃ t ∈ nhds x, Bornology.IsBounded (f '' t)) → Bornology.IsBounded (f '' s)
-- Mathlib.LinearAlgebra.AffineSpace.Midpoint
vsub_midpoint : ∀ {R : Type u_1} {V : Type u_2} {P : Type u_4} [inst : Ring R] [inst_1 : Invertible 2] [inst_2 : AddCommGroup V]
  [inst_3 : Module R V] [inst_4 : AddTorsor V P] (p₁ p₂ p : P), p -ᵥ midpoint R p₁ p₂ = ⅟2 • (p -ᵥ p₁) + ⅟2 • (p -ᵥ p₂)
-- Mathlib.Algebra.Homology.Monoidal
HomologicalComplex.instHasTensorOfHasTensorX : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.MonoidalCategory C]
  [inst_2 : CategoryTheory.Preadditive C] [inst_3 : (CategoryTheory.MonoidalCategory.curriedTensor C).Additive]
  [inst_4 : ∀ (X₁ : C), ((CategoryTheory.MonoidalCategory.curriedTensor C).obj X₁).Additive] {I : Type u_2}
  [inst_5 : AddMonoid I] {c : ComplexShape I} [inst_6 : c.TensorSigns] (K₁ K₂ : HomologicalComplex C c)
  [CategoryTheory.GradedObject.HasTensor K₁.X K₂.X], K₁.HasTensor K₂
-- Mathlib.Data.PFunctor.Multivariate.M
TypeVec.splitFun.eq_2 : ∀ {n : ℕ} {α : TypeVec.{u_1} (n + 1)} {α' : TypeVec.{u_2} (n + 1)} (f : α.drop.Arrow α'.drop) (g : α.last → α'.last),
  TypeVec.splitFun f g Fin2.fz = g
-- Mathlib.CategoryTheory.Sites.Hypercover.Homotopy
/-- Up to homotopy, the category of (pre-)`1`-hypercovers is cofiltered.  -/
CategoryTheory.PreOneHypercover.exists_nonempty_homotopy : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {S : C} {E : CategoryTheory.PreOneHypercover S}
  {F : CategoryTheory.PreOneHypercover S} [CategoryTheory.Limits.HasPullbacks C] (f g : E.Hom F),
  ∃ W h, Nonempty (CategoryTheory.PreOneHypercover.Homotopy (h.comp f) (h.comp g))
-- Mathlib.Order.Lattice
Bool.instDistribLattice : DistribLattice Bool
-- Std.Data.TreeMap.Lemmas
Std.TreeMap.minKeyD_insert_le_self : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Std.TreeMap α β cmp} [Std.TransCmp cmp] {k : α} {v : β}
  {fallback : α}, (cmp ((t.insert k v).minKeyD fallback) k).isLE = true
-- Mathlib.Algebra.Order.Monoid.Unbundled.WithTop
WithTop.untopD_zero : ∀ {α : Type u} [inst : Zero α] (d : α), WithTop.untopD d 0 = 0
-- Aesop.Tree.Data
Aesop.RappData.parent : {Goal MVarCluster : Type} → Aesop.RappData Goal MVarCluster → IO.Ref Goal
-- Mathlib.RingTheory.Algebraic.Basic
Subalgebra.isAlgebraic_bot_iff : ∀ {R : Type u} {S : Type u_1} [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : Algebra R S],
  Function.Injective ⇑(algebraMap R S) → ∀ {x : S}, IsAlgebraic (↥⊥) x ↔ IsAlgebraic R x
-- Std.Data.TreeMap.Raw.Lemmas
Std.TreeMap.Raw.contains_union : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t₁ t₂ : Std.TreeMap.Raw α β cmp} [Std.TransCmp cmp],
  t₁.WF → t₂.WF → ∀ {k : α}, (t₁ ∪ t₂).contains k = (t₁.contains k || t₂.contains k)