mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Analysis.Calculus.LineDeriv.Basic
HasLineDerivAt.tendsto_slope_zero_right : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {F : Type u_2} [inst_1 : NormedAddCommGroup F]
  [inst_2 : NormedSpace 𝕜 F] {E : Type u_3} [inst_3 : AddCommGroup E] [inst_4 : Module 𝕜 E] {f : E → F} {f' : F}
  {x v : E} [inst_5 : Preorder 𝕜],
  HasLineDerivAt 𝕜 f f' x v → Filter.Tendsto (fun t => t⁻¹ • (f (x + t • v) - f x)) (nhdsWithin 0 (Set.Ioi 0)) (nhds f')
-- Mathlib.Algebra.Module.TransferInstance
/-- The module instance from `AddEquiv.module` is compatible with the `R`-module structures,
if the `AddEquiv` is induced by an `R`-module isomorphism.  -/
LinearEquiv.isScalarTower : ∀ {R : Type u_1} {α : Type u_2} {β : Type u_3} [inst : Semiring R] (A : Type u_4) [inst_1 : Semiring A]
  [inst_2 : Module R A] [inst_3 : AddCommMonoid α] [inst_4 : AddCommMonoid β] [inst_5 : Module A β]
  [inst_6 : Module R α] [inst_7 : Module R β] [IsScalarTower R A β] (e : α ≃ₗ[R] β), IsScalarTower R A α
-- Mathlib.AlgebraicTopology.SimplicialSet.CategoryWithFibrations
/-- The fibrations for the Quillen model category structure (TODO)
on `SSet` are the morphisms which have the right lifting property
with respect to horn inclusions.  -/
SSet.modelCategoryQuillen.instCategoryWithFibrations : HomotopicalAlgebra.CategoryWithFibrations SSet
-- Mathlib.NumberTheory.NumberField.InfinitePlace.Basic
NumberField.InfinitePlace.mk_conjugate_eq : ∀ {K : Type u_1} [inst : Field K] (φ : K →+* ℂ),
  NumberField.InfinitePlace.mk (NumberField.ComplexEmbedding.conjugate φ) = NumberField.InfinitePlace.mk φ
-- Mathlib.CategoryTheory.Pi.Monoidal
CategoryTheory.Pi.braiding_hom_apply : ∀ {I : Type w₁} {C : I → Type u₁} [inst : (i : I) → CategoryTheory.Category.{v₁, u₁} (C i)]
  [inst_1 : (i : I) → CategoryTheory.MonoidalCategory (C i)] [inst_2 : (i : I) → CategoryTheory.BraidedCategory (C i)]
  {X Y : (i : I) → C i} {i : I}, (β_ X Y).hom i = (β_ (X i) (Y i)).hom
-- Init.Classical
Classical.epsilon_spec : ∀ {α : Sort u} {p : α → Prop} (hex : ∃ y, p y), p (Classical.epsilon p)
-- Mathlib.Algebra.Category.Semigrp.Basic
/-- Typecheck a `MulHom` as a morphism in `MagmaCat`.  -/
MagmaCat.ofHom : {X Y : Type u} → [inst : Mul X] → [inst_1 : Mul Y] → (X →ₙ* Y) → (MagmaCat.of X ⟶ MagmaCat.of Y)
-- Lean.Meta.Instances
Lean.Meta.synthInstance.checkSynthOrder : Lean.Option Bool
-- Mathlib.Topology.Algebra.InfiniteSum.SummationFilter
SummationFilter.comap.eq_1 : ∀ {β : Type u_2} {γ : Type u_3} (L : SummationFilter β) (f : γ ↪ β),
  L.comap f = { filter := Filter.map (fun s => s.preimage ⇑f ⋯) L.filter }
-- Std.Data.HashMap.Lemmas
Std.HashMap.keys_emptyWithCapacity : ∀ {α : Type u} {β : Type v} {x : BEq α} {x_1 : Hashable α} {c : ℕ}, (Std.HashMap.emptyWithCapacity c).keys = []
-- Mathlib.CategoryTheory.MorphismProperty.Factorization
CategoryTheory.MorphismProperty.FunctorialFactorizationData.mapZ_id : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] {W₁ W₂ : CategoryTheory.MorphismProperty C}
  (data : W₁.FunctorialFactorizationData W₂) {X Y : C} (f : X ⟶ Y),
  data.mapZ (CategoryTheory.CategoryStruct.id (CategoryTheory.Arrow.mk f)) =
    CategoryTheory.CategoryStruct.id (data.factorizationData f).Z
