mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Analysis.LocallyConvex.WithSeminorms
/-- In a semi-`NormedSpace`, a continuous seminorm is zero on elements of norm `0`.  -/
Seminorm.map_eq_zero_of_norm_eq_zero : ∀ {𝕜 : Type u_2} {F : Type u_7} [inst : NontriviallyNormedField 𝕜] [inst_1 : SeminormedAddCommGroup F]
  [inst_2 : NormedSpace 𝕜 F] (q : Seminorm 𝕜 F), Continuous ⇑q → ∀ {x : F}, ‖x‖ = 0 → q x = 0
-- Mathlib.LinearAlgebra.Matrix.Block
Matrix.BlockTriangular.sub : ∀ {α : Type u_1} {m : Type u_3} {R : Type v} {M N : Matrix m m R} {b : m → α} [inst : LT α]
  [inst_1 : SubNegZeroMonoid R], M.BlockTriangular b → N.BlockTriangular b → (M - N).BlockTriangular b
-- Mathlib.Order.Fin.Tuple
Antitone.vecCons : ∀ {α : Type u_1} [inst : Preorder α] {n : ℕ} {f : Fin (n + 1) → α} {a : α},
  Antitone f → f 0 ≤ a → Antitone (Matrix.vecCons a f)
-- Mathlib.Topology.Bornology.Hom
LocallyBoundedMap.comp_id : ∀ {α : Type u_2} {β : Type u_3} [inst : Bornology α] [inst_1 : Bornology β] (f : LocallyBoundedMap α β),
  f.comp (LocallyBoundedMap.id α) = f
-- Mathlib.Data.Option.Basic
Option.bind_eq_bind' : ∀ {α β : Type u} {f : α → Option β} {x : Option α}, x >>= f = x.bind f
-- Mathlib.Algebra.Lie.Subalgebra
LieSubalgebra.instPartialOrder : (R : Type u) →
  (L : Type v) →
    [inst : CommRing R] → [inst_1 : LieRing L] → [inst_2 : LieAlgebra R L] → PartialOrder (LieSubalgebra R L)
-- Mathlib.CategoryTheory.Limits.Shapes.Pullback.Assoc
/-- `(X₁ ×[Y₁] X₂) ×[Y₂] X₃` is the pullback `X₁ ×[Y₁] (X₂ ×[Y₂] X₃)`.  -/
CategoryTheory.Limits.pullbackAssocIsPullback : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    {X₁ X₂ X₃ Y₁ Y₂ : C} →
      (f₁ : X₁ ⟶ Y₁) →
        (f₂ : X₂ ⟶ Y₁) →
          (f₃ : X₂ ⟶ Y₂) →
            (f₄ : X₃ ⟶ Y₂) →
              [inst_1 : CategoryTheory.Limits.HasPullback f₁ f₂] →
                [inst_2 : CategoryTheory.Limits.HasPullback f₃ f₄] →
                  [inst_3 :
                      CategoryTheory.Limits.HasPullback
                        (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pullback.snd f₁ f₂) f₃) f₄] →
                    CategoryTheory.Limits.IsLimit
                      (CategoryTheory.Limits.PullbackCone.mk
                        (CategoryTheory.CategoryStruct.comp
                          (CategoryTheory.Limits.pullback.fst
                            (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pullback.snd f₁ f₂) f₃) f₄)
                          (CategoryTheory.Limits.pullback.fst f₁ f₂))
                        (CategoryTheory.Limits.pullback.lift
                          (CategoryTheory.CategoryStruct.comp
                            (CategoryTheory.Limits.pullback.fst
                              (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pullback.snd f₁ f₂) f₃) f₄)
                            (CategoryTheory.Limits.pullback.snd f₁ f₂))
                          (CategoryTheory.Limits.pullback.snd
                            (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pullback.snd f₁ f₂) f₃) f₄)
                          ⋯)
                        ⋯)
-- Mathlib.Order.Filter.Ultrafilter.Defs
Ultrafilter.map_id' : ∀ {α : Type u} (f : Ultrafilter α), Ultrafilter.map (fun x => x) f = f
-- Mathlib.RingTheory.TwoSidedIdeal.Operations
TwoSidedIdeal.comap.congr_simp : ∀ {R : Type u_1} {S : Type u_2} [inst : NonUnitalNonAssocRing R] [inst_1 : NonUnitalNonAssocRing S] {F : Type u_3}
  [inst_2 : FunLike F R S] (f f_1 : F),
  f = f_1 → ∀ [inst_3 : NonUnitalRingHomClass F R S], TwoSidedIdeal.comap f = TwoSidedIdeal.comap f_1
