mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Data.Rel
SetRel.isSymm_iInter : ∀ {α : Type u_1} {ι : Sort u_5} {R : ι → SetRel α α} [∀ (i : ι), (R i).IsSymm], SetRel.IsSymm (⋂ i, R i)
-- Std.Data.Iterators.Consumers.Set
/-- Traverses the given iterator and stores the emitted values in a `TreeSet`.

This variant terminates after finitely many steps and requires a proof that the iterator is
finite. If such a proof is not available, consider using `Iter.toTreeSet`.
 -/
Std.Iter.Total.toTreeSet : {α β : Type w} →
  [inst : Std.Iterator α Id β] →
    [Std.Iterators.Finite α Id] →
      [Std.IteratorLoop α Id Id] →
        Std.Iter.Total β → (cmp : autoParam (β → β → Ordering) Std.Iter.Total.toTreeSet._auto_1) → Std.TreeSet β cmp
-- Mathlib.Algebra.Group.Submonoid.Basic
MonoidHom.eq_of_eqOn_denseM : ∀ {M : Type u_1} {N : Type u_2} [inst : MulOneClass M] [inst_1 : MulOneClass N] {s : Set M},
  Submonoid.closure s = ⊤ → ∀ {f g : M →* N}, Set.EqOn (⇑f) (⇑g) s → f = g
-- Lean.Elab.Do.Basic
Lean.Elab.Do.ContInfoRef : Type
-- Init.Data.Range.Polymorphic.SInt
_private.Init.Data.Range.Polymorphic.SInt.0.ISize.instRxcHasSize_eq : ISize.instRxcHasSize = HasModel.instRxcHasSize✝
-- Mathlib.Analysis.CStarAlgebra.Spectrum
_private.Mathlib.Analysis.CStarAlgebra.Spectrum.0.«term_⋆» : Lean.TrailingParserDescr
-- Mathlib.CategoryTheory.Triangulated.Functor
/-- `F.mapTriangle` commutes with the rotation of triangles.  -/
CategoryTheory.Functor.mapTriangleRotateIso : {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.Preadditive C] →
                  [inst_6 : CategoryTheory.Preadditive D] →
                    [F.Additive] →
                      F.mapTriangle.comp (CategoryTheory.Pretriangulated.rotate D) ≅
                        (CategoryTheory.Pretriangulated.rotate C).comp F.mapTriangle
-- Lean.Elab.Util
Lean.Elab.MonadMacroAdapter.getNextMacroScope : {m : Type → Type} → [self : Lean.Elab.MonadMacroAdapter m] → m Lean.MacroScope
-- Mathlib.Analysis.Convex.Body
ConvexBody.convex : ∀ {V : Type u_1} [inst : TopologicalSpace V] [inst_1 : AddCommGroup V] [inst_2 : Module ℝ V] (K : ConvexBody V),
  Convex ℝ ↑K
-- Mathlib.FieldTheory.KummerExtension
rootOfSplitsXPowSubC_pow : ∀ {K : Type u} [inst : Field K] {n : ℕ} (a : K) (L : Type u_1) [inst_1 : Field L] [inst_2 : Algebra K L]
  [inst_3 : Polynomial.IsSplittingField K L (Polynomial.X ^ n - Polynomial.C a)] [inst_4 : NeZero n],
  rootOfSplitsXPowSubC ⋯ a L ^ n = (algebraMap K L) a
