mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.CategoryTheory.Triangulated.TStructure.AbelianSubcategory
CategoryTheory.Triangulated.AbelianSubcategory.hasCokernel : ∀ {C : Type u_1} {A : Type u_2} [inst : CategoryTheory.Category.{v_1, u_1} C]
  [inst_1 : CategoryTheory.Limits.HasZeroObject C] [inst_2 : CategoryTheory.Preadditive C]
  [inst_3 : CategoryTheory.HasShift C ℤ] [inst_4 : ∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive]
  [inst_5 : CategoryTheory.Pretriangulated C] [inst_6 : CategoryTheory.Category.{v_2, u_2} A]
  {ι : CategoryTheory.Functor A C},
  (∀ ⦃X Y : A⦄ ⦃n : ℤ⦄ (f : ι.obj X ⟶ (CategoryTheory.shiftFunctor C n).obj (ι.obj Y)), n < 0 → f = 0) →
    ∀ {X₁ X₂ : A} {f₁ : X₁ ⟶ X₂} {X₃ : C} {f₂ : ι.obj X₂ ⟶ X₃}
      {f₃ : X₃ ⟶ (CategoryTheory.shiftFunctor C 1).obj (ι.obj X₁)},
      CategoryTheory.Pretriangulated.Triangle.mk (ι.map f₁) f₂ f₃ ∈
          CategoryTheory.Pretriangulated.distinguishedTriangles →
        ∀ {K Q : A} {α : (CategoryTheory.shiftFunctor C 1).obj (ι.obj K) ⟶ X₃} {β : X₃ ⟶ ι.obj Q}
          {γ : ι.obj Q ⟶ (CategoryTheory.shiftFunctor C 1).obj ((CategoryTheory.shiftFunctor C 1).obj (ι.obj K))},
          CategoryTheory.Pretriangulated.Triangle.mk α β γ ∈ CategoryTheory.Pretriangulated.distinguishedTriangles →
            ∀ [ι.Full] [inst_8 : CategoryTheory.Preadditive A] [ι.Faithful], CategoryTheory.Limits.HasCokernel f₁
-- Mathlib.CategoryTheory.Comma.Arrow
CategoryTheory.Arrow.arrow_mk_comp_eqToHom : ∀ {T : Type u} [inst : CategoryTheory.Category.{v, u} T] {X Y Y' : T} (f : X ⟶ Y) (h : Y = Y'),
  CategoryTheory.Arrow.mk (CategoryTheory.CategoryStruct.comp f (CategoryTheory.eqToHom h)) = CategoryTheory.Arrow.mk f
-- Mathlib.Analysis.Convex.EGauge
egauge_empty : ∀ (𝕜 : Type u_1) [inst : NNNorm 𝕜] {E : Type u_2} [inst_1 : SMul 𝕜 E] (x : E), egauge 𝕜 ∅ x = ⊤
-- Mathlib.Algebra.Star.NonUnitalSubsemiring
/-- Reinterpret a `SubStarSemigroup` as a `Subsemigroup`.  -/
SubStarSemigroup.toSubsemigroup : {M : Type v} → [inst : Mul M] → [inst_1 : Star M] → SubStarSemigroup M → Subsemigroup M
-- Init.Data.List.Lemmas
List.getElem_set : ∀ {α : Type u_1} {l : List α} {i j : ℕ} {a : α} (h : j < (l.set i a).length), (l.set i a)[j] = if i = j then a else l[j]
-- Mathlib.Lean.Meta.RefinedDiscrTree.Basic
/-- The stack, used to emulate recursion. It contains the list of all expressions for which the
keys still need to be computed, in that order.

For example in `10.add (20.add 30)`, after computing the keys `⟨Nat.add, 2⟩` and `10`, the stack
will be a list of length 1 containing the expression `20.add 30`.
 -/
Lean.Meta.RefinedDiscrTree.LazyEntry.stack : Lean.Meta.RefinedDiscrTree.LazyEntry → List Lean.Meta.RefinedDiscrTree.StackEntry
-- Aesop.RuleTac.ElabRuleTerm
Aesop.elabGlobalRuleIdent? : Lean.Term → Lean.Elab.TermElabM (Option Lean.Name)
-- Mathlib.Order.Atoms
SetLike.isCoatom_iff : ∀ {A : Type u_4} {B : Type u_5} [inst : PartialOrder A] [inst_1 : SetLike A B] [IsConcreteLE A B] [inst_3 : OrderTop A]
  {K : A}, IsCoatom K ↔ K ≠ ⊤ ∧ ∀ (H : A) (g : B), K ≤ H → g ∉ K → g ∈ H → H = ⊤