-- Mathlib.Data.List.Intervals
List.Ico.self_empty : ∀ {n : ℕ}, List.Ico n n = []
-- Mathlib.MeasureTheory.MeasurableSpace.Constructions
MeasurableSet.image_inclusion' : ∀ {α : Type u_1} {m : MeasurableSpace α} {s t : Set α} (h : s ⊆ t) {u : Set ↑s},
  MeasurableSet (Subtype.val ⁻¹' s) → MeasurableSet u → MeasurableSet (Set.inclusion h '' u)
-- Mathlib.GroupTheory.SpecificGroups.Quaternion
/-- The (generalised) quaternion group `QuaternionGroup n` of order `4n`. It can be defined by the
presentation $\langle a, x | a^{2n} = 1, x^2 = a^n, x^{-1}ax=a^{-1}\rangle$. We write `a i` for
$a^i$ and `xa i` for $x * a^i$.
 -/
QuaternionGroup : ℕ → Type
-- Mathlib.Algebra.Order.Ring.Unbundled.Basic
/-- Variant of `mul_lt_of_lt_one_right` for `a` negative instead of positive.  -/
lt_mul_of_lt_one_right : ∀ {R : Type u} [inst : Semiring R] [inst_1 : PartialOrder R] {a b : R} [ExistsAddOfLE R] [PosMulStrictMono R]
  [AddRightStrictMono R] [AddRightReflectLT R], a < 0 → b < 1 → a < a * b
-- Mathlib.Data.Set.Insert
Set.pair_subset : ∀ {α : Type u_1} {s : Set α} {a b : α}, a ∈ s → b ∈ s → {a, b} ⊆ s
-- Mathlib.Tactic.ClickSuggestions.Util
Mathlib.Tactic.ClickSuggestions.Context.mk.injEq : ∀ («meta» : Lean.Server.DocumentMeta) (cursorPos : Lean.Lsp.Position) (onGoal : Option ℕ)
  (stx : Option (Lean.TSyntax `tactic)) (masterToken statusToken solvedToken : ProofWidgets.RefreshToken)
  (goal : Lean.MVarId) (hyp? : Option Lean.FVarId) (pos : Lean.SubExpr.Pos) (meta_1 : Lean.Server.DocumentMeta)
  (cursorPos_1 : Lean.Lsp.Position) (onGoal_1 : Option ℕ) (stx_1 : Option (Lean.TSyntax `tactic))
  (masterToken_1 statusToken_1 solvedToken_1 : ProofWidgets.RefreshToken) (goal_1 : Lean.MVarId)
  (hyp?_1 : Option Lean.FVarId) (pos_1 : Lean.SubExpr.Pos),
  ({ «meta» := «meta», cursorPos := cursorPos, onGoal := onGoal, stx := stx, masterToken := masterToken,
        statusToken := statusToken, solvedToken := solvedToken, goal := goal, hyp? := hyp?, pos := pos } =
      { «meta» := meta_1, cursorPos := cursorPos_1, onGoal := onGoal_1, stx := stx_1, masterToken := masterToken_1,
        statusToken := statusToken_1, solvedToken := solvedToken_1, goal := goal_1, hyp? := hyp?_1, pos := pos_1 }) =
    («meta» = meta_1 ∧
      cursorPos = cursorPos_1 ∧
        onGoal = onGoal_1 ∧
          stx = stx_1 ∧
            masterToken = masterToken_1 ∧
              statusToken = statusToken_1 ∧ solvedToken = solvedToken_1 ∧ goal = goal_1 ∧ hyp? = hyp?_1 ∧ pos = pos_1)
-- Mathlib.Analysis.Analytic.Composition
FormalMultilinearSeries.compPartialSumTarget.eq_1 : ∀ (m M N : ℕ), FormalMultilinearSeries.compPartialSumTarget m M N = ⋯.toFinset
-- Std.Data.Internal.List.Associative
Std.Internal.List.getEntry?_replaceEntry : ∀ {α : Type u} {β : α → Type v} [inst : BEq α] [PartialEquivBEq α] {l : List ((a : α) × β a)} {a k : α} {v : β k},
  Std.Internal.List.getEntry? a (Std.Internal.List.replaceEntry k v l) =
    if Std.Internal.List.containsKey k l = true ∧ (k == a) = true then some ⟨k, v⟩ else Std.Internal.List.getEntry? a l
-- Mathlib.Data.Set.Finite.Lattice
/-- **Alias** of `Set.finite_sdiff_iUnion_Ioo`. -/
Set.finite_diff_iUnion_Ioo : ∀ {α : Type u} [inst : LinearOrder α] (s : Set α), (s \ ⋃ x ∈ s, ⋃ y ∈ s, Set.Ioo x y).Finite
-- Mathlib.GroupTheory.Coprod.Basic
Monoid.Coprod.fst_swap : ∀ {M : Type u_1} {N : Type u_2} [inst : Monoid M] [inst_1 : Monoid N] (x : Monoid.Coprod M N),
  Monoid.Coprod.fst ((Monoid.Coprod.swap M N) x) = Monoid.Coprod.snd x
-- Mathlib.AlgebraicTopology.SimplicialSet.Monoidal
SSet.prod_δ_snd : ∀ (X Y : SSet) {n : ℕ} (i : Fin (n + 2))
  (z : (CategoryTheory.MonoidalCategoryStruct.tensorObj X Y).obj (Opposite.op { len := n + 1 })),
  ((CategoryTheory.ConcreteCategory.hom
          (CategoryTheory.SimplicialObject.δ (CategoryTheory.MonoidalCategoryStruct.tensorObj X Y) i))
        z).2 =
    (CategoryTheory.ConcreteCategory.hom (CategoryTheory.SimplicialObject.δ Y i)) z.2
-- Mathlib.CategoryTheory.Preadditive.Biproducts
CategoryTheory.Limits.BinaryBicone.ofLimitCone_inl : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Preadditive C] {X Y : C}
  {t : CategoryTheory.Limits.Cone (CategoryTheory.Limits.pair X Y)} (ht : CategoryTheory.Limits.IsLimit t),
  (CategoryTheory.Limits.BinaryBicone.ofLimitCone ht).inl =
    CategoryTheory.Limits.BinaryFan.IsLimit.lift ht (CategoryTheory.CategoryStruct.id X) 0