-- Mathlib.SetTheory.Cardinal.Arithmetic
Cardinal.mk_bounded_set_le_of_infinite : ∀ (α : Type u) [Infinite α] (c : Cardinal.{u}), Cardinal.mk { t // Cardinal.mk ↑t ≤ c } ≤ Cardinal.mk α ^ c
-- Init.Data.List.Erase
List.IsPrefix.eraseIdx : ∀ {α : Type u_1} {l l' : List α}, l <+: l' → ∀ (k : ℕ), l.eraseIdx k <+: l'.eraseIdx k
-- Init.Data.Vector.Find
Vector.find?_empty : ∀ {α : Type} {p : α → Bool}, Vector.find? p #v[] = none
-- Mathlib.Algebra.Group.Defs
/-- A group is called *cyclic* if it is generated by a single element. 

[Wikidata Q245462](https://www.wikidata.org/wiki/Q245462) -/
IsAddCyclic : (G : Type u) → [SMul ℤ G] → Prop
-- Mathlib.LinearAlgebra.CliffordAlgebra.BaseChange
CliffordAlgebra.ofBaseChange_tmul_ι : ∀ {R : Type u_1} (A : Type u_2) {V : Type u_3} [inst : CommRing R] [inst_1 : CommRing A] [inst_2 : AddCommGroup V]
  [inst_3 : Algebra R A] [inst_4 : Module R V] [inst_5 : Invertible 2] (Q : QuadraticForm R V) (z : A) (v : V),
  (CliffordAlgebra.ofBaseChange A Q) (z ⊗ₜ[R] (CliffordAlgebra.ι Q) v) =
    (CliffordAlgebra.ι (QuadraticForm.baseChange A Q)) (z ⊗ₜ[R] v)
-- Mathlib.AlgebraicGeometry.Morphisms.Finite
/-- **Alias** of `AlgebraicGeometry.IsFinite.finite_app`. -/
AlgebraicGeometry.Scheme.Hom.finite_app : ∀ {X Y : AlgebraicGeometry.Scheme} (f : X ⟶ Y) [self : AlgebraicGeometry.IsFinite f] (U : Y.Opens),
  AlgebraicGeometry.IsAffineOpen U → (CommRingCat.Hom.hom (AlgebraicGeometry.Scheme.Hom.app f U)).Finite
-- Mathlib.MeasureTheory.OuterMeasure.Basic
MeasureTheory.measure_pos_of_superset : ∀ {α : Type u_1} {F : Type u_3} [inst : FunLike F (Set α) ENNReal] [MeasureTheory.OuterMeasureClass F α] {μ : F}
  {s t : Set α}, s ⊆ t → μ s ≠ 0 → 0 < μ t
-- Std.Tactic.BVDecide.LRAT.Parser
Std.Tactic.BVDecide.LRAT.Parser.Binary.parseLit : Std.Internal.Parsec.ByteArray.Parser ℤ
-- Mathlib.CategoryTheory.Comma.StructuredArrow.Functor
CategoryTheory.CostructuredArrow.commaToGrothendieckPrecompFunctor_map_base : ∀ {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] (L : CategoryTheory.Functor C D)
  (R : CategoryTheory.Functor E D) {X Y : CategoryTheory.Comma L R} (f : X ⟶ Y),
  ((CategoryTheory.CostructuredArrow.commaToGrothendieckPrecompFunctor L R).map f).base = f.right
-- Mathlib.Geometry.Euclidean.Angle.Unoriented.TriangleInequality
_private.Mathlib.Geometry.Euclidean.Angle.Unoriented.TriangleInequality.0.InnerProductGeometry.angle_expression_of_angle_eq_angle_sum : ∀ {V : Type u_1} [inst : NormedAddCommGroup V] [inst_1 : InnerProductSpace ℝ V] {x y z : V},
  ‖x‖ = 1 →
    ‖y‖ = 1 →
      ‖z‖ = 1 →
        InnerProductGeometry.angle x z ≠ Real.pi →
          InnerProductGeometry.angle x z = InnerProductGeometry.angle x y + InnerProductGeometry.angle y z →
            Real.sin (InnerProductGeometry.angle x z) • y =
              Real.sin (InnerProductGeometry.angle y z) • x + Real.sin (InnerProductGeometry.angle x y) • z
-- Batteries.Data.Array.Basic
_private.Batteries.Data.Array.Basic.0.Array.scanrMFast.loop : {m : Type u_1 → Type u_2} →
  {α : Type u_3} →
    {β : Type u_1} →
      [Monad m] →
        (α → β → m β) →
          β →
            (as : Array α) →
              (start stop : USize) →
                start.toNat ≤ as.size → (acc : Array β) → start.toNat - stop.toNat < acc.size → m (Array β)
-- Mathlib.Order.Hom.BoundedLattice
/-- Reinterpret a bounded lattice homomorphism as a bounded lattice homomorphism between the dual
bounded lattices.  -/
BoundedLatticeHom.dual : {α : Type u_2} →
  {β : Type u_3} →
    [inst : Lattice α] →
      [inst_1 : BoundedOrder α] →
        [inst_2 : Lattice β] → [inst_3 : BoundedOrder β] → BoundedLatticeHom α β ≃ BoundedLatticeHom αᵒᵈ βᵒᵈ
-- Mathlib.Algebra.ContinuedFractions.Computation.CorrectnessTerminating
/-- If `GenContFract.of v` terminates, then its convergents will eventually always be `v`.  -/
GenContFract.of_correctness_atTop_of_terminates : ∀ {K : Type u_1} [inst : Field K] [inst_1 : LinearOrder K] {v : K} [inst_2 : FloorRing K],
  (GenContFract.of v).Terminates → ∀ᶠ (n : ℕ) in Filter.atTop, v = (GenContFract.of v).convs n
-- Std.Data.DHashMap.RawLemmas
Std.DHashMap.Raw.mem_alter_of_beq_eq_false : ∀ {α : Type u} {β : α → Type v} [inst : BEq α] [inst_1 : Hashable α] {m : Std.DHashMap.Raw α β} [inst_2 : LawfulBEq α]
  {k k' : α} {f : Option (β k) → Option (β k)}, m.WF → (k == k') = false → (k' ∈ m.alter k f ↔ k' ∈ m)
-- Mathlib.MeasureTheory.Function.AEEqFun
MeasureTheory.AEEqFun.instOne.eq_1 : ∀ {α : Type u_1} {β : Type u_2} [inst : MeasurableSpace α] {μ : MeasureTheory.Measure α} [inst_1 : TopologicalSpace β]
  [inst_2 : One β], MeasureTheory.AEEqFun.instOne = { one := MeasureTheory.AEEqFun.const α 1 }
-- Lean.Meta.Closure
Lean.Meta.Closure.State.levelArgs : Lean.Meta.Closure.State → Array Lean.Level
-- Qq.Macro
Qq.Impl.UnquoteState.levelNames : Qq.Impl.UnquoteState → List Lean.Name
-- Mathlib.Analysis.SpecialFunctions.Log.Base
Real.le_logb_iff_rpow_le_of_base_lt_one : ∀ {b x y : ℝ}, 0 < b → b < 1 → 0 < y → (x ≤ Real.logb b y ↔ y ≤ b ^ x)
-- Mathlib.Topology.Compactness.LocallyFinite
/-- If `X` is a compact space, then a locally finite family of nonempty sets of `X` can have only
finitely many elements, `Set.Finite` version.  -/
LocallyFinite.finite_of_compact : ∀ {X : Type u_1} {ι : Type u_2} [inst : TopologicalSpace X] [CompactSpace X] {f : ι → Set X},
  LocallyFinite f → (∀ (i : ι), (f i).Nonempty) → Set.univ.Finite
-- Mathlib.Algebra.Lie.Weights.Cartan
LieAlgebra.le_zeroRootSubalgebra : ∀ (R : Type u_1) (L : Type u_2) [inst : CommRing R] [inst_1 : LieRing L] [inst_2 : LieAlgebra R L]
  (H : LieSubalgebra R L) [inst_3 : LieRing.IsNilpotent ↥H], H ≤ LieAlgebra.zeroRootSubalgebra R L H
-- Std.Time.Internal.Bounded
/-- Convert a `Bounded.LE` to a Nat.
 -/
Std.Time.Internal.Bounded.LE.toNat : {lo hi : ℤ} → Std.Time.Internal.Bounded.LE lo hi → ℕ
-- Mathlib.Algebra.Homology.HomotopyCategory.DegreewiseSplit
CochainComplex.homOfDegreewiseSplit.eq_1 : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v, u_1} C] [inst_1 : CategoryTheory.Preadditive C]
  (S : CategoryTheory.ShortComplex (CochainComplex C ℤ))
  (σ : (n : ℤ) → (S.map (HomologicalComplex.eval C (ComplexShape.up ℤ) n)).Splitting),
  CochainComplex.homOfDegreewiseSplit S σ =
    (CochainComplex.HomComplex.Cocycle.equivHom S.X₃
          ((CategoryTheory.shiftFunctor (CochainComplex C ℤ) 1).obj S.X₁)).symm
      ((CochainComplex.cocycleOfDegreewiseSplit S σ).rightShift 1 0 CochainComplex.homOfDegreewiseSplit._proof_1)
-- Mathlib.CategoryTheory.Preadditive.Injective.Resolution
/-- the cochain complex must be degreewise injective  -/
CategoryTheory.InjectiveResolution.injective : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Limits.HasZeroObject C]
  [inst_2 : CategoryTheory.Limits.HasZeroMorphisms C] {Z : C} (self : CategoryTheory.InjectiveResolution Z) (n : ℕ),
  CategoryTheory.Injective (self.cocomplex.X n)