-- Mathlib.CategoryTheory.Limits.FunctorCategory.Shapes.Pullbacks
/-- The pullback cone `combinePullbackCones` is limiting.
 -/
CategoryTheory.Limits.PullbackCone.combineIsLimit : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    {D : Type u₂} →
      [inst_1 : CategoryTheory.Category.{v₂, u₂} D] →
        {F G H : CategoryTheory.Functor D C} →
          (f : F ⟶ H) →
            (g : G ⟶ H) →
              (c : (X : D) → CategoryTheory.Limits.PullbackCone (f.app X) (g.app X)) →
                (hc : (X : D) → CategoryTheory.Limits.IsLimit (c X)) →
                  CategoryTheory.Limits.IsLimit (CategoryTheory.Limits.PullbackCone.combine f g c hc)
-- Init.Data.SInt.Basic
instReprAtomInt16 : ReprAtom Int16
-- Mathlib.Combinatorics.Matroid.Rank.ENat
Matroid.IsBasis.eRk_eq_eRk_union : ∀ {α : Type u_1} {M : Matroid α} {I X : Set α}, M.IsBasis I X → ∀ (Y : Set α), M.eRk (I ∪ Y) = M.eRk (X ∪ Y)
-- Mathlib.RingTheory.RamificationInertia.Inertia
Ideal.inertiaDeg_smul : ∀ (R : Type u_1) {S : Type u_2} [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : Algebra R S] (q : Ideal S)
  {G : Type u_4} [inst_3 : Group G] [inst_4 : MulSemiringAction G S] [SMulCommClass G R S] (g : G),
  (g • q).inertiaDeg R = q.inertiaDeg R
-- Mathlib.CategoryTheory.Monoidal.Free.Basic
CategoryTheory.FreeMonoidalCategory.HomEquiv.ρ_inv_hom : ∀ {C : Type u} {X : CategoryTheory.FreeMonoidalCategory C},
  CategoryTheory.FreeMonoidalCategory.HomEquiv
    ((CategoryTheory.FreeMonoidalCategory.Hom.ρ_inv X).comp (CategoryTheory.FreeMonoidalCategory.Hom.ρ_hom X))
    (CategoryTheory.FreeMonoidalCategory.Hom.id X)
-- Mathlib.Analysis.PSeries
NNReal.summable_one_div_rpow : ∀ {p : ℝ}, (Summable fun n => 1 / ↑n ^ p) ↔ 1 < p
-- Mathlib.Algebra.Algebra.Unitization
Unitization.instNonAssocSemiring : {R : Type u_1} →
  {A : Type u_2} →
    [inst : Semiring R] → [inst_1 : NonUnitalNonAssocSemiring A] → [Module R A] → NonAssocSemiring (Unitization R A)
-- Mathlib.MeasureTheory.VectorMeasure.Variation.SignedMeasure
/-- The pointwise bound `‖s i‖ ≤ s.totalVariation.real i` for any signed measure.  -/
MeasureTheory.SignedMeasure.norm_le_totalVariation : ∀ {X : Type u_1} {mX : MeasurableSpace X} (s : MeasureTheory.SignedMeasure X) (i : Set X),
  ‖s i‖ ≤ s.totalVariation.real i
-- Init.WFTactics
/-- `decreasing_tactic` is called by default on well-founded recursions in order
to synthesize a proof that recursive calls decrease along the selected
well founded relation. It can be locally overridden by using `decreasing_by tac`
on the recursive definition, and it can also be globally extended by adding
more definitions for `decreasing_tactic` (or `decreasing_trivial`,
which this tactic calls).  -/
tacticDecreasing_tactic : Lean.ParserDescr
-- Mathlib.Algebra.Order.Monoid.Unbundled.Basic
mul_lt_mul_left : ∀ {α : Type u_1} [inst : Mul α] [inst_1 : LT α] [i : MulRightStrictMono α] {b c : α}, b < c → ∀ (a : α), b * a < c * a
-- Mathlib.Tactic.Translate.Core
/-- Warn the user when the declaration has a simple scoped attribute.  -/
Mathlib.Tactic.Translate.warnAttr : {α β : Type} →
  [Inhabited β] →
    Lean.Syntax →
      Lean.SimpleScopedEnvExtension α β →
        (β → Lean.Name → Bool) → Lean.Name → Lean.Name → Lean.Name → Lean.Name → Lean.CoreM Unit