-- Mathlib.Algebra.Algebra.Basic
algebraMap.coe_inj : ∀ (R : Type u_1) (A : Type u_2) [inst : CommSemiring R] [inst_1 : Semiring A] [inst_2 : Algebra R A] [FaithfulSMul R A]
  {a b : R}, ↑a = ↑b ↔ a = b
-- Mathlib.SetTheory.Cardinal.ENat
Cardinal.toENat_lt_ofNat : ∀ {c : Cardinal.{u}} {n : ℕ} [inst : n.AtLeastTwo], Cardinal.toENat c < OfNat.ofNat n ↔ c < OfNat.ofNat n
-- Mathlib.Algebra.Homology.SpectralObject.SpectralSequence
CategoryTheory.Abelian.SpectralObject.SpectralSequence.HomologyData.kfSc_X₁ : ∀ {C : Type u_1} {ι : Type u_2} {κ : Type u_3} [inst : CategoryTheory.Category.{v_1, u_1} C]
  [inst_1 : CategoryTheory.Abelian C] [inst_2 : Preorder ι] (X : CategoryTheory.Abelian.SpectralObject C ι)
  {c : ℤ → ComplexShape κ} {r₀ : ℤ} (data : CategoryTheory.Abelian.SpectralObject.SpectralSequenceDataCore ι c r₀)
  (r r' : ℤ) (hrr' : r + 1 = r') (hr : r₀ ≤ r) (pq' pq'' : κ) (i₀' i₀ i₁ i₂ i₃ : ι) (hi₀' : i₀' = data.i₀ r' pq' ⋯)
  (hi₀ : i₀ = data.i₀ r pq' ⋯) (hi₁ : i₁ = data.i₁ pq') (hi₂ : i₂ = data.i₂ pq') (hi₃ : i₃ = data.i₃ r pq' ⋯)
  (n₀ n₁ n₂ : ℤ) (hn₁' : n₁ = data.deg pq')
  (hn₁ : autoParam (n₀ + 1 = n₁) CategoryTheory.Abelian.SpectralObject.SpectralSequence.HomologyData.kfSc._auto_1)
  (hn₂ : autoParam (n₁ + 1 = n₂) CategoryTheory.Abelian.SpectralObject.SpectralSequence.HomologyData.kfSc._auto_3),
  (CategoryTheory.Abelian.SpectralObject.SpectralSequence.HomologyData.kfSc X data r r' hrr' hr pq' pq'' i₀' i₀ i₁ i₂ i₃
        hi₀' hi₀ hi₁ hi₂ hi₃ n₀ n₁ n₂ hn₁' hn₁ hn₂).X₁ =
    X.E (CategoryTheory.homOfLE ⋯) (CategoryTheory.homOfLE ⋯) (CategoryTheory.homOfLE ⋯) n₀ n₁ n₂ hn₁ ⋯
-- Lean.Meta.Tactic.Grind.Arith.CommRing.Types
Lean.Meta.Grind.Arith.CommRing.ringExt : Lean.Meta.Grind.SolverExtension Lean.Meta.Grind.Arith.CommRing.State
-- Mathlib.Combinatorics.SetFamily.Intersecting
Set.Intersecting.compl_notMem : ∀ {α : Type u_1} [inst : BooleanAlgebra α] {s : Set α}, s.Intersecting → ∀ {a : α}, a ∈ s → aᶜ ∉ s
-- Mathlib.Data.List.MinMax
List.minimum.eq_1 : ∀ {α : Type u_1} [inst : Preorder α] [inst_1 : DecidableLT α] (l : List α), l.minimum = List.argmin id l
-- Mathlib.RingTheory.Polynomial.Content
Polynomial.primPart_mul : ∀ {R : Type u_2} [inst : CommRing R] [inst_1 : StrongNormalizedGCDMonoid R] {p q : Polynomial R},
  p * q ≠ 0 → (p * q).primPart = p.primPart * q.primPart
-- Mathlib.Algebra.TrivSqZeroExt.Basic
/-- A universal property of the trivial square-zero extension, providing a unique
`TrivSqZeroExt R M →ₐ[R] A` for every pair of maps `f : R →ₐ[S] A` and `g : M →ₗ[S] A`,
where the range of `g` has no non-zero products, and scaling the input to `g` on the left or right
amounts to a corresponding multiplication by `f` in the output.

This isomorphism is named to match the very similar `Complex.lift`.  -/
TrivSqZeroExt.liftEquiv : {S : Type u_1} →
  {R : Type u} →
    {M : Type v} →
      [inst : CommSemiring S] →
        [inst_1 : Semiring R] →
          [inst_2 : AddCommMonoid M] →
            [inst_3 : Algebra S R] →
              [inst_4 : Module S M] →
                [inst_5 : Module R M] →
                  [inst_6 : Module Rᵐᵒᵖ M] →
                    [inst_7 : SMulCommClass R Rᵐᵒᵖ M] →
                      [inst_8 : IsScalarTower S R M] →
                        [inst_9 : IsScalarTower S Rᵐᵒᵖ M] →
                          {A : Type u_2} →
                            [inst_10 : Semiring A] →
                              [inst_11 : Algebra S A] →
                                { fg //
                                    (∀ (x y : M), fg.2 x * fg.2 y = 0) ∧
                                      (∀ (r : R) (x : M), fg.2 (r • x) = fg.1 r * fg.2 x) ∧
                                        ∀ (r : R) (x : M), fg.2 (MulOpposite.op r • x) = fg.2 x * fg.1 r } ≃
                                  (TrivSqZeroExt R M →ₐ[S] A)
-- Mathlib.CategoryTheory.Bicategory.Basic
CategoryTheory.Bicategory.leftUnitorNatIso_hom_app : ∀ {B : Type u} [inst : CategoryTheory.Bicategory B] (a b : B) (X : a ⟶ b),
  (CategoryTheory.Bicategory.leftUnitorNatIso a b).hom.app X = (CategoryTheory.Bicategory.leftUnitor X).hom
-- Mathlib.Analysis.ODE.ExistUnique
/-- There exists only one solution of an ODE $\dot x=v(t, x)$ with
a given initial value provided that the RHS is Lipschitz continuous in `x`.  -/
ODE_solution_unique : ∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] {v : ℝ → E → E} {K : NNReal} {f g : ℝ → E}
  {a b : ℝ},
  (∀ (t : ℝ), LipschitzWith K (v t)) →
    ContinuousOn f (Set.Icc a b) →
      (∀ t ∈ Set.Ico a b, HasDerivWithinAt f (v t (f t)) (Set.Ici t) t) →
        ContinuousOn g (Set.Icc a b) →
          (∀ t ∈ Set.Ico a b, HasDerivWithinAt g (v t (g t)) (Set.Ici t) t) → f a = g a → Set.EqOn f g (Set.Icc a b)