-- Lean.Meta.Tactic.Grind.Arith.Linear.Types
/-- `IsLinearOrder` instance if available  -/
Lean.Meta.Grind.Arith.Linear.NatStruct.isLinearInst? : Lean.Meta.Grind.Arith.Linear.NatStruct → Option Lean.Expr
-- Lean.Language.Basic
Lean.Language.Snapshot.mk.sizeOf_spec : ∀ (desc : autoParam String Lean.Language.Snapshot.desc._autoParam) (diagnostics : Lean.Language.Snapshot.Diagnostics)
  (infoTree? : Option Lean.Elab.InfoTree) (traces : Lean.TraceState) (isFatal : Bool),
  sizeOf { desc := desc, diagnostics := diagnostics, infoTree? := infoTree?, traces := traces, isFatal := isFatal } =
    1 + sizeOf desc + sizeOf diagnostics + sizeOf infoTree? + sizeOf traces + sizeOf isFatal
-- Init.Omega.Constraint
Lean.Omega.Constraint.mk.inj : ∀ {lowerBound : Lean.Omega.LowerBound} {upperBound : Lean.Omega.UpperBound} {lowerBound_1 : Lean.Omega.LowerBound}
  {upperBound_1 : Lean.Omega.UpperBound},
  { lowerBound := lowerBound, upperBound := upperBound } = { lowerBound := lowerBound_1, upperBound := upperBound_1 } →
    lowerBound = lowerBound_1 ∧ upperBound = upperBound_1