-- Mathlib.Order.MinMax
min_left_commutative : ∀ {α : Type u} [inst : LinearOrder α], LeftCommutative min
-- Init.Internal.Order.Basic
Lean.Order.instCCPOIO : {α : Type} → Lean.Order.CCPO (IO α)
-- Mathlib.Topology.Algebra.Module.ClosedSubmodule
ClosedSubmodule.mapEquiv_symm : ∀ {R : Type u_2} {M : Type u_3} {N : Type u_4} [inst : Semiring R] [inst_1 : AddCommMonoid M]
  [inst_2 : TopologicalSpace M] [inst_3 : Module R M] [inst_4 : AddCommMonoid N] [inst_5 : TopologicalSpace N]
  [inst_6 : Module R N] (f : M ≃L[R] N), ClosedSubmodule.mapEquiv f.symm = (ClosedSubmodule.mapEquiv f).symm
-- Mathlib.SetTheory.Cardinal.Regular
Cardinal.IsInaccessible.nat_lt : ∀ {c : Cardinal.{u_1}}, c.IsInaccessible → ∀ (n : ℕ), ↑n < c
-- Init.Data.List.ControlImpl
_private.Init.Data.List.ControlImpl.0.List.flatMapMTR.match_1.eq_2 : ∀ {α : Type u_1} {β : Type u_2} (motive : List α → List (List β) → Sort u_3) (a : α) (as : List α) (bs : List (List β))
  (h_1 : (bs : List (List β)) → motive [] bs)
  (h_2 : (a : α) → (as : List α) → (bs : List (List β)) → motive (a :: as) bs),
  (match a :: as, bs with
    | [], bs => h_1 bs
    | a :: as, bs => h_2 a as bs) =
    h_2 a as bs
-- Init.Data.String.Slice
_private.Init.Data.String.Slice.0.String.Slice.RevSplitIterator.instIteratorOfPure.match_3.eq_2 : ∀ {ρ : Type} {ρ_1 : ρ} {σ : String.Slice → Type} [inst : String.Slice.Pattern.ToBackwardSearcher ρ_1 σ]
  {m : Type → Type u_1} {s : String.Slice} (motive : Std.IterM m String.Slice → Sort u_2)
  (h_1 :
    (currPos : s.Pos) →
      (searcher : Std.Iter (String.Slice.Pattern.SearchStep s)) →
        motive { internalState := String.Slice.RevSplitIterator.operating currPos searcher })
  (h_2 : Unit → motive { internalState := String.Slice.RevSplitIterator.atEnd }),
  (match { internalState := String.Slice.RevSplitIterator.atEnd } with
    | { internalState := String.Slice.RevSplitIterator.operating currPos searcher } => h_1 currPos searcher
    | { internalState := String.Slice.RevSplitIterator.atEnd } => h_2 ()) =
    h_2 ()
-- Mathlib.AlgebraicTopology.SimplicialObject.Split
CategoryTheory.SimplicialObject.Splitting.IndexSet.epiComp_snd_coe : ∀ {Δ₁ Δ₂ : SimplexCategoryᵒᵖ} (A : CategoryTheory.SimplicialObject.Splitting.IndexSet Δ₁) (p : Δ₁ ⟶ Δ₂)
  [inst : CategoryTheory.Epi p.unop], ↑(A.epiComp p).snd = CategoryTheory.CategoryStruct.comp p.unop A.e
-- Std.Tactic.BVDecide.Bitblast.BVExpr.Circuit.Lemmas.Operations.Extract
Std.Tactic.BVDecide.BVExpr.bitblast.blastExtract.go_get_aux : ∀ {α : Type} [inst : Hashable α] [inst_1 : DecidableEq α] {w newWidth : ℕ} (aig : Std.Sat.AIG α) (input : aig.RefVec w)
  (lo curr : ℕ) (hcurr : curr ≤ newWidth) (s : aig.RefVec curr) (idx : ℕ) (hidx1 : idx < curr),
  (Std.Tactic.BVDecide.BVExpr.bitblast.blastExtract.go input lo curr hcurr s).get idx ⋯ = s.get idx hidx1