-- Mathlib.AlgebraicTopology.DoldKan.Normalized
AlgebraicTopology.DoldKan.HigherFacesVanish.inclusionOfMooreComplexMap : ∀ {A : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} A] [inst_1 : CategoryTheory.Abelian A]
  {X : CategoryTheory.SimplicialObject A} (n : ℕ),
  AlgebraicTopology.DoldKan.HigherFacesVanish (n + 1) ((AlgebraicTopology.inclusionOfMooreComplexMap X).f (n + 1))
-- Mathlib.Combinatorics.Matroid.Basic
Matroid.IsBase.exchange_isBase_of_indep : ∀ {α : Type u_1} {M : Matroid α} {B : Set α} {e f : α},
  M.IsBase B → f ∉ B → M.Indep (insert f (B \ {e})) → M.IsBase (insert f (B \ {e}))
-- Init.Data.Hashable
instHashableUInt64 : Hashable UInt64
-- Mathlib.Combinatorics.Matroid.Rank.Cardinal
Matroid.cRk_insert_closure_eq : ∀ {α : Type u} (M : Matroid α) [M.InvariantCardinalRank] (e : α) (X : Set α),
  M.cRk (insert e (M.closure X)) = M.cRk (insert e X)
-- Init.Data.Vector.Attach
Vector.toArray_attachWith : ∀ {α : Type u_1} {n : ℕ} {xs : Vector α n} {P : α → Prop} {H : ∀ x ∈ xs, P x},
  (xs.attachWith P H).toArray = xs.toArray.attachWith P ⋯