-- Mathlib.RingTheory.Polynomial.DegreeLT
Polynomial.comap_taylorEquiv_degreeLT : ∀ {R : Type u_1} [inst : CommRing R] {r : R} {n : ℕ},
  Submodule.comap (↑↑(Polynomial.taylorEquiv r)) (Polynomial.degreeLT R n) = Polynomial.degreeLT R n
-- Std.Time.Format.Basic
/-- Parses an input string using a builder function to produce a value.
 -/
Std.Time.GenericFormat.parseBuilder : {aw : Std.Time.Awareness} →
  {α : Type} →
    (format : Std.Time.GenericFormat aw) → Std.Time.FormatType (Option α) format.string → String → Except String α
-- Mathlib.Analysis.Complex.UpperHalfPlane.Manifold
UpperHalfPlane.contMDiff_inv_denom : ∀ {n : WithTop ℕ∞} (g : GL (Fin 2) ℝ),
  ContMDiff (modelWithCornersSelf ℂ ℂ) (modelWithCornersSelf ℂ ℂ) n fun τ => (UpperHalfPlane.denom g ↑τ)⁻¹
-- Init.Data.List.Basic
List.any_cons : ∀ {α : Type u_1} {a : α} {l : List α} {f : α → Bool}, (a :: l).any f = (f a || l.any f)
-- Init.Data.Slice.List.Lemmas
List.toList_mkSlice_roi_eq_toList_mkSlice_roo : ∀ {α : Type u_1} {xs : List α} {lo : ℕ},
  Std.Slice.toList (Std.Roi.Sliceable.mkSlice xs lo<...*) =
    Std.Slice.toList (Std.Roo.Sliceable.mkSlice xs lo<...xs.length)
-- Mathlib.CategoryTheory.Monoidal.Hopf_
/-- The underlying object in the ambient monoidal category  -/
CategoryTheory.Hopf.X : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    [inst_1 : CategoryTheory.MonoidalCategory C] →
      [inst_2 : CategoryTheory.BraidedCategory C] → CategoryTheory.Hopf C → C