-- Mathlib.Order.ConditionallyCompleteLattice.Finset
Set.Nonempty.csSup_mem : ∀ {α : Type u_2} [inst : ConditionallyCompleteLinearOrder α] {s : Set α}, s.Nonempty → s.Finite → sSup s ∈ s
-- Lean.Meta.Constructions.CtorElim
_private.Lean.Meta.Constructions.CtorElim.0.Lean.mkCtorElimType : Lean.Name → Lean.MetaM Unit
-- Mathlib.RingTheory.Valuation.Extension
Valuation.HasExtension.algebraMap_mem_valuationSubring : ∀ {K : outParam (Type u_5)} {L : outParam (Type u_6)} {Γ₀ : outParam (Type u_7)} {Γ₁ : outParam (Type u_8)}
  [inst : Field K] [inst_1 : Field L] [inst_2 : Algebra K L] [inst_3 : LinearOrderedCommGroupWithZero Γ₀]
  [inst_4 : LinearOrderedCommGroupWithZero Γ₁] (vK : Valuation K Γ₀) (vL : Valuation L Γ₁) [vK.HasExtension vL]
  (x : ↥vK.valuationSubring), (algebraMap K L) ↑x ∈ vL.valuationSubring
-- Init.Data.Fin.Bitwise
Fin.or_val_of_uSizeSize : ∀ (a b : Fin USize.size), ↑(a ||| b) = ↑a ||| ↑b
-- Mathlib.Analysis.Normed.Algebra.TrivSqZeroExt
TrivSqZeroExt.fst_expSeries : ∀ (𝕜 : Type u_1) {R : Type u_3} {M : Type u_4} [inst : Field 𝕜] [inst_1 : Ring R] [inst_2 : AddCommGroup M]
  [inst_3 : Algebra 𝕜 R] [inst_4 : Module 𝕜 M] [inst_5 : Module R M] [inst_6 : Module Rᵐᵒᵖ M]
  [inst_7 : SMulCommClass R Rᵐᵒᵖ M] [inst_8 : IsScalarTower 𝕜 R M] [inst_9 : IsScalarTower 𝕜 Rᵐᵒᵖ M]
  [inst_10 : TopologicalSpace R] [inst_11 : TopologicalSpace M] [inst_12 : IsTopologicalRing R]
  [inst_13 : IsTopologicalAddGroup M] [inst_14 : ContinuousSMul R M] [inst_15 : ContinuousSMul Rᵐᵒᵖ M]
  (x : TrivSqZeroExt R M) (n : ℕ),
  ((NormedSpace.expSeries 𝕜 (TrivSqZeroExt R M) n) fun x_1 => x).fst = (NormedSpace.expSeries 𝕜 R n) fun x_1 => x.fst
-- Mathlib.Data.List.Lattice
/-- **Alias** of `List.cons_bagInter_of_not_mem`. -/
List.cons_bagInter_of_neg : ∀ {α : Type u_1} {l₂ : List α} {a : α} [inst : DecidableEq α] (l₁ : List α),
  a ∉ l₂ → (a :: l₁).bagInter l₂ = l₁.bagInter l₂
-- Lean.PrettyPrinter.Delaborator.SubExpr
Lean.PrettyPrinter.Delaborator.SubExpr.HoleIterator.next : Lean.PrettyPrinter.Delaborator.SubExpr.HoleIterator → Lean.PrettyPrinter.Delaborator.SubExpr.HoleIterator
-- Mathlib.Order.Std
/-- ≤ forms a partial order.  -/
PartialOrder.OfStdArgs.isPartialOrder : ∀ {α : Type u_1} (self : PartialOrder.OfStdArgs α),
  let this := self.le;
  Std.IsPartialOrder α
-- Mathlib.Data.W.Constructions
_private.Mathlib.Data.W.Constructions.0.WType.ofList.match_1.splitter : (γ : Type u_1) →
  (motive : List γ → Sort u_2) →
    (x : List γ) → (Unit → motive []) → ((hd : γ) → (tl : List γ) → motive (hd :: tl)) → motive x
-- Mathlib.MeasureTheory.Measure.Typeclasses.SFinite
/-- Auxiliary lemma for `iSup_restrict_spanningSets`.  -/
MeasureTheory.Measure.iSup_restrict_spanningSets_of_measurableSet : ∀ {α : Type u_1} {m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} {s : Set α}
  [inst : MeasureTheory.SigmaFinite μ], MeasurableSet s → ⨆ i, (μ.restrict (MeasureTheory.spanningSets μ i)) s = μ s