-- Lean.DocString.Parser
/-- Parses a header.  -/
Lean.Doc.Parser.header : Lean.Doc.Parser.BlockCtxt → Lean.Parser.ParserFn
-- Mathlib.Data.Int.Order.Units
Int.neg_one_pow_ne_zero : ∀ {n : ℕ}, (-1) ^ n ≠ 0
-- Init.Data.Slice.List.Basic
/-- A region of some underlying list. List slices can be used to avoid copying or allocating space,
while being more convenient than tracking the bounds by hand.

A list slice only stores the suffix of the underlying list, starting from the range's lower bound
so that the cost of operations on the slice does not depend on the start position. However,
the cost of creating a list slice is linear in the start position.
 -/
ListSlice : Type u → Type u
-- Init.Data.List.Pairwise
List.nodup_append : ∀ {α : Type u_1} {l₁ l₂ : List α}, (l₁ ++ l₂).Nodup ↔ l₁.Nodup ∧ l₂.Nodup ∧ ∀ a ∈ l₁, ∀ b ∈ l₂, a ≠ b
-- Init.Data.Ord.Basic
/-- Constructs an `LE` instance from an `Ord` instance that asserts that the result of `compare`
satisfies `Ordering.isLE`.
 -/
leOfOrd : {α : Type u_1} → [Ord α] → LE α
-- Lean.Expr
/-- A total order for expressions that takes the structure into account (e.g., variable names).  -/
Lean.Expr.lt : Lean.Expr → Lean.Expr → Bool
-- Mathlib.Algebra.Free
FreeAddMagmaAssocQuotientEquiv.eq_1 : ∀ (α : Type u),
  FreeAddMagmaAssocQuotientEquiv α =
    (AddMagma.FreeAddSemigroup.lift FreeAddMagma.toFreeAddSemigroup).toAddEquiv
      (FreeAddSemigroup.lift (⇑AddMagma.FreeAddSemigroup.of ∘ FreeAddMagma.of)) ⋯ ⋯