-- Lean.Util.ParamMinimizer
_private.Lean.Util.ParamMinimizer.0.Lean.Util.ParamMinimizer.Context.mk.injEq : ∀ {m : Type → Type} (initialMask : Array Bool) (test : Array Bool → m Bool) (maxCalls : ℕ) (initialMask_1 : Array Bool)
  (test_1 : Array Bool → m Bool) (maxCalls_1 : ℕ),
  ({ initialMask := initialMask, test := test, maxCalls := maxCalls } =
      { initialMask := initialMask_1, test := test_1, maxCalls := maxCalls_1 }) =
    (initialMask = initialMask_1 ∧ test = test_1 ∧ maxCalls = maxCalls_1)
-- Mathlib.MeasureTheory.Constructions.ProjectiveFamilyContent
MeasureTheory.projectiveFamilyContent_cylinder : ∀ {ι : Type u_1} {α : ι → Type u_2} {mα : (i : ι) → MeasurableSpace (α i)}
  {P : (J : Finset ι) → MeasureTheory.Measure ((j : ↥J) → α ↑j)} {I : Finset ι} {S : Set ((i : ↥I) → α ↑i)}
  (hP : MeasureTheory.IsProjectiveMeasureFamily P),
  MeasurableSet S → (MeasureTheory.projectiveFamilyContent hP) (MeasureTheory.cylinder I S) = (P I) S
-- Mathlib.CategoryTheory.Limits.IsLimit
/-- If `F.cones` is represented by `X`, any cone is the extension of the limit cone by the
corresponding morphism.  -/
CategoryTheory.Limits.IsLimit.OfNatIso.cone_fac : ∀ {J : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} J] {C : Type u₃} [inst_1 : CategoryTheory.Category.{v₃, u₃} C]
  {F : CategoryTheory.Functor J C} {X : C} (h : F.cones.RepresentableBy X) (s : CategoryTheory.Limits.Cone F),
  (CategoryTheory.Limits.IsLimit.OfNatIso.limitCone h).extend (CategoryTheory.Limits.IsLimit.OfNatIso.homOfCone h s) = s
-- Mathlib.Computability.TuringMachine.Tape
Turing.Tape.nth.eq_1 : ∀ {Γ : Type u_1} [inst : Inhabited Γ] (T : Turing.Tape Γ), T.nth 0 = T.head
-- Mathlib.Algebra.BigOperators.Group.Finset.Piecewise
Fintype.sum_eq_add_sum_compl : ∀ {ι : Type u_1} {M : Type u_3} [inst : AddCommMonoid M] [inst_1 : DecidableEq ι] [inst_2 : Fintype ι] (a : ι)
  (f : ι → M), ∑ i, f i = f a + ∑ i ∈ {a}ᶜ, f i
-- Mathlib.Algebra.Lie.Subalgebra
LieSubalgebra.map_top : ∀ (R : Type u) (L : Type v) [inst : CommRing R] [inst_1 : LieRing L] [inst_2 : LieAlgebra R L] {L₂ : Type w}
  [inst_3 : LieRing L₂] [inst_4 : LieAlgebra R L₂] (f : L →ₗ⁅R⁆ L₂), f.range = LieSubalgebra.map f ⊤
-- Init.Data.List.Lemmas
List.getElem?_eq_some_getElem_iff : ∀ {α : Type u_1} {xs : List α} {i : ℕ} (h : i < xs.length), xs[i]? = some xs[i] ↔ True
-- Mathlib.CategoryTheory.Join.Pseudofunctor
CategoryTheory.Join.pseudofunctorLeft_mapComp_hom_toNatTrans_app : ∀ (D : Type u₂) [inst : CategoryTheory.Category.{v₂, u₂} D] {a b c : CategoryTheory.Cat} (x : a ⟶ b) (x_1 : b ⟶ c)
  (X : CategoryTheory.Join (↑a) D),
  ((CategoryTheory.Join.pseudofunctorLeft D).mapComp x x_1).hom.toNatTrans.app X =
    CategoryTheory.CategoryStruct.comp
      (match X with
      | CategoryTheory.Join.left x_2 =>
        CategoryTheory.CategoryStruct.id (CategoryTheory.Join.left (x_1.toFunctor.obj (x.toFunctor.obj x_2)))
      | CategoryTheory.Join.right x => CategoryTheory.CategoryStruct.id (CategoryTheory.Join.right x))
      ((CategoryTheory.Join.mapPairComp x.toFunctor (CategoryTheory.Functor.id D) x_1.toFunctor
              (CategoryTheory.Functor.id D)).hom.app
        X)