-- Mathlib.LinearAlgebra.QuadraticForm.Basic
QuadraticMap.linMulLin_comp : ∀ {R : Type u_3} {M : Type u_4} {A : Type u_7} [inst : CommSemiring R] [inst_1 : NonUnitalNonAssocSemiring A]
  [inst_2 : AddCommMonoid M] [inst_3 : Module R M] [inst_4 : Module R A] [inst_5 : SMulCommClass R A A]
  [inst_6 : IsScalarTower R A A] {N' : Type u_8} [inst_7 : AddCommMonoid N'] [inst_8 : Module R N'] (f g : M →ₗ[R] A)
  (h : N' →ₗ[R] M), (QuadraticMap.linMulLin f g).comp h = QuadraticMap.linMulLin (f ∘ₗ h) (g ∘ₗ h)
-- Mathlib.Algebra.Module.SpanRank
Submodule.spanFinrank_bot : ∀ {R : Type u_1} {M : Type u} [inst : Semiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M], ⊥.spanFinrank = 0
-- Mathlib.CategoryTheory.Galois.IsFundamentalgroup
_private.Mathlib.CategoryTheory.Galois.IsFundamentalgroup.0.CategoryTheory.PreGaloisCategory.isoOnObj_inv_hom_hom_apply : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{u₂, u₁} C] (F : CategoryTheory.Functor C FintypeCat) {G : Type u_1}
  [inst_1 : Group G] [inst_2 : (X : C) → MulAction G (F.obj X).obj] (g : G) (X : C) (a : (F.obj X).obj),
  (CategoryTheory.ConcreteCategory.hom (CategoryTheory.PreGaloisCategory.isoOnObj✝ F g X).inv.hom) a = g⁻¹ • a
-- Mathlib.Logic.Function.Basic
Function.not_surjective : Function.Surjective Not
-- Mathlib.CategoryTheory.Sites.Hypercover.One
CategoryTheory.PreOneHypercover.Hom.w₁₂_assoc : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {S : C} {E : CategoryTheory.PreOneHypercover S}
  {F : CategoryTheory.PreOneHypercover S} (self : E.Hom F) {i j : E.I₀} (k : E.I₁ i j) {Z : C}
  (h : F.X (self.s₀ j) ⟶ Z),
  CategoryTheory.CategoryStruct.comp (self.h₁ k) (CategoryTheory.CategoryStruct.comp (F.p₂ (self.s₁ k)) h) =
    CategoryTheory.CategoryStruct.comp (E.p₂ k) (CategoryTheory.CategoryStruct.comp (self.h₀ j) h)
-- Mathlib.Algebra.Ring.Int.Parity
Int.natAbs_even : ∀ {n : ℤ}, Even n.natAbs ↔ Even n
-- Mathlib.Topology.Compactness.Compact
/-- For every directed family of closed sets whose intersection avoids a compact set,
there exists a single element of the family which itself avoids this compact set.  -/
IsCompact.elim_directed_family_closed : ∀ {X : Type u} [inst : TopologicalSpace X] {s : Set X} {ι : Type v} [Nonempty ι],
  IsCompact s →
    ∀ (t : ι → Set X),
      (∀ (i : ι), IsClosed (t i)) → s ∩ ⋂ i, t i = ∅ → Directed (fun x1 x2 => x1 ⊇ x2) t → ∃ i, s ∩ t i = ∅
-- Mathlib.MeasureTheory.Measure.AEDisjoint
MeasureTheory.AEDisjoint.mono : ∀ {α : Type u_2} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} {s t u v : Set α},
  MeasureTheory.AEDisjoint μ s t → u ⊆ s → v ⊆ t → MeasureTheory.AEDisjoint μ u v