-- Mathlib.Data.Finsupp.WellFounded
Finsupp.Lex.wellFounded_of_finite : ∀ {α : Type u_1} {N : Type u_2} [inst : Zero N] (r : α → α → Prop) {s : N → N → Prop} [IsStrictTotalOrder α r]
  [Finite α], WellFounded s → WellFounded (Finsupp.Lex r s)
-- Mathlib.Algebra.Order.Kleene
kstar_eq_self : ∀ {α : Type u_1} [inst : KleeneAlgebra α] {a : α}, KStar.kstar a = a ↔ a * a = a ∧ 1 ≤ a
-- Batteries.Lean.NameMapAttribute
Lean.NameMapAttributeImpl.mk.sizeOf_spec : ∀ {α : Type} [inst : SizeOf α] (name : Lean.Name) (ref : autoParam Lean.Name Lean.NameMapAttributeImpl.ref._autoParam)
  (descr : String) (add : Lean.Name → Lean.Syntax → Lean.AttrM α),
  sizeOf { name := name, ref := ref, descr := descr, add := add } = 1 + sizeOf name + sizeOf ref + sizeOf descr
-- Mathlib.Logic.Equiv.Fin.Basic
Fin.preimage_apply_01_prod : ∀ {α : Fin 2 → Type u} (s : Set (α 0)) (t : Set (α 1)),
  (fun f => (f 0, f 1)) ⁻¹' s ×ˢ t = Set.univ.pi (Fin.cons s (Fin.cons t finZeroElim))
-- Mathlib.Algebra.BigOperators.Group.Finset.Interval
Finset.prod_Icc_of_even_eq_range : ∀ {α : Type u_1} [inst : CommGroup α] {f : ℤ → α},
  Function.Even f → ∀ (N : ℕ), ∏ m ∈ Finset.Icc (-↑N) ↑N, f m = (∏ m ∈ Finset.range (N + 1), f ↑m) ^ 2 / f 0
-- Mathlib.Tactic.LinearCombination.Lemmas
Mathlib.Tactic.LinearCombination.smul_const_eq : ∀ {α : Type u_1} {b c : α} {K : Type u_2} [inst : SMul K α], b = c → ∀ (s : K), s • b = s • c
-- Mathlib.Analysis.Complex.Trigonometric
Complex.sinh_sq : ∀ (x : ℂ), Complex.sinh x ^ 2 = Complex.cosh x ^ 2 - 1
-- Init.Tactics
/-- `infer_instance` is an abbreviation for `exact inferInstance`.
It synthesizes a value of any target type by typeclass inference.
 -/