-- Mathlib.Tactic.Order.CollectFacts
Mathlib.Tactic.Order.instInhabitedAtomicFact : Inhabited Mathlib.Tactic.Order.AtomicFact
-- Mathlib.Algebra.Order.Module.HahnEmbedding
/-- `coeff` is strictly monotone.  -/
HahnEmbedding.Seed.strictMono_coeff : ∀ {K : Type u_1} [inst : DivisionRing K] [inst_1 : LinearOrder K] [inst_2 : IsOrderedRing K] [inst_3 : Archimedean K]
  {M : Type u_2} [inst_4 : AddCommGroup M] [inst_5 : LinearOrder M] [inst_6 : IsOrderedAddMonoid M]
  [inst_7 : Module K M] [inst_8 : IsOrderedModule K M] {R : Type u_3} [inst_9 : AddCommGroup R]
  [inst_10 : LinearOrder R] [inst_11 : Module K R] (self : HahnEmbedding.Seed K M R) (c : FiniteArchimedeanClass M),
  StrictMono ⇑(self.coeff c)
-- Init.Data.Range.Polymorphic.Lemmas
Std.Roc.forIn'_eq_match : ∀ {α : Type u} {r : Std.Roc α} [inst : LE α] [inst_1 : DecidableLE α] [inst_2 : LT α] [DecidableLT α]
  [inst_4 : Std.PRange.UpwardEnumerable α] [inst_5 : Std.PRange.LawfulUpwardEnumerableLT α]
  [inst_6 : Std.PRange.LawfulUpwardEnumerableLE α] [inst_7 : Std.Rxc.IsAlwaysFinite α]
  [inst_8 : Std.PRange.LawfulUpwardEnumerable α] {m : Type u → Type w} [inst_9 : Monad m] [LawfulMonad m] {γ : Type u}
  {init : γ} {f : (a : α) → a ∈ r → γ → m (ForInStep γ)},
  forIn' r init f =
    match hs : Std.PRange.succ? r.lower with
    | none => pure init
    | some next =>
      if hu : next ≤ r.upper then
        have hlt := ⋯;
        do
        let __do_lift ← f next ⋯ init
        match __do_lift with
          | ForInStep.yield c => forIn' (next<...=r.upper) c fun a ha acc => f a ⋯ acc
          | ForInStep.done c => pure c
      else pure init
-- Lean.Meta.Tactic.Grind.Types
/-- Returns all equivalence classes in the current goal.  -/
Lean.Meta.Grind.Goal.getEqcs : Lean.Meta.Grind.Goal → optParam Bool false → List (List Lean.Expr)
-- Mathlib.Algebra.Category.CommBialgCat
CommBialgCat.isoEquivBialgEquiv_apply : ∀ {R : Type u} [inst : CommRing R] {X Y : Type v} [inst_1 : CommRing X] [inst_2 : Bialgebra R X] [inst_3 : CommRing Y]
  [inst_4 : Bialgebra R Y] (i : CommBialgCat.of R X ≅ CommBialgCat.of R Y),
  CommBialgCat.isoEquivBialgEquiv i = CommBialgCat.bialgEquivOfIso i
-- Mathlib.Algebra.Order.Floor.Ring
natCast_floor_eq_intCast_floor : ∀ {R : Type u_2} [inst : Ring R] [inst_1 : LinearOrder R] [inst_2 : FloorRing R] {a : R}, 0 ≤ a → ↑⌊a⌋₊ = ↑⌊a⌋
-- Mathlib.Algebra.Group.Submonoid.Membership
Submonoid.induction_of_closure_eq_top_left : ∀ {M : Type u_1} [inst : Monoid M] {s : Set M} {motive : M → Prop},
  Submonoid.closure s = ⊤ → ∀ (x : M), motive 1 → (∀ x ∈ s, ∀ (y : M), motive y → motive (x * y)) → motive x