-- Init.Data.Nat.Internal.Linear
Nat.Internal.Linear.hugeFuel : ℕ
-- Mathlib.Analysis.Calculus.FDeriv.Pow
hasFDerivAt_pow : ∀ {𝕜 : Type u_1} {𝔸 : Type u_2} [inst : NontriviallyNormedField 𝕜] [inst_1 : NormedCommRing 𝔸]
  [inst_2 : NormedAlgebra 𝕜 𝔸] (n : ℕ) {x : 𝔸},
  HasFDerivAt (fun x => x ^ n) ((n • x ^ (n - 1)) • ContinuousLinearMap.id 𝕜 𝔸) x
-- Mathlib.RingTheory.Extension.Basic
Algebra.Extension.instIsScalarTowerRing : ∀ {R : Type u} {S : Type v} [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : Algebra R S] (P : Algebra.Extension R S)
  {R₀ : Type u_1} [inst_3 : CommRing R₀] [inst_4 : Algebra R₀ R] [inst_5 : Algebra R₀ S]
  [inst_6 : IsScalarTower R₀ R S], IsScalarTower R₀ R P.Ring
-- Mathlib.Control.Monad.Cont
WriterT.callCC : {m : Type u → Type v} →
  [Monad m] →
    [MonadCont m] →
      {α β ω : Type u} → [EmptyCollection ω] → (MonadCont.Label α (WriterT ω m) β → WriterT ω m α) → WriterT ω m α
-- Mathlib.Data.Multiset.Filter
Multiset.filter_filterMap : ∀ {α : Type u_1} {β : Type v} (f : α → Option β) (p : β → Prop) [inst : DecidablePred p] (s : Multiset α),
  Multiset.filter p (Multiset.filterMap f s) =
    Multiset.filterMap (fun x => Option.filter (fun b => decide (p b)) (f x)) s
-- Std.Data.Internal.List.Associative
_private.Std.Data.Internal.List.Associative.0.Std.Internal.List.alterKey_cons_perm.match_1.eq_2 : ∀ {α : Type u_3} {β : α → Type u_1} {k : α} (motive : Option (β k) → Sort u_2) (v : β k) (h_1 : Unit → motive none)
  (h_2 : (v : β k) → motive (some v)),
  (match some v with
    | none => h_1 ()
    | some v => h_2 v) =
    h_2 v
-- Mathlib.Data.Finmap
Finmap.lookup_singleton_eq : ∀ {α : Type u} {β : α → Type v} [inst : DecidableEq α] {a : α} {b : β a},
  Finmap.lookup a (Finmap.singleton a b) = some b