Lean.Parser.Tactic.tacticInfer_instance : Lean.ParserDescr
-- Mathlib.NumberTheory.Dioph
Poly.instFunLike : {α : Type u_1} → FunLike (Poly α) (α → ℕ) ℤ
-- Init.Data.Range.Polymorphic.NatLemmas
Nat.getElem!_toArray_rco : ∀ {m n i : ℕ}, (m...n).toArray[i]! = if i < n - m then m + i else 0
-- Std.Data.DHashMap.Lemmas
Std.DHashMap.Const.getKey?_insertMany_list_of_mem : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} {β : Type v} {m : Std.DHashMap α fun x => β} [EquivBEq α]
  [LawfulHashable α] {l : List (α × β)} {k k' : α},
  (k == k') = true →
    List.Pairwise (fun a b => (a.1 == b.1) = false) l →
      k ∈ List.map Prod.fst l → (Std.DHashMap.Const.insertMany m l).getKey? k' = some k
-- Mathlib.RingTheory.DedekindDomain.AdicValuation
/-- The `v`-adic absolute value function on `R` defined as `b` raised to negative `v`-adic
valuation, for some `b` in `ℝ≥0`  -/
IsDedekindDomain.HeightOneSpectrum.intAdicAbvDef : {R : Type u_1} →
  [inst : CommRing R] → [IsDedekindDomain R] → IsDedekindDomain.HeightOneSpectrum R → {b : NNReal} → 1 < b → R → NNReal
-- Mathlib.CategoryTheory.Limits.Types.Colimits
CategoryTheory.Limits.Types.jointly_surjective_of_isColimit : ∀ {J : Type v} [inst : CategoryTheory.Category.{w, v} J] {F : CategoryTheory.Functor J (Type u)}
  {t : CategoryTheory.Limits.Cocone F} (h : CategoryTheory.Limits.IsColimit t) (x : t.pt),
  ∃ j y, (CategoryTheory.ConcreteCategory.hom (t.ι.app j)) y = x
-- Mathlib.Analysis.Convex.Segment
Nonneg.Icc_subset_segment : ∀ {𝕜 : Type u_1} [inst : Field 𝕜] [inst_1 : LinearOrder 𝕜] [inst_2 : IsStrictOrderedRing 𝕜] {x y : { t // 0 ≤ t }},
  Set.Icc x y ⊆ segment { t // 0 ≤ t } x y
-- Mathlib.Algebra.Order.Monoid.Unbundled.Pow
nsmul_neg_iff : ∀ {M : Type u_3} [inst : AddMonoid M] [inst_1 : LinearOrder M] [AddLeftMono M] {x : M} {n : ℕ},
  n ≠ 0 → (n • x < 0 ↔ x < 0)
-- Lean.Meta.Tactic.Grind.Parser
Lean.Parser.Command.GrindCnstr.sizeLt.parenthesizer : Lean.PrettyPrinter.Parenthesizer
-- Mathlib.Tactic.ITauto
Mathlib.Tactic.ITauto.Proof.andRight.inj : ∀ {ak : Mathlib.Tactic.ITauto.AndKind} {p : Mathlib.Tactic.ITauto.Proof} {ak_1 : Mathlib.Tactic.ITauto.AndKind}
  {p_1 : Mathlib.Tactic.ITauto.Proof},
  Mathlib.Tactic.ITauto.Proof.andRight ak p = Mathlib.Tactic.ITauto.Proof.andRight ak_1 p_1 → ak = ak_1 ∧ p = p_1
-- Mathlib.RingTheory.Algebraic.Basic
is_transcendental_of_subsingleton : ∀ (R : Type u) {A : Type v} [inst : CommRing R] [inst_1 : Ring A] [inst_2 : Algebra R A] [Subsingleton R] (x : A),
  Transcendental R x
-- Mathlib.LinearAlgebra.RootSystem.RootPositive
/-- The bilinear form bundled inside a `RootPositiveForm`.  -/
RootPairing.RootPositiveForm.form : {ι : Type u_1} →
  {R : Type u_2} →
    {S : Type u_3} →
      {M : Type u_4} →
        {N : Type u_5} →
          [inst : CommRing S] →
            [inst_1 : LinearOrder S] →
              [inst_2 : CommRing R] →
                [inst_3 : Algebra S R] →
                  [inst_4 : AddCommGroup M] →
                    [inst_5 : Module R M] →
                      [inst_6 : AddCommGroup N] →
                        [inst_7 : Module R N] →
                          {P : RootPairing ι R M N} →
                            [inst_8 : P.IsValuedIn S] → RootPairing.RootPositiveForm S P → LinearMap.BilinForm R M
-- Mathlib.Algebra.Category.ModuleCat.Topology.Basic
TopModuleCat.free_obj : ∀ (R : Type u) [inst : Ring R] [inst_1 : TopologicalSpace R] (X : TopCat),
  (TopModuleCat.free R).obj X = TopModuleCat.freeObj R X
-- Mathlib.Data.Set.Basic
Set.union_eq_right : ∀ {α : Type u} {s t : Set α}, s ∪ t = t ↔ s ⊆ t
-- Mathlib.Combinatorics.SetFamily.Compression.Down
Finset.memberSubfamily_memberSubfamily : ∀ {α : Type u_1} [inst : DecidableEq α] {𝒜 : Finset (Finset α)} {a : α},
  Finset.memberSubfamily a (Finset.memberSubfamily a 𝒜) = ∅
-- Mathlib.Probability.Process.Stopping
MeasureTheory.IsStoppingTime.sigmaFinite_stopping_time : ∀ {Ω : Type u_1} {m : MeasurableSpace Ω} {ι : Type u_4} [inst : SemilatticeSup ι] [OrderBot ι]
  {μ : MeasureTheory.Measure Ω} {f : MeasureTheory.Filtration ι m} {τ : Ω → WithTop ι}
  [MeasureTheory.SigmaFiniteFiltration μ f] (hτ : MeasureTheory.IsStoppingTime f τ),
  MeasureTheory.SigmaFinite (μ.trim ⋯)
-- Mathlib.GroupTheory.GroupAction.Transitive
/-- An action of a group is pretransitive iff any element can be moved from a fixed given one.  -/
MulAction.isPretransitive_iff_base : ∀ {G : Type u_1} {X : Type u_2} [inst : Group G] [inst_1 : MulAction G X] (a : X),
  MulAction.IsPretransitive G X ↔ ∀ (x : X), ∃ g, g • a = x
-- Init.Data.String.Decode
ByteArray.utf8DecodeChar?.FirstByte.oneMore.sizeOf_spec : sizeOf ByteArray.utf8DecodeChar?.FirstByte.oneMore = 1
-- Mathlib.RingTheory.RingHom.Flat
/-- The identity of a ring is flat.  -/
RingHom.Flat.id : ∀ (R : Type u_1) [inst : CommRing R], (RingHom.id R).Flat
-- Mathlib.CategoryTheory.Equivalence
CategoryTheory.Equivalence.counitIso_functor_comp : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  (e : C ≌ D) (X : C),
  CategoryTheory.CategoryStruct.comp (e.counitIso.inv.app (e.functor.obj X)) (e.functor.map (e.unitIso.inv.app X)) =
    CategoryTheory.CategoryStruct.id (e.functor.obj X)
-- Mathlib.CategoryTheory.Limits.Shapes.Products
/-- **Alias** of `CategoryTheory.Limits.Cofan.IsColimit.mk`.

---

Make a cofan `f` into a colimit cofan by providing `desc`, `fac`, and `uniq` --
just a convenience lemma to avoid having to go through `Discrete`  -/
CategoryTheory.Limits.mkCofanColimit : {β : Type w} →
  {C : Type u} →
    [inst : CategoryTheory.Category.{v, u} C] →
      {f : β → C} →
        (s : CategoryTheory.Limits.Cofan f) →
          (desc : (t : CategoryTheory.Limits.Cofan f) → s.pt ⟶ t.pt) →
            autoParam
                (∀ (t : CategoryTheory.Limits.Cofan f) (j : β),
                  CategoryTheory.CategoryStruct.comp (s.inj j) (desc t) = t.inj j)
                CategoryTheory.Limits.Cofan.IsColimit.mk._auto_1 →
              autoParam
                  (∀ (t : CategoryTheory.Limits.Cofan f) (m : s.pt ⟶ t.pt),
                    (∀ (j : β), CategoryTheory.CategoryStruct.comp (s.inj j) m = t.inj j) → m = desc t)
                  CategoryTheory.Limits.Cofan.IsColimit.mk._auto_3 →
                CategoryTheory.Limits.IsColimit s
-- Mathlib.LinearAlgebra.Projection
/-- The linear projection onto a subspace along its complement is an idempotent.  -/
Submodule.isIdempotentElem_projection : ∀ {R : Type u_1} [inst : Ring R] {E : Type u_2} [inst_1 : AddCommGroup E] [inst_2 : Module R E] {p q : Submodule R E}
  (hpq : IsCompl p q), IsIdempotentElem (p.projection q hpq)
-- Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic
Real.pi_pos : 0 < Real.pi
-- Mathlib.GroupTheory.OrderOfElement
mem_zpowers_iff_mem_range_orderOf : ∀ {G : Type u_1} [inst : Group G] {x y : G} [Finite G] [inst_2 : DecidableEq G],
  y ∈ Subgroup.zpowers x ↔ y ∈ Finset.image (fun x_1 => x ^ x_1) (Finset.range (orderOf x))
-- Std.Data.Internal.List.Associative
Std.Internal.List.getKeyD_filter_containsKey_of_containsKey_right : ∀ {α : Type u} {β : α → Type v} [inst : BEq α] [EquivBEq α] {l₁ l₂ : List ((a : α) × β a)} {k fallback : α},
  Std.Internal.List.DistinctKeys l₁ →
    Std.Internal.List.containsKey k l₂ = true →
      Std.Internal.List.getKeyD k (List.filter (fun p => Std.Internal.List.containsKey p.fst l₂) l₁) fallback =
        Std.Internal.List.getKeyD k l₁ fallback
-- Mathlib.CategoryTheory.Localization.SmallHom
/-- This property holds if the type of morphisms between `X` and `Y`
in the localized category with respect to `W : MorphismProperty C`
is small.  -/
CategoryTheory.Localization.HasSmallLocalizedHom : {C : Type u₁} → [inst : CategoryTheory.Category.{v₁, u₁} C] → CategoryTheory.MorphismProperty C → C → C → Prop
-- Mathlib.Data.Multiset.AddSub
Multiset.count_add : ∀ {α : Type u_1} [inst : DecidableEq α] (a : α) (s t : Multiset α),
  Multiset.count a (s + t) = Multiset.count a s + Multiset.count a t
-- Mathlib.MeasureTheory.Integral.CircleIntegral
circleIntegral.integral_const_mul : ∀ (a : ℂ) (f : ℂ → ℂ) (c : ℂ) (R : ℝ), ∮ (z : ℂ) in C(c, R), a * f z = a * ∮ (z : ℂ) in C(c, R), f z
-- Init.Data.Int.Lemmas
Int.neg_mul : ∀ (a b : ℤ), -a * b = -(a * b)
-- Mathlib.RingTheory.Ideal.Pointwise
Ideal.stabilizerEquiv_apply_smul : ∀ {M : Type u_1} {R : Type u_3} [inst : Group M] [inst_1 : Semiring R] [inst_2 : MulSemiringAction M R] {N : Type u_4}
  [inst_3 : Group N] [inst_4 : MulSemiringAction N R] (I : Ideal R) (e : M ≃* N)
  (he : ∀ (m : M) (x : R), e m • x = m • x) (m : ↥(MulAction.stabilizer M I)) (x : R),
  (I.stabilizerEquiv e he) m • x = m • x
-- Mathlib.Analysis.Calculus.Deriv.Abs
not_differentiableAt_abs_zero : ¬DifferentiableAt ℝ abs 0
-- Lean.Meta.Tactic.FunIndCollect
Lean.Meta.FunInd.SeenCalls.isEmpty : Lean.Meta.FunInd.SeenCalls → Bool
-- Mathlib.Algebra.Lie.Submodule
/-- An equivalence of Lie modules yields an order-preserving equivalence of their lattices of Lie
Submodules.  -/
LieSubmodule.orderIsoMapComap : {R : Type u} →
  {L : Type v} →
    {M : Type w} →
      {M' : Type w₁} →
        [inst : CommRing R] →
          [inst_1 : LieRing L] →
            [inst_2 : AddCommGroup M] →
              [inst_3 : Module R M] →
                [inst_4 : LieRingModule L M] →
                  [inst_5 : AddCommGroup M'] →
                    [inst_6 : Module R M'] →
                      [inst_7 : LieRingModule L M'] → (M ≃ₗ⁅R,L⁆ M') → LieSubmodule R L M ≃o LieSubmodule R L M'
-- Std.Data.HashMap.Lemmas
Std.HashMap.contains_congr : ∀ {α : Type u} {β : Type v} {x : BEq α} {x_1 : Hashable α} {m : Std.HashMap α β} [EquivBEq α] [LawfulHashable α]
  {a b : α}, (a == b) = true → m.contains a = m.contains b
-- Mathlib.GroupTheory.PGroup
IsPGroup.to_sup_of_normal_right : ∀ {p : ℕ} {G : Type u_1} [inst : Group G] {H K : Subgroup G},
  IsPGroup p ↥H → IsPGroup p ↥K → ∀ [K.Normal], IsPGroup p ↥(H ⊔ K)
-- Mathlib.LinearAlgebra.SModEq.Basic
SModEq.mul : ∀ {A : Type u_3} [inst : CommRing A] {I : Ideal A} {x₁ x₂ y₁ y₂ : A},
  x₁ ≡ y₁ [SMOD I] → x₂ ≡ y₂ [SMOD I] → x₁ * x₂ ≡ y₁ * y₂ [SMOD I]
-- Init.Data.Vector.Lemmas
Vector.find?_toList : ∀ {α : Type} {n : ℕ} {p : α → Bool} {xs : Vector α n}, List.find? p xs.toList = Vector.find? p xs
-- Init.Data.BitVec.Lemmas
BitVec.shiftLeft_xor_distrib : ∀ {w : ℕ} (x y : BitVec w) (n : ℕ), (x ^^^ y) <<< n = x <<< n ^^^ y <<< n
-- Mathlib.Data.Int.Lemmas
Int.natAbs_lt_iff_sq_lt : ∀ {a b : ℤ}, a.natAbs < b.natAbs ↔ a ^ 2 < b ^ 2