-- Mathlib.CategoryTheory.Sites.Sieves
CategoryTheory.Sieve.functorPushforward_apply : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  (F : CategoryTheory.Functor C D) {X : C} (R : CategoryTheory.Sieve X),
  (CategoryTheory.Sieve.functorPushforward F R).arrows = CategoryTheory.Presieve.functorPushforward F R.arrows
-- Mathlib.RingTheory.SimpleModule.Isotypic
IsIsotypicOfType.of_injective : ∀ {R : Type u_2} {M : Type u} {N : Type u_3} {S : Type u_4} [inst : Ring R] [inst_1 : AddCommGroup M]
  [inst_2 : AddCommGroup N] [inst_3 : AddCommGroup S] [inst_4 : Module R M] [inst_5 : Module R N] [inst_6 : Module R S],
  IsIsotypicOfType R N S → ∀ (f : M →ₗ[R] N), Function.Injective ⇑f → IsIsotypicOfType R M S
-- Mathlib.CategoryTheory.Sites.Hypercover.Homotopy
CategoryTheory.PreOneHypercover.sieve₁'_cylinder : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {S : C} {E : CategoryTheory.PreOneHypercover S}
  {F : CategoryTheory.PreOneHypercover S} [inst_1 : CategoryTheory.Limits.HasPullbacks C] (f g : E.Hom F)
  (i j : (i : E.I₀) × F.I₁ (f.s₀ i) (g.s₀ i)),
  (CategoryTheory.PreOneHypercover.cylinder f g).sieve₁' i j =
    CategoryTheory.Sieve.pullback
      (CategoryTheory.Limits.pullback.map ((CategoryTheory.PreOneHypercover.cylinder f g).f i)
        ((CategoryTheory.PreOneHypercover.cylinder f g).f j) (E.f i.fst) (E.f j.fst)
        (CategoryTheory.Limits.pullback.fst (CategoryTheory.Limits.pullback.lift (f.h₀ i.fst) (g.h₀ i.fst) ⋯)
          (F.toPullback i.snd))
        (CategoryTheory.Limits.pullback.fst (CategoryTheory.Limits.pullback.lift (f.h₀ j.fst) (g.h₀ j.fst) ⋯)
          (F.toPullback j.snd))
        (CategoryTheory.CategoryStruct.id S) ⋯ ⋯)
      (E.sieve₁' i.fst j.fst)
-- Mathlib.RingTheory.Morita.Basic
IsMoritaEquivalent.of_algEquiv : ∀ (R : Type u₀) [inst : CommSemiring R] {A : Type u₁} [inst_1 : Ring A] [inst_2 : Algebra R A] {B : Type u₂}
  [inst_3 : Ring B] [inst_4 : Algebra R B] (f : A ≃ₐ[R] B), IsMoritaEquivalent R A B
-- Mathlib.Combinatorics.SimpleGraph.Connectivity.Subgraph
SimpleGraph.Subgraph.Connected.preconnected : ∀ {V : Type u} {G : SimpleGraph V} {H : G.Subgraph}, H.Connected → H.Preconnected
-- Mathlib.Logic.Function.Basic
Function.hasUncurryBase : {α : Type u_1} → {β : Type u_2} → Function.HasUncurry (α → β) α β
-- Aesop.Forward.State
/-- Match hypothesis `hyp` against the slot with index `slot` in `cs` (which
must be a valid index).  -/
Aesop.ClusterState.matchPremise? : Array Lean.MVarId →
  Array Lean.LMVarId → Aesop.ClusterState → Aesop.SlotIndex → Lean.FVarId → Aesop.BaseM (Option Aesop.Substitution)
-- Mathlib.NumberTheory.LegendreSymbol.GaussEisensteinLemmas
/-- Each of the sums in this lemma is the cardinality of the set of integer points in each of the
two triangles formed by the diagonal of the rectangle `(0, p/2) × (0, q/2)`. Adding them
gives the number of points in the rectangle.  -/
ZMod.sum_mul_div_add_sum_mul_div_eq_mul : ∀ (p q : ℕ) [hp : Fact (Nat.Prime p)],
  ↑q ≠ 0 → ∑ a ∈ Finset.Ico 1 (p / 2).succ, a * q / p + ∑ a ∈ Finset.Ico 1 (q / 2).succ, a * p / q = p / 2 * (q / 2)
-- Mathlib.Probability.Martingale.Upcrossing
MeasureTheory.upcrossingStrat_nonneg : ∀ {Ω : Type u_1} {a b : ℝ} {f : ℕ → Ω → ℝ} {N n : ℕ} {ω : Ω}, 0 ≤ MeasureTheory.upcrossingStrat a b f N n ω
-- Init.Data.String.Lemmas.Order
String.Slice.Pos.sliceFrom_lt_iff : ∀ {s : String.Slice} {p₀ : s.Pos} {p : (s.sliceFrom p₀).Pos} {q : s.Pos} {h : p₀ ≤ q},
  p₀.sliceFrom q h < p ↔ q < String.Slice.Pos.ofSliceFrom p
-- Mathlib.Combinatorics.Enumerative.DyckWord
DyckWord.denest.congr_simp : ∀ (p p_1 : DyckWord) (e_p : p = p_1) (hn : p.IsNested), p.denest hn = p_1.denest ⋯
-- Mathlib.Topology.UrysohnsLemma
Urysohns.CU.lim_eq_midpoint : ∀ {X : Type u_1} [inst : TopologicalSpace X] {P : Set X → Set X → Prop} (c : Urysohns.CU P) (x : X),
  c.lim x = midpoint ℝ (c.left.lim x) (c.right.lim x)
-- Mathlib.Algebra.Module.Submodule.Equiv
Submodule.equivSubtypeMap_symm_apply : ∀ {R : Type u_1} {M : Type u_5} [inst : Semiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M] {p : Submodule R M}
  {q : Submodule R ↥p} (x : ↥(Submodule.map p.subtype q)), ↑↑((p.equivSubtypeMap q).symm x) = ↑x
-- Mathlib.CategoryTheory.Action.Basic
CategoryTheory.Functor.instFullActionMapActionOfFaithful : ∀ {V : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} V] {W : Type u_2}
  [inst_1 : CategoryTheory.Category.{v_2, u_2} W] (F : CategoryTheory.Functor V W) (G : Type u_3) [inst_2 : Monoid G]
  [F.Faithful] [F.Full], (F.mapAction G).Full