-- Mathlib.Analysis.Calculus.LHopital
/-- **L'Hôpital's rule** for approaching a real, `deriv` version. This
does not require anything about the situation at `a`  -/
deriv.lhopital_zero_nhdsNE : ∀ {a : ℝ} {l : Filter ℝ} {f g : ℝ → ℝ},
  (∀ᶠ (x : ℝ) in nhdsWithin a {a}ᶜ, DifferentiableAt ℝ f x) →
    (∀ᶠ (x : ℝ) in nhdsWithin a {a}ᶜ, deriv g x ≠ 0) →
      Filter.Tendsto f (nhdsWithin a {a}ᶜ) (nhds 0) →
        Filter.Tendsto g (nhdsWithin a {a}ᶜ) (nhds 0) →
          Filter.Tendsto (fun x => deriv f x / deriv g x) (nhdsWithin a {a}ᶜ) l →
            Filter.Tendsto (fun x => f x / g x) (nhdsWithin a {a}ᶜ) l
-- Mathlib.RepresentationTheory.Coinduced
/-- Given a monoid homomorphism `φ : G →* H`, this is the functor sending a `G`-representation `A`
to the coinduced `H`-representation `coind φ A`, with action on maps given by postcomposition.  -/
Rep.coindFunctor : (k : Type u) →
  {G : Type v} →
    {H : Type w} →
      [inst : CommRing k] →
        [inst_1 : Monoid G] →
          [inst_2 : Monoid H] → (G →* H) → CategoryTheory.Functor (Rep.{t, u, v} k G) (Rep.{max w t, u, w} k H)
-- Mathlib.NumberTheory.NumberField.CMField
NumberField.CMExtension.equivMaximalRealSubfield.congr_simp : ∀ (F : Type u_1) (K : Type u_2) [inst : Field F] [inst_1 : NumberField.IsTotallyReal F] [inst_2 : Field K]
  [inst_3 : CharZero K] [inst_4 : Algebra.IsIntegral ℚ K] [inst_5 : NumberField.IsTotallyComplex K]
  [inst_6 : Algebra F K] [inst_7 : Algebra.IsQuadraticExtension F K],
  NumberField.CMExtension.equivMaximalRealSubfield F K = NumberField.CMExtension.equivMaximalRealSubfield F K
-- Mathlib.CategoryTheory.Monoidal.Internal.Types.Basic
MonTypeEquivalenceMon.monMonoid : (A : Type u) → [CategoryTheory.MonObj A] → Monoid A
-- Mathlib.Algebra.Order.Hom.Monoid
OrderMonoidHom.instInhabited : (α : Type u_2) → [inst : Preorder α] → [inst_1 : MulOneClass α] → Inhabited (α →*o α)
-- Mathlib.Data.Set.Prod
Set.univ_pi_update : ∀ {ι : Type u_1} {α : ι → Type u_2} [inst : DecidableEq ι] {β : ι → Type u_4} (i : ι) (f : (j : ι) → α j) (a : α i)
  (t : (j : ι) → α j → Set (β j)),
  (Set.univ.pi fun j => t j (Function.update f i a j)) = {x | x i ∈ t i a} ∩ {i}ᶜ.pi fun j => t j (f j)
-- Mathlib.Topology.Algebra.Nonarchimedean.Bases
RingSubgroupsBasis.hasBasis_nhds : ∀ {A : Type u_1} {ι : Type u_2} [inst : Ring A] [inst_1 : Nonempty ι] {B : ι → AddSubgroup A}
  (hB : RingSubgroupsBasis B) (a : A), (nhds a).HasBasis (fun x => True) fun i => {b | b - a ∈ B i}
-- Mathlib.Algebra.Lie.Prod
LieHom.coe_inl : ∀ {R : Type u_1} {L₁ : Type u_2} {L₂ : Type u_3} [inst : CommRing R] [inst_1 : LieRing L₁] [inst_2 : LieAlgebra R L₁]
  [inst_3 : LieRing L₂] [inst_4 : LieAlgebra R L₂], ⇑(LieHom.inl R L₁ L₂) = fun x => (x, 0)