-- Lean.Elab.Command
Lean.Elab.Command.State.traceState : Lean.Elab.Command.State → Lean.TraceState
-- Std.Data.DTreeMap.Raw.Lemmas
Std.DTreeMap.Raw.contains_modify : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t : Std.DTreeMap.Raw α β cmp} [Std.TransCmp cmp]
  [inst : Std.LawfulEqCmp cmp], t.WF → ∀ {k k' : α} {f : β k → β k}, (t.modify k f).contains k' = t.contains k'
-- Mathlib.LinearAlgebra.DFinsupp
DFinsupp.sigmaCurryLEquiv_symm_apply : ∀ {ι : Type u_1} {R : Type u_3} [inst : Semiring R] [inst_1 : DecidableEq ι] {α : ι → Type u_7}
  {M : (i : ι) → α i → Type u_8} [inst_2 : (i : ι) → (j : α i) → AddCommMonoid (M i j)]
  [inst_3 : (i : ι) → (j : α i) → Module R (M i j)] (a : Π₀ (i : ι) (j : α i), M i j),
  DFinsupp.sigmaCurryLEquiv.symm a = DFinsupp.sigmaCurryEquiv.symm a
-- Init.Data.UInt.Lemmas
UInt8.toUInt32_toUInt16 : ∀ (n : UInt8), n.toUInt16.toUInt32 = n.toUInt32
-- Mathlib.AlgebraicGeometry.EllipticCurve.Weierstrass
WeierstrassCurve.b₂_of_char_two : ∀ {R : Type u} [inst : CommRing R] (W : WeierstrassCurve R) [CharP R 2], W.b₂ = W.a₁ ^ 2
-- Mathlib.LinearAlgebra.Matrix.Defs
Matrix.zero : {m : Type u_2} → {n : Type u_3} → {α : Type v} → [Zero α] → Zero (Matrix m n α)
-- Mathlib.MeasureTheory.MeasurableSpace.Embedding
/-- Products distribute over sums (on the left) as measurable spaces.  -/
MeasurableEquiv.prodSumDistrib : (α : Type u_6) →
  (β : Type u_7) →
    (γ : Type u_8) →
      [inst : MeasurableSpace α] →
        [inst_1 : MeasurableSpace β] → [inst_2 : MeasurableSpace γ] → α × (β ⊕ γ) ≃ᵐ α × β ⊕ α × γ
-- Mathlib.Data.FunLike.Equiv
EquivLike.surjective : ∀ {E : Sort u_1} {α : Sort u_3} {β : Sort u_4} [inst : EquivLike E α β] (e : E), Function.Surjective ⇑e
-- Mathlib.RingTheory.TwoSidedIdeal.Operations
TwoSidedIdeal.mem_span_iff_mem_addSubgroup_closure : ∀ {R : Type u_1} [inst : Ring R] {s : Set R} {z : R},
  z ∈ TwoSidedIdeal.span s ↔ z ∈ AddSubgroup.closure (Set.univ * s * Set.univ)
-- Mathlib.Analysis.Convex.Intrinsic
/-- **Alias** of the reverse direction of `intrinsicClosure_nonempty`. -/
Set.Nonempty.intrinsicClosure : ∀ {𝕜 : Type u_1} {V : Type u_2} {P : Type u_5} [inst : Ring 𝕜] [inst_1 : AddCommGroup V] [inst_2 : Module 𝕜 V]
  [inst_3 : TopologicalSpace P] [inst_4 : AddTorsor V P] {s : Set P}, s.Nonempty → (intrinsicClosure 𝕜 s).Nonempty
-- Mathlib.Geometry.Manifold.ContMDiff.Atlas
StructureGroupoid.maximalAtlas.eq_1 : ∀ {H : Type u} (M : Type u_2) [inst : TopologicalSpace H] [inst_1 : TopologicalSpace M] [inst_2 : ChartedSpace H M]
  (G : StructureGroupoid H),
  StructureGroupoid.maximalAtlas M G = {e | ∀ e' ∈ atlas H M, e.symm.trans e' ∈ G ∧ e'.symm.trans e ∈ G}
-- Init.Data.Range.Polymorphic.Lemmas
Std.Rii.toList_eq_nil_iff : ∀ {α : Type u} {r : Std.Rii α} [inst : LT α] [DecidableLT α] [inst_2 : Std.PRange.Least? α]
  [inst_3 : Std.PRange.UpwardEnumerable α] [inst_4 : Std.PRange.LawfulUpwardEnumerable α]
  [Std.PRange.LawfulUpwardEnumerableLT α] [Std.PRange.LawfulUpwardEnumerableLeast? α] [inst : Std.Rxi.IsAlwaysFinite α],
  r.toList = [] ↔ ¬Nonempty α
-- Init.GrindInstances.ToInt
Lean.Grind.instModUInt32UintOfNatNat : Lean.Grind.ToInt.Mod UInt32 (Lean.Grind.IntInterval.uint 32)
-- Mathlib.MeasureTheory.Covering.Differentiation
/-- If, for all `x` in a set `s`, one has frequently `ρ a / μ a < p`, then `ρ s ≤ p * μ s`, as
proved in `measure_le_of_frequently_le`. Since `ρ a / μ a` tends almost everywhere to
`v.limRatioMeas hρ x`, the same property holds for sets `s` on which `v.limRatioMeas hρ < p`.  -/
VitaliFamily.measure_le_mul_of_subset_limRatioMeas_lt : ∀ {α : Type u_1} [inst : PseudoMetricSpace α] {m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α}
  (v : VitaliFamily μ) [inst_1 : SecondCountableTopology α] [inst_2 : BorelSpace α]
  [inst_3 : MeasureTheory.IsLocallyFiniteMeasure μ] {ρ : MeasureTheory.Measure α}
  [inst_4 : MeasureTheory.IsLocallyFiniteMeasure ρ] (hρ : ρ.AbsolutelyContinuous μ) {p : NNReal} {s : Set α},
  s ⊆ {x | v.limRatioMeas hρ x < ↑p} → ρ s ≤ ↑p * μ s
-- Mathlib.GroupTheory.GroupAction.Defs
/-- Decomposition of a type `X` as a disjoint union of its orbits under an additive
group action.  -/
AddAction.selfEquivSigmaOrbits : (G : Type u_1) →
  (α : Type u_2) →
    [inst : AddGroup G] →
      [inst_1 : AddAction G α] → α ≃ (ω : AddAction.orbitRel.Quotient G α) × ↑(AddAction.orbit G (Quotient.out ω))
-- Mathlib.CategoryTheory.Bicategory.NaturalTransformation.Lax
CategoryTheory.Lax.StrongTrans.app : {B : Type u₁} →
  [inst : CategoryTheory.Bicategory B] →
    {C : Type u₂} →
      [inst_1 : CategoryTheory.Bicategory C] →
        {F G : CategoryTheory.LaxFunctor B C} → CategoryTheory.Lax.StrongTrans F G → (a : B) → F.obj a ⟶ G.obj a
-- Mathlib.Data.PNat.Prime
PNat.Coprime.gcd_mul_right_cancel_right : ∀ (m : ℕ+) {n k : ℕ+}, k.Coprime m → m.gcd (n * k) = m.gcd n
-- Mathlib.Data.ENNReal.Inv
ENNReal.eq_of_forall_le_nnreal_iff : ∀ {x y : ENNReal}, (∀ (r : NNReal), x ≤ ↑r ↔ y ≤ ↑r) → x = y
-- Mathlib.Algebra.Order.Group.Pointwise.Interval
Set.preimage_mul_const_Ici_of_neg : ∀ {α : Type u_1} [inst : Field α] [inst_1 : LinearOrder α] [IsStrictOrderedRing α] (a : α) {c : α},
  c < 0 → (fun x => x * c) ⁻¹' Set.Ici a = Set.Iic (a / c)
-- Mathlib.Order.Interval.Finset.Basic
Finset.left_mem_Icc : ∀ {α : Type u_2} {a b : α} [inst : Preorder α] [inst_1 : LocallyFiniteOrder α], a ∈ Finset.Icc a b ↔ a ≤ b
-- Mathlib.CategoryTheory.Monoidal.Action.Opposites
/-- Define a right action of `C` on `D` from a left action of `Cᴹᵒᵖ` on `D` via
the formula `d ⊙ᵣ c := (mop c) ⊙ₗ d`.  -/
CategoryTheory.MonoidalCategory.MonoidalRightAction.rightActionOfMonoidalOppositeLeftAction : (C : Type u_1) →
  (D : Type u_2) →
    [inst : CategoryTheory.Category.{v_1, u_1} C] →
      [inst_1 : CategoryTheory.MonoidalCategory C] →
        [inst_2 : CategoryTheory.Category.{v_2, u_2} D] →
          [CategoryTheory.MonoidalCategory.MonoidalLeftAction Cᴹᵒᵖ D] →
            CategoryTheory.MonoidalCategory.MonoidalRightAction C D
-- Mathlib.Tactic.Use
/-- Run the `useLoop` on the main goal then discharge remaining explicit `Prop` arguments.  -/
Mathlib.Tactic.runUse : Bool → Lean.Elab.Tactic.TacticM Unit → List Lean.Term → Lean.Elab.Tactic.TacticM Unit
-- Mathlib.MeasureTheory.Function.LpSpace.Basic
MeasureTheory.MemLp.enorm_rpow : ∀ {α : Type u_1} {m : MeasurableSpace α} {p : ENNReal} {μ : MeasureTheory.Measure α} {ε : Type u_6}
  [inst : TopologicalSpace ε] [inst_1 : ContinuousENorm ε] {f : α → ε},
  MeasureTheory.MemLp f p μ → p ≠ 0 → p ≠ ⊤ → MeasureTheory.MemLp (fun x => ‖f x‖ₑ ^ p.toReal) 1 μ
-- Mathlib.Tactic.CategoryTheory.Coherence.Datatypes
Mathlib.Tactic.BicategoryLike.MonadMor₂.mk : {m : Type → Type} →
  (Mathlib.Tactic.BicategoryLike.Mor₂Iso → m Mathlib.Tactic.BicategoryLike.Mor₂) →
    (Mathlib.Tactic.BicategoryLike.AtomIso → m Mathlib.Tactic.BicategoryLike.Atom) →
      (Mathlib.Tactic.BicategoryLike.Mor₂Iso → m Mathlib.Tactic.BicategoryLike.Mor₂) →
        (Mathlib.Tactic.BicategoryLike.AtomIso → m Mathlib.Tactic.BicategoryLike.Atom) →
          (Mathlib.Tactic.BicategoryLike.Mor₁ → m Mathlib.Tactic.BicategoryLike.Mor₂) →
            (Mathlib.Tactic.BicategoryLike.Mor₂ →
                Mathlib.Tactic.BicategoryLike.Mor₂ → m Mathlib.Tactic.BicategoryLike.Mor₂) →
              (Mathlib.Tactic.BicategoryLike.Mor₁ →
                  Mathlib.Tactic.BicategoryLike.Mor₂ → m Mathlib.Tactic.BicategoryLike.Mor₂) →
                (Mathlib.Tactic.BicategoryLike.Mor₂ →
                    Mathlib.Tactic.BicategoryLike.Mor₁ → m Mathlib.Tactic.BicategoryLike.Mor₂) →
                  (Mathlib.Tactic.BicategoryLike.Mor₂ →
                      Mathlib.Tactic.BicategoryLike.Mor₂ → m Mathlib.Tactic.BicategoryLike.Mor₂) →
                    (Mathlib.Tactic.BicategoryLike.CoherenceHom →
                        Mathlib.Tactic.BicategoryLike.Mor₂ →
                          Mathlib.Tactic.BicategoryLike.Mor₂ → m Mathlib.Tactic.BicategoryLike.Mor₂) →
                      Mathlib.Tactic.BicategoryLike.MonadMor₂ m
-- Mathlib.Logic.Equiv.Defs
Equiv.trans_refl : ∀ {α : Sort u} {β : Sort v} (e : α ≃ β), e.trans (Equiv.refl β) = e
-- Mathlib.CategoryTheory.Limits.Shapes.Multiequalizer
CategoryTheory.Limits.MultispanIndex.inj_sndSigmaMapOfIsColimit : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {J : CategoryTheory.Limits.MultispanShape}
  (I : CategoryTheory.Limits.MultispanIndex J C) {c : CategoryTheory.Limits.Cofan I.left}
  (d : CategoryTheory.Limits.Cofan I.right) (hc : CategoryTheory.Limits.IsColimit c) (i : J.L),
  CategoryTheory.CategoryStruct.comp (c.inj i) (I.sndSigmaMapOfIsColimit d hc) =
    CategoryTheory.CategoryStruct.comp (I.snd i) (d.inj (J.snd i))
-- Mathlib.Algebra.Quandle
Rack.PreEnvelGroupRel'.trans.injEq : ∀ {R : Type u} [inst : Rack R] {a b c : Rack.PreEnvelGroup R} (hab : Rack.PreEnvelGroupRel' R a b)
  (hbc : Rack.PreEnvelGroupRel' R b c) (b_1 : Rack.PreEnvelGroup R) (hab_1 : Rack.PreEnvelGroupRel' R a b_1)
  (hbc_1 : Rack.PreEnvelGroupRel' R b_1 c), (hab.trans hbc = hab_1.trans hbc_1) = (b = b_1 ∧ hab ≍ hab_1 ∧ hbc ≍ hbc_1)
-- Mathlib.CategoryTheory.Limits.IsLimit
CategoryTheory.Limits.IsLimit.mk : {J : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} J] →
    {C : Type u₃} →
      [inst_1 : CategoryTheory.Category.{v₃, u₃} C] →
        {F : CategoryTheory.Functor J C} →
          {t : CategoryTheory.Limits.Cone F} →
            (lift : (s : CategoryTheory.Limits.Cone F) → s.pt ⟶ t.pt) →
              autoParam
                  (∀ (s : CategoryTheory.Limits.Cone F) (j : J),
                    CategoryTheory.CategoryStruct.comp (lift s) (t.π.app j) = s.π.app j)
                  CategoryTheory.Limits.IsLimit.fac._autoParam →
                autoParam
                    (∀ (s : CategoryTheory.Limits.Cone F) (m : s.pt ⟶ t.pt),
                      (∀ (j : J), CategoryTheory.CategoryStruct.comp m (t.π.app j) = s.π.app j) → m = lift s)
                    CategoryTheory.Limits.IsLimit.uniq._autoParam →
                  CategoryTheory.Limits.IsLimit t
-- Mathlib.Order.Hom.Bounded
TopHom.mk.sizeOf_spec : ∀ {α : Type u_6} {β : Type u_7} [inst : Top α] [inst_1 : Top β] [inst_2 : SizeOf α] [inst_3 : SizeOf β] (toFun : α → β)
  (map_top' : toFun ⊤ = ⊤), sizeOf { toFun := toFun, map_top' := map_top' } = 1 + sizeOf map_top'
-- Mathlib.Algebra.Homology.HomotopyCategory.HomComplex
/-- The `1`-cocycle given by the differential on a cochain complex.  -/
CochainComplex.HomComplex.Cocycle.diff : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    [inst_1 : CategoryTheory.Preadditive C] → (K : CochainComplex C ℤ) → CochainComplex.HomComplex.Cocycle K K 1
-- Init.Control.Lawful.Instances
StateT.run_seqRight : ∀ {m : Type u_1 → Type u_2} {σ α β : Type u_1} [inst : Monad m] (x : StateT σ m α) (y : StateT σ m β) (s : σ),
  (x *> y).run s = do
    let p ← x.run s
    y.run p.2
-- Mathlib.RingTheory.Radical.Basic
/-- The radical of an element `a` in a unique factorization monoid is the product of
the prime factors of `a`.  -/
UniqueFactorizationMonoid.radical : {M : Type u_1} → [inst : CommMonoidWithZero M] → [NormalizationMonoid M] → [UniqueFactorizationMonoid M] → M → M
-- Mathlib.GroupTheory.Finiteness
/-- An equivalent expression of `AddSubgroup.fg` in terms of `Set.Finite` instead of
`Finset`.  -/
AddSubgroup.fg_iff : ∀ {G : Type u_3} [inst : AddGroup G] (P : AddSubgroup G), P.FG ↔ ∃ S, AddSubgroup.closure S = P ∧ S.Finite
-- Mathlib.Tactic.Order.CollectFacts
Mathlib.Tactic.Order.AtomicFact.ne.inj : ∀ {lhs rhs : ℕ} {proof : Lean.Expr} {lhs_1 rhs_1 : ℕ} {proof_1 : Lean.Expr},
  Mathlib.Tactic.Order.AtomicFact.ne lhs rhs proof = Mathlib.Tactic.Order.AtomicFact.ne lhs_1 rhs_1 proof_1 →
    lhs = lhs_1 ∧ rhs = rhs_1 ∧ proof = proof_1
-- Mathlib.Probability.Independence.CharacteristicFunction
ProbabilityTheory.charFunDual_map_add_prod_eq_mul : ∀ {E : Type u_2} {mE : MeasurableSpace E} [inst : NormedAddCommGroup E] [BorelSpace E] [SecondCountableTopology E]
  [inst_3 : NormedSpace ℝ E] {μ ν : MeasureTheory.Measure E} [MeasureTheory.IsProbabilityMeasure μ]
  [MeasureTheory.IsProbabilityMeasure ν],
  MeasureTheory.charFunDual (MeasureTheory.Measure.map (fun p => p.1 + p.2) (μ.prod ν)) =
    MeasureTheory.charFunDual μ * MeasureTheory.charFunDual ν
-- Mathlib.Order.Filter.NAry
/-- Symmetric statement to `Filter.map₂_map_left_anticomm`.  -/
Filter.map_map₂_antidistrib_left : ∀ {α : Type u_1} {β : Type u_3} {β' : Type u_4} {γ : Type u_5} {δ : Type u_7} {m : α → β → γ} {f : Filter α}
  {g : Filter β} {n : γ → δ} {m' : β' → α → δ} {n' : β → β'},
  (∀ (a : α) (b : β), n (m a b) = m' (n' b) a) → Filter.map n (Filter.map₂ m f g) = Filter.map₂ m' (Filter.map n' g) f
-- Mathlib.Order.Fin.InsertNth
Fin.insertNth_monotone : ∀ {n : ℕ} {α : Type u_1} [inst : Preorder α] {f : Fin (n + 1) → α},
  Monotone f → ∀ (i : Fin n) (x : α), f i.castSucc ≤ x → x ≤ f i.succ → Monotone (i.castSucc.succ.insertNth x f)
-- Mathlib.AlgebraicTopology.SimplicialSet.AnodyneExtensions.Basic
SSet.anodyneExtensions_eq_retracts_transfiniteCompositions : SSet.anodyneExtensions =
  (CategoryTheory.MorphismProperty.transfiniteCompositions.{u, u, u + 1}
      (CategoryTheory.MorphismProperty.coproducts.{u, u, u + 1} SSet.modelCategoryQuillen.J).pushouts).retracts
-- Lean.PrettyPrinter.Delaborator.SubExpr
Lean.PrettyPrinter.Delaborator.SubExpr.HoleIterator.mk : ℕ → ℕ → Lean.PrettyPrinter.Delaborator.SubExpr.HoleIterator
-- Mathlib.Order.Filter.Lift
Filter.lift'_neBot_iff : ∀ {α : Type u_1} {β : Type u_2} {f : Filter α} {h : Set α → Set β},
  Monotone h → ((f.lift' h).NeBot ↔ ∀ s ∈ f, (h s).Nonempty)
-- Mathlib.Topology.Order.ScottTopology
Topology.IsScott.isUpperSet_of_isOpen : ∀ {α : Type u_1} {D : Set (Set α)} [inst : Preorder α] [inst_1 : TopologicalSpace α] {s : Set α} [Topology.IsScott α D],
  IsOpen s → IsUpperSet s
-- Mathlib.Algebra.Notation.Pi.Defs
Pi.instMul : {ι : Type u_1} → {M : ι → Type u_5} → [(i : ι) → Mul (M i)] → Mul ((i : ι) → M i)
-- Init.Data.List.Sublist
List.prefix_rfl : ∀ {α : Type u_1} {l : List α}, l <+: l
-- Mathlib.Algebra.Polynomial.CoeffMem
/-- For polynomials `p q : R[X]`, the coefficients of `p %ₘ q` can be written as sums of products of
coefficients of `p` and `q`.

Precisely, each summand needs at most one coefficient of `p` and `deg p` coefficients of `q`.  -/
Polynomial.coeff_modByMonic_mem_pow_natDegree_mul : ∀ {R : Type u_2} {S : Type u_3} [inst : CommRing R] [inst_1 : Ring S] [inst_2 : Algebra R S] (p q : Polynomial S)
  (Mp : Submodule R S),
  (∀ (i : ℕ), p.coeff i ∈ Mp) →
    1 ∈ Mp →
      ∀ (Mq : Submodule R S), (∀ (i : ℕ), q.coeff i ∈ Mq) → 1 ∈ Mq → ∀ (i : ℕ), (p %ₘ q).coeff i ∈ Mq ^ p.natDegree * Mp
-- Mathlib.Geometry.Manifold.MFDeriv.SpecificFunctions
MDifferentiableWithinAt.sum : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {H : Type u_3} [inst_3 : TopologicalSpace H] {I : ModelWithCorners 𝕜 E H} {M : Type u_4}
  [inst_4 : TopologicalSpace M] [inst_5 : ChartedSpace H M] {E' : Type u_5} [inst_6 : NormedAddCommGroup E']
  [inst_7 : NormedSpace 𝕜 E'] {s : Set M} {z : M} {ι : Type} {t : Finset ι} {f : ι → M → E'},
  (∀ i ∈ t, MDiffAt[s] (f i) z) → MDiffAt[s] (∑ i ∈ t, f i) z
-- Mathlib.RingTheory.IdealFilter.Topology
/-- A set `s` is a neighbourhood of `a` iff it contains a left-additive coset of some ideal
`I ∈ F`.  -/
WithIdealFilter.mem_nhds_iff : ∀ {A : Type u_1} [inst : Ring A] {F : IdealFilter A} {a : WithIdealFilter F} {s : Set (WithIdealFilter F)},
  s ∈ nhds a ↔ ∃ I ∈ F, a +ᵥ WithIdealFilter.idealSet I ⊆ s
-- Mathlib.Analysis.Normed.Operator.BoundedLinearMaps
/-- Scalar multiplication (for a normed `𝕜`-algebra acting on a normed `𝕜`-module) as a bounded
bilinear map.  -/
isBoundedBilinearMap_smul : ∀ {𝕜 : Type u_1} {A : Type u_2} [inst : CommSemiring 𝕜] [inst_1 : SeminormedRing A] [inst_2 : Algebra 𝕜 A]
  {E : Type u_3} [inst_3 : SeminormedAddCommGroup E] [inst_4 : Module 𝕜 E] [inst_5 : Module A E] [IsBoundedSMul A E]
  [IsScalarTower 𝕜 A E], IsBoundedBilinearMap 𝕜 fun p => p.1 • p.2
-- Mathlib.CategoryTheory.Limits.Shapes.FiniteLimits
CategoryTheory.Limits.HasFiniteColimits.mk : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C],
  (∀ (J : Type) [𝒥 : CategoryTheory.SmallCategory J] [CategoryTheory.FinCategory J],
      CategoryTheory.Limits.HasColimitsOfShape J C) →
    CategoryTheory.Limits.HasFiniteColimits C
-- Mathlib.Dynamics.TopologicalEntropy.Subset
Dynamics.IsDynNetIn.monotone_subset : ∀ {X : Type u_1} {T : X → X} {F G s : Set X} {U : SetRel X X} {n : ℕ},
  F ⊆ G → Dynamics.IsDynNetIn T F U n s → Dynamics.IsDynNetIn T G U n s
-- Mathlib.Algebra.Group.Subgroup.Even
AddSubgroup.mem_even : ∀ {G : Type u_1} [inst : AddCommGroup G] {a : G}, a ∈ AddSubgroup.even G ↔ Even a
-- Batteries.Data.BinomialHeap.Basic
/-- `O(n)`. Fold a monadic function over the tree structure to accumulate a value.  -/
Batteries.BinomialHeap.Imp.HeapNode.foldTreeM : {m : Type u_1 → Type u_2} →
  {β : Type u_1} → {α : Type u_3} → [Monad m] → β → (α → β → β → m β) → Batteries.BinomialHeap.Imp.HeapNode α → m β
-- Mathlib.Order.PrimeIdeal
Order.Ideal.PrimePair.disjoint : ∀ {P : Type u_1} [inst : Preorder P] (IF : Order.Ideal.PrimePair P), Disjoint ↑IF.I ↑IF.F
-- Std.Http.Data.Headers.Basic
Std.Http.Header.Host.mk.inj : ∀ {host : Std.Http.URI.Host} {port : Std.Http.URI.Port} {host_1 : Std.Http.URI.Host} {port_1 : Std.Http.URI.Port},
  { host := host, port := port } = { host := host_1, port := port_1 } → host = host_1 ∧ port = port_1
-- Init.Data.String.Iterator
/-- The size of a string iterator is the number of bytes remaining.

Recursive functions that iterate towards the end of a string will typically decrease this measure.
 -/
String.Legacy.instSizeOfIterator : SizeOf String.Legacy.Iterator
-- Mathlib.Topology.Irreducible
instPreirreducibleSpaceOfSubsingleton : ∀ {X : Type u_1} [inst : TopologicalSpace X] [Subsingleton X], PreirreducibleSpace X
-- Mathlib.Order.Hom.BoundedLattice
InfTopHom.dual.eq_1 : ∀ {α : Type u_2} {β : Type u_3} [inst : Min α] [inst_1 : Top α] [inst_2 : Min β] [inst_3 : Top β],
  InfTopHom.dual =
    { toFun := fun f => { toSupHom := InfHom.dual f.toInfHom, map_bot' := ⋯ },
      invFun := fun f => { toInfHom := InfHom.dual.symm f.toSupHom, map_top' := ⋯ }, left_inv := ⋯, right_inv := ⋯ }
-- Mathlib.GroupTheory.MonoidLocalization.Basic
/-- Copy of `Quotient.recOnSubsingleton₂` for `Localization`  -/
Localization.recOnSubsingleton₂ : {M : Type u_1} →
  [inst : CommMonoid M] →
    {S : Submonoid M} →
      {r : Localization S → Localization S → Sort u} →
        [h : ∀ (a c : M) (b d : ↥S), Subsingleton (r (Localization.mk a b) (Localization.mk c d))] →
          (x y : Localization S) → ((a c : M) → (b d : ↥S) → r (Localization.mk a b) (Localization.mk c d)) → r x y
-- Mathlib.Algebra.MonoidAlgebra.Module
/-- The trivial monoid algebra is the base ring.  -/
MonoidAlgebra.uniqueLinearEquiv : (R : Type u_1) →
  {S : Type u_2} →
    (M : Type u_3) →
      [inst : Semiring R] →
        [inst_1 : Semiring S] → [inst_2 : Module R S] → [One M] → [Subsingleton M] → MonoidAlgebra S M ≃ₗ[R] S
-- Mathlib.Geometry.Manifold.MFDeriv.Basic
mdifferentiableWithinAt_of_isInvertible_mfderivWithin : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {H : Type u_3} [inst_3 : TopologicalSpace H] {I : ModelWithCorners 𝕜 E H} {M : Type u_4}
  [inst_4 : TopologicalSpace M] [inst_5 : ChartedSpace H M] {E' : Type u_5} [inst_6 : NormedAddCommGroup E']
  [inst_7 : NormedSpace 𝕜 E'] {H' : Type u_6} [inst_8 : TopologicalSpace H'] {I' : ModelWithCorners 𝕜 E' H'}
  {M' : Type u_7} [inst_9 : TopologicalSpace M'] [inst_10 : ChartedSpace H' M'] {f : M → M'} {x : M} {s : Set M},
  (mfderiv[s] f x).IsInvertible → MDiffAt[s] f x
-- Mathlib.Data.List.FinRange
List.nodup_ofFn_ofInjective : ∀ {α : Type u} {n : ℕ} {f : Fin n → α}, Function.Injective f → (List.ofFn f).Nodup