-- Mathlib.Algebra.Category.Grp.Colimits
/-- Inclusion of `F.obj j` into the candidate colimit.
 -/
AddCommGrpCat.Colimits.Quot.ι : {J : Type u} →
  [inst : CategoryTheory.Category.{v, u} J] →
    (F : CategoryTheory.Functor J AddCommGrpCat) →
      [inst_1 : DecidableEq J] → (j : J) → ↑(F.obj j) →+ AddCommGrpCat.Colimits.Quot F
-- Mathlib.Geometry.Convex.Cone.Face.Basic
/-- The image of a face of a cone under an equivalence is a face of the image of the cone.  -/
PointedCone.IsFaceOf.map_equiv : ∀ {R : Type u_1} {M : Type u_2} {N : Type u_3} [inst : Semiring R] [inst_1 : PartialOrder R] [inst_2 : IsOrderedRing R]
  [inst_3 : AddCommGroup M] [inst_4 : Module R M] {C F : PointedCone R M} [inst_5 : AddCommGroup N]
  [inst_6 : Module R N] (e : M ≃ₗ[R] N), F.IsFaceOf C → (PointedCone.map (↑e) F).IsFaceOf (PointedCone.map (↑e) C)
-- Mathlib.Topology.Compactification.StoneCech
instT2SpaceStoneCech : ∀ {α : Type u} [inst : TopologicalSpace α], T2Space (StoneCech α)
-- Lean.Meta.CongrTheorems
Lean.Meta.mkHCongrWithArity : Lean.Expr → ℕ → Lean.MetaM Lean.Meta.CongrTheorem
-- Mathlib.Algebra.Category.Ring.Colimits
RingCat.Colimits.descFunLift.eq_4 : ∀ {J : Type v} [inst : CategoryTheory.SmallCategory J] (F : CategoryTheory.Functor J RingCat)
  (s : CategoryTheory.Limits.Cocone F) (x_1 : RingCat.Colimits.Prequotient F),
  RingCat.Colimits.descFunLift F s x_1.neg = -RingCat.Colimits.descFunLift F s x_1