-- Mathlib.CategoryTheory.Limits.Types.ColimitType
CategoryTheory.Functor.CoconeTypes.IsColimit.of_equiv : ∀ {J : Type u} [inst : CategoryTheory.Category.{v, u} J] {F : CategoryTheory.Functor J (Type w₀)} {c : F.CoconeTypes},
  c.IsColimit →
    ∀ {c' : F.CoconeTypes} (e : c.pt ≃ c'.pt), (∀ (j : J) (x : F.obj j), c'.ι j x = e (c.ι j x)) → c'.IsColimit
-- Mathlib.CategoryTheory.Preadditive.Injective.Basic
CategoryTheory.Retract.injective : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {X Y : C} (h : CategoryTheory.Retract X Y)
  [i : CategoryTheory.Injective Y], CategoryTheory.Injective X
-- Lean.Widget.InteractiveCode
/-- Information about a subexpression within delaborated code.  -/
Lean.Widget.SubexprInfo : Type
-- Mathlib.Dynamics.Transitive
/-- An action of an additive monoid `M` on `α` that is continuous in the second
argument is topologically transitive if and only if any nonempty open subset `U` of `α` with
`(m +ᵥ ·) ⁻¹' U ⊆ U` for all `m : M` is dense in `α`.  -/
AddAction.isTopologicallyTransitive_iff_dense_of_preimage_invariant : ∀ (M : Type u_1) {α : Type u_2} [inst : TopologicalSpace α] [inst_1 : AddMonoid M] [inst_2 : AddAction M α]
  [h : ContinuousConstVAdd M α],
  AddAction.IsTopologicallyTransitive M α ↔
    ∀ {U : Set α}, IsOpen U → U.Nonempty → (∀ (m : M), (fun x => m +ᵥ x) ⁻¹' U ⊆ U) → Dense U
-- Mathlib.RingTheory.RingInvo
/-- Any type satisfying `RingInvoClass` can be cast into `RingInvo` via
`RingInvoClass.toRingInvo`.  -/
RingInvo.instCoeTCOfRingInvoClass : {F : Type u_1} →
  {R : Type u_2} → [inst : Semiring R] → [inst_1 : EquivLike F R Rᵐᵒᵖ] → [RingInvoClass F R] → CoeTC F (RingInvo R)
-- Mathlib.Data.Matrix.Mul
Matrix.sub_vecMul : ∀ {m : Type u_2} {n : Type u_3} {α : Type v} [inst : NonUnitalNonAssocRing α] [inst_1 : Fintype m] (A : Matrix m n α)
  (x y : m → α), Matrix.vecMul (x - y) A = Matrix.vecMul x A - Matrix.vecMul y A
-- Lean.Elab.PreDefinition.Basic
Lean.Elab.PreDefinition.filterAttrs : Lean.Elab.PreDefinition → (Lean.Elab.Attribute → Bool) → Lean.Elab.PreDefinition
-- Mathlib.Algebra.Homology.Embedding.AreComplementary
/-- If `ι₁` and `ι₂` are the index types of complementary embeddings into a
complex shape of index type `ι`, this is a constructor for (dependent) maps from `ι`,
which takes as inputs the "restrictions" to `ι₁` and `ι₂`.  -/
ComplexShape.Embedding.AreComplementary.desc : {ι : Type u_1} →
  {ι₁ : Type u_2} →
    {ι₂ : Type u_3} →
      {c : ComplexShape ι} →
        {c₁ : ComplexShape ι₁} →
          {c₂ : ComplexShape ι₂} →
            {e₁ : c₁.Embedding c} →
              {e₂ : c₂.Embedding c} →
                e₁.AreComplementary e₂ →
                  {X : ι → Type u_5} → ((i₁ : ι₁) → X (e₁.f i₁)) → ((i₂ : ι₂) → X (e₂.f i₂)) → (i : ι) → X i
-- Mathlib.Topology.Order.Lattice
ContinuousOn.inf' : ∀ {L : Type u_1} {X : Type u_2} [inst : TopologicalSpace L] [inst_1 : TopologicalSpace X] [inst_2 : Min L]
  [ContinuousInf L] {f g : X → L} {s : Set X}, ContinuousOn f s → ContinuousOn g s → ContinuousOn (f ⊓ g) s
-- Lean.Environment
_private.Lean.Environment.0.Lean.PersistentEnvExtension.getModuleEntries.unsafe_1 : {α β σ : Type} →
  [Inhabited σ] → Lean.PersistentEnvExtension α β σ → Lean.ModuleIdx → Array Lean.EnvExtensionState → Array α
-- Mathlib.Analysis.Normed.Group.Basic
/-- **Triangle inequality** for the norm.  -/
norm_add_le_of_le : ∀ {E : Type u_5} [inst : SeminormedAddGroup E] {a₁ a₂ : E} {r₁ r₂ : ℝ}, ‖a₁‖ ≤ r₁ → ‖a₂‖ ≤ r₂ → ‖a₁ + a₂‖ ≤ r₁ + r₂