mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.CategoryTheory.Preadditive.Biproducts
CategoryTheory.Limits.biprod.ext_to_iff : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Preadditive C] {X Y : C}
  [inst_2 : CategoryTheory.Limits.HasBinaryBiproduct X Y] {Z : C} {f g : Z ⟶ X ⊞ Y},
  f = g ↔
    CategoryTheory.CategoryStruct.comp f CategoryTheory.Limits.biprod.fst =
        CategoryTheory.CategoryStruct.comp g CategoryTheory.Limits.biprod.fst ∧
      CategoryTheory.CategoryStruct.comp f CategoryTheory.Limits.biprod.snd =
        CategoryTheory.CategoryStruct.comp g CategoryTheory.Limits.biprod.snd
-- Mathlib.Algebra.Lie.Derivation.Basic
LieDerivation.leibniz' : ∀ {R : Type u_1} {L : Type u_2} {M : Type u_3} [inst : CommRing R] [inst_1 : LieRing L] [inst_2 : LieAlgebra R L]
  [inst_3 : AddCommGroup M] [inst_4 : Module R M] [inst_5 : LieRingModule L M] [inst_6 : LieModule R L M]
  (self : LieDerivation R L M) (a b : L), ↑self ⁅a, b⁆ = ⁅a, ↑self b⁆ - ⁅b, ↑self a⁆
-- Mathlib.Algebra.GroupWithZero.Defs
mul_right_injective₀ : ∀ {M₀ : Type u_1} [inst : Mul M₀] [inst_1 : Zero M₀] [IsLeftCancelMulZero M₀] {a : M₀},
  a ≠ 0 → Function.Injective fun x => a * x
-- Init.Data.List.Scan.Basic
/-- Folds a monadic function over a list from the right, accumulating partial results starting with
`init`. The accumulated values are combined with the each element of the list in order, using `f`.
 -/
List.scanrM : {m : Type u_1 → Type u_2} → {α : Type u_3} → {β : Type u_1} → [Monad m] → (α → β → m β) → β → List α → m (List β)
-- Std.Data.ExtTreeMap.Lemmas
Std.ExtTreeMap.getElem?_insertMany_list_of_mem : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Std.ExtTreeMap α β cmp} [inst : Std.TransCmp cmp]
  [inst_1 : BEq α] [Std.LawfulBEqCmp cmp] {l : List (α × β)} {k k' : α},
  cmp k k' = Ordering.eq →
    ∀ {v : β}, List.Pairwise (fun a b => ¬cmp a.1 b.1 = Ordering.eq) l → (k, v) ∈ l → (t.insertMany l)[k']? = some v
-- Mathlib.CategoryTheory.Limits.Shapes.BinaryBiproducts
CategoryTheory.Limits.Bicone.toBinaryBiconeFunctor_obj_snd : ∀ {C : Type uC} [inst : CategoryTheory.Category.{uC', uC} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  {X Y : C} (b : CategoryTheory.Limits.Bicone (CategoryTheory.Limits.pairFunction X Y)),
  (CategoryTheory.Limits.Bicone.toBinaryBiconeFunctor.obj b).snd = b.π CategoryTheory.Limits.WalkingPair.right
-- Mathlib.GroupTheory.GroupAction.SubMulAction.OfFixingSubgroup
SubAddAction.ofFixingAddSubgroup_insert_map_bijective : ∀ {M : Type u_1} {α : Type u_2} [inst : AddGroup M] [inst_1 : AddAction M α] {a : α}
  {s : Set ↥(SubAddAction.ofStabilizer M a)}, Function.Bijective ⇑(SubAddAction.ofFixingAddSubgroup_insert_map a s)
-- Mathlib.Data.QPF.Multivariate.Basic
MvQPF.lawfulMvFunctor : ∀ {n : ℕ} {F : TypeVec.{u} n → Type u_1} [q : MvQPF F], LawfulMvFunctor F
-- Lean.Meta.Tactic.Contradiction
_private.Lean.Meta.Tactic.Contradiction.0.Lean.Meta.isElimEmptyInductiveCandidate : Lean.FVarId → Lean.MetaM Bool
-- Mathlib.SetTheory.Ordinal.Arithmetic
Ordinal.sub_le : ∀ {a b c : Ordinal.{u_4}}, a - b ≤ c ↔ a ≤ b + c
-- Lean.Meta.TryThis
/-- Style as a warning. By default, decorates the text with an undersquiggle; providing the
argument `decorated := false` turns this off.  -/
Lean.Meta.Tactic.TryThis.SuggestionStyle.warning : optParam Bool true → Lean.Meta.Tactic.TryThis.SuggestionStyle
-- Mathlib.Topology.Irreducible
/-- A space is preirreducible iff all nonempty open sets are dense.  -/
preirreducibleSpace_iff_open_dense : ∀ (X : Type u_3) [inst : TopologicalSpace X], PreirreducibleSpace X ↔ ∀ ⦃U : Set X⦄, IsOpen U → U.Nonempty → Dense U
-- Mathlib.CategoryTheory.Limits.HasLimits
CategoryTheory.Limits.limit.π.eq_1 : ∀ {J : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} J] {C : Type u} [inst_1 : CategoryTheory.Category.{v, u} C]
  (F : CategoryTheory.Functor J C) [inst_2 : CategoryTheory.Limits.HasLimit F] (j : J),
  CategoryTheory.Limits.limit.π F j = (CategoryTheory.Limits.limit.cone F).π.app j
-- Mathlib.AlgebraicGeometry.AffineScheme
AlgebraicGeometry.IsAffineOpen.app_basicOpen_eq_away_map : ∀ {X Y : AlgebraicGeometry.Scheme} (f : X ⟶ Y) {U : Y.Opens} (hU : AlgebraicGeometry.IsAffineOpen U)
  (h : AlgebraicGeometry.IsAffineOpen ((TopologicalSpace.Opens.map f.base).obj U))
  (r : ↑(Y.presheaf.obj (Opposite.op U))),
  AlgebraicGeometry.Scheme.Hom.app f (Y.basicOpen r) =
    CategoryTheory.CategoryStruct.comp
      (CommRingCat.ofHom
        (IsLocalization.Away.map (↑(Y.presheaf.obj (Opposite.op (Y.basicOpen r))))
          (↑(X.presheaf.obj
              (Opposite.op
                (X.basicOpen ((CategoryTheory.ConcreteCategory.hom (AlgebraicGeometry.Scheme.Hom.app f U)) r)))))
          (CommRingCat.Hom.hom (AlgebraicGeometry.Scheme.Hom.app f U)) r))
      (X.presheaf.map (CategoryTheory.eqToHom ⋯).op)
-- Mathlib.Algebra.Tropical.Basic
Tropical.instLinearOrderTropical : {R : Type u} → [LinearOrder R] → LinearOrder (Tropical R)
-- Lean.Elab.DocString
/-- Throws an appropriate error for an unknown doc element (role/directive/code block/command).
Distinguishes "name resolves but isn't registered" from "name doesn't resolve at all",
and includes shadowed-name suggestions when applicable.
 -/
_private.Lean.Elab.DocString.0.Lean.Doc.throwUnknownDocElem : {α β : Type} → Lean.NameMap (Array Lean.Name) → Lean.NameMap α → Lean.Ident → String → Lean.Doc.DocM β
-- Mathlib.Order.CompleteLattice.Basic
iInf_iInf_eq_left : ∀ {α : Type u_1} {β : Type u_2} [inst : CompleteLattice α] {b : β} {f : (x : β) → x = b → α},
  ⨅ x, ⨅ (h : x = b), f x h = f b ⋯
-- Mathlib.Algebra.Order.Archimedean.Class
/-- Lift a function `M → α` that's monotone along archimedean classes to a
monotone function `MulArchimedeanClass M →o α`.  -/
MulArchimedeanClass.liftOrderHom : {M : Type u_1} →
  [inst : CommGroup M] →
    [inst_1 : LinearOrder M] →
      [inst_2 : IsOrderedMonoid M] →
        {α : Type u_2} →
          [inst_3 : PartialOrder α] →
            (f : M → α) →
              (∀ (a b : M), MulArchimedeanClass.mk a ≤ MulArchimedeanClass.mk b → f a ≤ f b) →
                MulArchimedeanClass M →o α
-- Mathlib.CategoryTheory.ObjectProperty.ColimitsOfShape
CategoryTheory.ObjectProperty.strictColimitsOfShape.colimit : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] {P : CategoryTheory.ObjectProperty C} {J : Type u'}
  [inst_1 : CategoryTheory.Category.{v', u'} J] (F : CategoryTheory.Functor J C)
  [inst_2 : CategoryTheory.Limits.HasColimit F],
  (∀ (j : J), P (F.obj j)) → P.strictColimitsOfShape J (CategoryTheory.Limits.colimit F)
-- Mathlib.Analysis.BoxIntegral.Basic
BoxIntegral.Integrable.neg : ∀ {ι : Type u} {E : Type v} {F : Type w} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E]
  [inst_2 : NormedAddCommGroup F] [inst_3 : NormedSpace ℝ F] {I : BoxIntegral.Box ι} [inst_4 : Fintype ι]
  {l : BoxIntegral.IntegrationParams} {f : (ι → ℝ) → E} {vol : BoxIntegral.BoxAdditiveMap ι (E →L[ℝ] F) ⊤},
  BoxIntegral.Integrable I l f vol → BoxIntegral.Integrable I l (-f) vol
-- Mathlib.Probability.Process.Stopping
MeasureTheory.isStronglyProgressive_min_stopping_time : ∀ {Ω : Type u_1} {ι : Type u_3} {m : MeasurableSpace Ω} [inst : Nonempty ι] {τ : Ω → WithTop ι} [inst_1 : LinearOrder ι]
  [inst_2 : MeasurableSpace ι] [inst_3 : TopologicalSpace ι] [OrderTopology ι] [SecondCountableTopology ι]
  [BorelSpace ι] {f : MeasureTheory.Filtration ι m} [TopologicalSpace.PseudoMetrizableSpace ι],
  MeasureTheory.IsStoppingTime f τ → MeasureTheory.IsStronglyProgressive f fun i ω => (min (↑i) (τ ω)).untopA
-- Mathlib.Algebra.Algebra.Tower
Algebra.algebraMapSubmonoid_map_map : ∀ {R : Type u_1} {A : Type u_2} {B : Type u_3} [inst : CommSemiring R] [inst_1 : CommSemiring A] [inst_2 : Algebra R A]
  (M : Submonoid R) [inst_3 : Semiring B] [inst_4 : Algebra R B] [inst_5 : Algebra A B] [IsScalarTower R A B],
  Algebra.algebraMapSubmonoid B (Algebra.algebraMapSubmonoid A M) = Algebra.algebraMapSubmonoid B M
-- Mathlib.LinearAlgebra.CliffordAlgebra.Grading
CliffordAlgebra.iSup_ι_range_eq_top : ∀ {R : Type u_1} {M : Type u_2} [inst : CommRing R] [inst_1 : AddCommGroup M] [inst_2 : Module R M]
  (Q : QuadraticForm R M), ⨆ i, (CliffordAlgebra.ι Q).range ^ i = ⊤
-- Mathlib.Algebra.Polynomial.Monic
Polynomial.Monic.not_dvd_of_degree_lt : ∀ {R : Type u} [inst : Semiring R] {p q : Polynomial R}, p.Monic → q ≠ 0 → q.degree < p.degree → ¬p ∣ q
-- Mathlib.CategoryTheory.Core
CategoryTheory.Equivalence.core_unitIso_inv_app_iso_hom : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  (E : C ≌ D) (X : CategoryTheory.Core C), (E.core.unitIso.inv.app X).iso.hom = E.unitIso.inv.app X.of
-- Mathlib.AlgebraicTopology.SimplicialObject.Basic
/-- The point of the augmentation.  -/
CategoryTheory.SimplicialObject.Augmented.point : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] → CategoryTheory.Functor (CategoryTheory.SimplicialObject.Augmented C) C
-- Lean.Meta.Tactic.Simp.BuiltinSimprocs.Nat
_private.Lean.Meta.Tactic.Simp.BuiltinSimprocs.Nat.0.Nat.mkOfDecideEqTrue : Lean.Expr → Lean.MetaM Lean.Expr
-- Init.Data.UInt.Lemmas
UInt16.toUInt8_div : ∀ (a b : UInt16), a < 256 → b < 256 → (a / b).toUInt8 = a.toUInt8 / b.toUInt8
-- Mathlib.MeasureTheory.Group.Convolution
/-- Scoped notation for the multiplicative convolution of measures.  -/
MeasureTheory.«term_∗ₘ_» : Lean.TrailingParserDescr
-- Mathlib.Analysis.SpecialFunctions.Pow.Deriv
Real.hasStrictDerivAt_rpow_const_of_ne : ∀ {x : ℝ}, x ≠ 0 → ∀ (p : ℝ), HasStrictDerivAt (fun x => x ^ p) (p * x ^ (p - 1)) x
-- Mathlib.SetTheory.ZFC.Rank
PSet.rank_empty : ∅.rank = 0
-- Mathlib.AlgebraicTopology.SimplicialSet.StdSimplexOne
SSet.stdSimplex.objMk₁_apply_eq_zero_iff : ∀ {n : ℕ} (i : Fin (n + 2)) (j : Fin (n + 1)), (SSet.stdSimplex.objMk₁ i) j = 0 ↔ j.castSucc < i
-- Mathlib.Algebra.Ring.Subsemiring.Basic
/-- If all the elements of a set `s` commute, then `closure s` is a commutative semiring.  -/
Subsemiring.isMulCommutative_closure : ∀ {R' : Type u_1} [inst : Semiring R'] {s : Set R'},
  (∀ x ∈ s, ∀ y ∈ s, x * y = y * x) → IsMulCommutative ↥(Subsemiring.closure s)
-- Mathlib.CategoryTheory.Monoidal.Grp
CategoryTheory.Grp.mkIso.eq_1 : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.CartesianMonoidalCategory C]
  {G H : CategoryTheory.Grp C} (e : G.X ≅ H.X)
  (one_f : CategoryTheory.CategoryStruct.comp CategoryTheory.MonObj.one e.hom = CategoryTheory.MonObj.one)
  (mul_f :
    CategoryTheory.CategoryStruct.comp CategoryTheory.MonObj.mul e.hom =
      CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.tensorHom e.hom e.hom)
        CategoryTheory.MonObj.mul),
  CategoryTheory.Grp.mkIso e one_f mul_f = CategoryTheory.Grp.mkIso' e
-- Mathlib.Algebra.Homology.Embedding.Restriction
HomologicalComplex.restrictionXIso.eq_1 : ∀ {ι : Type u_1} {ι' : Type u_2} {c : ComplexShape ι} {c' : ComplexShape ι'} {C : Type u_3}
  [inst : CategoryTheory.Category.{v_1, u_3} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  (K : HomologicalComplex C c') (e : c.Embedding c') [inst_2 : e.IsRelIff] {i : ι} {i' : ι'} (h : e.f i = i'),
  K.restrictionXIso e h = CategoryTheory.eqToIso ⋯
-- Mathlib.Algebra.SkewMonoidAlgebra.Basic
SkewMonoidAlgebra.eta : ∀ {k : Type u_1} {G : Type u_2} [inst : AddMonoid k] (f : SkewMonoidAlgebra k G), { coeff := f.coeff } = f
-- Mathlib.Tactic.Linarith.Datatypes
/-- Replace the collection of all hypotheses with new hypotheses.
These expressions are proof terms.  -/
Mathlib.Tactic.Linarith.GlobalPreprocessor.transform : Mathlib.Tactic.Linarith.GlobalPreprocessor → List Lean.Expr → Lean.MetaM (List Lean.Expr)
-- Init.Data.Array.Zip
Array.zip_eq_empty_iff : ∀ {α : Type u_1} {β : Type u_2} {as : Array α} {bs : Array β}, as.zip bs = #[] ↔ as = #[] ∨ bs = #[]
-- Mathlib.CategoryTheory.Limits.Shapes.Pullback.Categorical.Basic
/-- The square `transformObjPrecomposeObjSquare` is itself natural.  -/
CategoryTheory.Limits.CategoricalPullback.CatCommSqOver.transformObjPrecomposeObjSquare_iso_hom_naturality₂ : ∀ {A : Type u₁} {B : Type u₂} {C : Type u₃} [inst : CategoryTheory.Category.{v₁, u₁} A]
  [inst_1 : CategoryTheory.Category.{v₂, u₂} B] [inst_2 : CategoryTheory.Category.{v₃, u₃} C]
  {F : CategoryTheory.Functor A B} {G : CategoryTheory.Functor C B} {A₁ : Type u₄} {B₁ : Type u₅} {C₁ : Type u₆}
  [inst_3 : CategoryTheory.Category.{v₄, u₄} A₁] [inst_4 : CategoryTheory.Category.{v₅, u₅} B₁]
  [inst_5 : CategoryTheory.Category.{v₆, u₆} C₁] {F₁ : CategoryTheory.Functor A₁ B₁} {G₁ : CategoryTheory.Functor C₁ B₁}
  {X : Type u₇} {Y : Type u₈} [inst_6 : CategoryTheory.Category.{v₇, u₇} X]
  [inst_7 : CategoryTheory.Category.{v₈, u₈} Y] (U : CategoryTheory.Functor X Y)
  {ψ ψ' : CategoryTheory.Limits.CatCospanTransform F G F₁ G₁} (η : ψ ⟶ ψ'),
  CategoryTheory.CategoryStruct.comp
      (CategoryTheory.Functor.whiskerRight ((CategoryTheory.Limits.CategoricalPullback.CatCommSqOver.transform Y).map η)
        ((CategoryTheory.Limits.CategoricalPullback.CatCommSqOver.precompose F₁ G₁).obj U))
      (CategoryTheory.CatCommSq.iso ((CategoryTheory.Limits.CategoricalPullback.CatCommSqOver.transform Y).obj ψ')
          ((CategoryTheory.Limits.CategoricalPullback.CatCommSqOver.precompose F G).obj U)
          ((CategoryTheory.Limits.CategoricalPullback.CatCommSqOver.precompose F₁ G₁).obj U)
          ((CategoryTheory.Limits.CategoricalPullback.CatCommSqOver.transform X).obj ψ')).hom =
    CategoryTheory.CategoryStruct.comp
      (CategoryTheory.CatCommSq.iso ((CategoryTheory.Limits.CategoricalPullback.CatCommSqOver.transform Y).obj ψ)
          ((CategoryTheory.Limits.CategoricalPullback.CatCommSqOver.precompose F G).obj U)
          ((CategoryTheory.Limits.CategoricalPullback.CatCommSqOver.precompose F₁ G₁).obj U)
          ((CategoryTheory.Limits.CategoricalPullback.CatCommSqOver.transform X).obj ψ)).hom
      (((CategoryTheory.Limits.CategoricalPullback.CatCommSqOver.precompose F G).obj U).whiskerLeft
        ((CategoryTheory.Limits.CategoricalPullback.CatCommSqOver.transform X).map η))
-- Mathlib.GroupTheory.Index
/-- Relative version of `Subgroup.index_eq_two_iff_exists_notMem_and'`.  -/
Subgroup.relIndex_eq_two_iff_exists_notMem_and' : ∀ {G : Type u_1} [inst : Group G] {H K : Subgroup G}, H.relIndex K = 2 ↔ ∃ a ∈ K, a ∉ H ∧ ∀ b ∈ K, a * b ∈ H ∨ b ∈ H
-- Mathlib.Algebra.Free
Magma.AssocQuotient.induction_on : ∀ {α : Type u} [inst : Mul α] {C : Magma.AssocQuotient α → Prop} (x : Magma.AssocQuotient α),
  (∀ (x : α), C (Magma.AssocQuotient.of x)) → C x
-- Mathlib.Data.List.Nodup
List.Nodup.get_inj_iff : ∀ {α : Type u} {l : List α}, l.Nodup → ∀ {i j : Fin l.length}, l.get i = l.get j ↔ i = j
-- Mathlib.MeasureTheory.Measure.MeasureSpace
MeasureTheory.Measure.add_top : ∀ {α : Type u_1} {m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α}, μ + ⊤ = ⊤
-- Mathlib.Algebra.Order.Field.Basic
IsGLB.mul_right : ∀ {α : Type u_2} [inst : Semifield α] [inst_1 : PartialOrder α] [PosMulReflectLT α] {a b : α} [IsStrictOrderedRing α]
  {s : Set α}, 0 ≤ a → IsGLB s b → IsGLB ((fun b => b * a) '' s) (b * a)
-- Mathlib.Analysis.Convex.Deriv
/-- If a function `f` is continuous and `f'` is strictly monotone on `ℝ` then `f` is strictly
convex. Note that we don't require differentiability, since it is guaranteed at all but at most
one point by the strict monotonicity of `f'`.  -/
StrictMono.strictConvexOn_univ_of_deriv : ∀ {f : ℝ → ℝ}, Continuous f → StrictMono (deriv f) → StrictConvexOn ℝ Set.univ f
-- Mathlib.Analysis.Calculus.MeanValue
/-- The mean value theorem on a convex set: if the derivative of a function is bounded by `C` on
`s`, then the function is `C`-Lipschitz on `s`. Version with `fderivWithin` and
`LipschitzOnWith`.  -/
Convex.lipschitzOnWith_of_nnnorm_fderivWithin_le : ∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] {𝕜 : Type u_3} {G : Type u_4}
  [inst_2 : NontriviallyNormedField 𝕜] [IsRCLikeNormedField 𝕜] [inst_4 : NormedSpace 𝕜 E]
  [inst_5 : NormedAddCommGroup G] [inst_6 : NormedSpace 𝕜 G] {f : E → G} {s : Set E} {C : NNReal},
  DifferentiableOn 𝕜 f s → (∀ x ∈ s, ‖fderivWithin 𝕜 f s x‖₊ ≤ C) → Convex ℝ s → LipschitzOnWith C f s
-- Mathlib.Topology.Category.LightProfinite.AsLimit
/-- A cone over `S.diagram` whose cone point is isomorphic to `S`.
(Auxiliary definition, use `S.asLimitCone` instead.)
 -/
LightProfinite.asLimitConeAux : (S : LightProfinite) → CategoryTheory.Limits.Cone S.diagram
-- Init.Data.Array.Find
Array.isSome_finIdxOf? : ∀ {α : Type u_1} [inst : BEq α] [PartialEquivBEq α] {xs : Array α} {a : α}, (xs.finIdxOf? a).isSome = xs.contains a
-- Lean.Setup
Lean.Idbg.idbgClientLoop : {α : Type} → [Nonempty α] → String → Array Lean.Import → (α → String) → IO Unit
-- Mathlib.Algebra.GCDMonoid.Basic
gcd_eq_normalize : ∀ {α : Type u_1} [inst : CommMonoidWithZero α] [inst_1 : NormalizedGCDMonoid α] {a b c : α},
  gcd a b ∣ c → c ∣ gcd a b → gcd a b = normalize c
-- Mathlib.RingTheory.Ideal.Quotient.PowTransition
Ideal.map_mk_comap_factorPow : ∀ {R : Type u_3} [inst : CommRing R] (I : Ideal R) {a b : ℕ},
  0 < a →
    ∀ (le : a ≤ b),
      Ideal.comap (Ideal.Quotient.factorPow I le) (Ideal.map (Ideal.Quotient.mk (I ^ a)) I) =
        Ideal.map (Ideal.Quotient.mk (I ^ b)) I
-- Std.Data.HashMap.RawLemmas
Std.HashMap.Raw.mem_insertMany_list : ∀ {α : Type u} {β : Type v} {m : Std.HashMap.Raw α β} [inst : BEq α] [inst_1 : Hashable α] [EquivBEq α]
  [LawfulHashable α],
  m.WF → ∀ {l : List (α × β)} {k : α}, k ∈ m.insertMany l ↔ k ∈ m ∨ (List.map Prod.fst l).contains k = true
-- Mathlib.Order.Types.Defs
OrderType.type_congr : ∀ {α β : Type u} [inst : LinearOrder α] [inst_1 : LinearOrder β] (h : α ≃o β), OrderType.type α = OrderType.type β
-- Mathlib.Analysis.SpecialFunctions.Exp
Real.image_exp_Icc : ∀ (a b : ℝ), Real.exp '' Set.Icc a b = Set.Icc (Real.exp a) (Real.exp b)
-- Mathlib.Combinatorics.Matroid.Loop
Matroid.isNonloop_of_loopless : ∀ {α : Type u_1} {M : Matroid α} {e : α} [M.Loopless],
  autoParam (e ∈ M.E) Matroid.isNonloop_of_loopless._auto_1 → M.IsNonloop e
-- Mathlib.NumberTheory.Divisors
Int.swap_mem_divisorsAntidiag : ∀ {xy : ℤ × ℤ} {z : ℤ}, xy.swap ∈ z.divisorsAntidiag ↔ xy ∈ z.divisorsAntidiag
-- Lean.Elab.Tactic.Omega.MinNatAbs
/-- The minimum non-zero entry in a list of natural numbers, or zero if all entries are zero.

We completely characterize the function via
`nonzeroMinimum_eq_zero_iff` and `nonzeroMinimum_eq_nonzero_iff` below.
 -/
Lean.Elab.Tactic.Omega.List.nonzeroMinimum : List ℕ → ℕ
-- Mathlib.Analysis.Distribution.TestFunction
TestFunction.mk.injEq : ∀ {E : Type u_3} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] {Ω : TopologicalSpace.Opens E} {F : Type u_4}
  [inst_2 : NormedAddCommGroup F] [inst_3 : NormedSpace ℝ F] {n : ℕ∞} (toFun : E → F)
  (contDiff' : ContDiff ℝ (↑n) toFun) (hasCompactSupport' : HasCompactSupport toFun)
  (tsupport_subset' : tsupport toFun ⊆ ↑Ω) (toFun_1 : E → F) (contDiff'_1 : ContDiff ℝ (↑n) toFun_1)
  (hasCompactSupport'_1 : HasCompactSupport toFun_1) (tsupport_subset'_1 : tsupport toFun_1 ⊆ ↑Ω),
  ({ toFun := toFun, contDiff' := contDiff', hasCompactSupport' := hasCompactSupport',
        tsupport_subset' := tsupport_subset' } =
      { toFun := toFun_1, contDiff' := contDiff'_1, hasCompactSupport' := hasCompactSupport'_1,
        tsupport_subset' := tsupport_subset'_1 }) =
    (toFun = toFun_1)
-- Aesop.Rule
Aesop.LocalNormSimpRule.mk.sizeOf_spec : ∀ (id : Lean.Name) (simpTheorem : Lean.Term),
  sizeOf { id := id, simpTheorem := simpTheorem } = 1 + sizeOf id + sizeOf simpTheorem
-- Mathlib.RingTheory.PowerSeries.Ideal
PowerSeries.map_constantCoeff_le_self_of_X_mem : ∀ {R : Type u_1} [inst : CommRing R] {I : Ideal (PowerSeries R)},
  PowerSeries.X ∈ I → Ideal.map (PowerSeries.C.comp PowerSeries.constantCoeff) I ≤ I
-- Mathlib.Combinatorics.SimpleGraph.Clique
SimpleGraph.cliqueFree_bot : ∀ {α : Type u_1} {n : ℕ}, 2 ≤ n → ⊥.CliqueFree n
-- Mathlib.Algebra.Group.Basic
eq_sub_iff_add_eq' : ∀ {G : Type u_3} [inst : AddCommGroup G] {a b c : G}, a = b - c ↔ c + a = b
-- Mathlib.Analysis.InnerProductSpace.TwoDim
Orientation.kahler.congr_simp : ∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : InnerProductSpace ℝ E] [inst_2 : Fact (Module.finrank ℝ E = 2)]
  (o o_1 : Orientation ℝ E (Fin 2)), o = o_1 → o.kahler = o_1.kahler
-- Init.Data.Int.Gcd
Int.gcd_right_eq_iff : ∀ {a b b' : ℤ}, a.gcd b = a.gcd b' ↔ ∀ (c : ℤ), c ∣ a → (c ∣ b ↔ c ∣ b')
-- Mathlib.Topology.Algebra.Module.ContinuousLinearMap.Basic
/-- Coerce continuous linear maps to linear maps.  -/
ContinuousLinearMap.LinearMap.coe : {R₁ : Type u_1} →
  {R₂ : Type u_2} →
    [inst : Semiring R₁] →
      [inst_1 : Semiring R₂] →
        {σ₁₂ : R₁ →+* R₂} →
          {M₁ : Type u_4} →
            [inst_2 : TopologicalSpace M₁] →
              [inst_3 : AddCommMonoid M₁] →
                {M₂ : Type u_6} →
                  [inst_4 : TopologicalSpace M₂] →
                    [inst_5 : AddCommMonoid M₂] →
                      [inst_6 : Module R₁ M₁] → [inst_7 : Module R₂ M₂] → Coe (M₁ →SL[σ₁₂] M₂) (M₁ →ₛₗ[σ₁₂] M₂)
-- Mathlib.LinearAlgebra.QuadraticForm.QuadraticModuleCat
QuadraticModuleCat.mk.inj : ∀ {R : Type u} {inst : CommRing R} {toModuleCat : ModuleCat R} {form : QuadraticForm R ↑toModuleCat}
  {toModuleCat_1 : ModuleCat R} {form_1 : QuadraticForm R ↑toModuleCat_1},
  { toModuleCat := toModuleCat, form := form } = { toModuleCat := toModuleCat_1, form := form_1 } →
    toModuleCat = toModuleCat_1 ∧ form ≍ form_1
-- Mathlib.CategoryTheory.Monoidal.Mod
/-- The action of an additive monoid object on itself.  -/
CategoryTheory.AddModObj.regular : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    [inst_1 : CategoryTheory.MonoidalCategory C] →
      (M : C) → [inst_2 : CategoryTheory.AddMonObj M] → CategoryTheory.AddModObj M M
-- Lean.Meta.Tactic.Grind.EMatchTheorem
/-- Monad for collecting patterns for a theorem.  -/
_private.Lean.Meta.Tactic.Grind.EMatchTheorem.0.Lean.Meta.Grind.CollectorM : Type → Type
-- Mathlib.Tactic.ITauto
/-- Constructor for `p = q`.  -/
Mathlib.Tactic.ITauto.IProp.eq : Mathlib.Tactic.ITauto.IProp → Mathlib.Tactic.ITauto.IProp → Mathlib.Tactic.ITauto.IProp
-- Mathlib.Data.Multiset.Filter
Multiset.count_filter : ∀ {α : Type u_1} [inst : DecidableEq α] {p : α → Prop} [inst_1 : DecidablePred p] {a : α} {s : Multiset α},
  Multiset.count a (Multiset.filter p s) = if p a then Multiset.count a s else 0
-- Mathlib.Analysis.Complex.Hadamard
/-- The correct generalization of `interpStrip` to produce bounds in the general case.  -/
Complex.HadamardThreeLines.interpStrip' : {E : Type u_1} → [NormedAddCommGroup E] → (ℂ → E) → ℝ → ℝ → ℂ → ℂ
-- Mathlib.Topology.MetricSpace.Pseudo.Defs
Metric.uniformity_basis_dist_pow : ∀ {α : Type u} [inst : PseudoMetricSpace α] {r : ℝ},
  0 < r → r < 1 → (uniformity α).HasBasis (fun x => True) fun n => {p | dist p.1 p.2 < r ^ n}
-- Batteries.Classes.Order
Std.instOrientedCmpByKey : ∀ {α : Type u_1} {β : Type u_2} (f : α → β) (cmp : β → β → Ordering) [Std.OrientedCmp cmp],
  Std.OrientedCmp (Ordering.byKey f cmp)
-- Mathlib.Order.Antichain
IsMaxAntichain.eq_1 : ∀ {α : Type u_1} (r : α → α → Prop) (s : Set α),
  IsMaxAntichain r s = (IsAntichain r s ∧ ∀ ⦃t : Set α⦄, IsAntichain r t → s ⊆ t → s = t)
-- Lean.Meta.Tactic.Try.Collect
Lean.Meta.Try.Info : Type
-- Mathlib.RingTheory.Coprime.Lemmas
IsRelPrime.pow_left_iff : ∀ {α : Type u_1} [inst : CommMonoid α] [DecompositionMonoid α] {x y : α} {m : ℕ},
  0 < m → (IsRelPrime (x ^ m) y ↔ IsRelPrime x y)
-- Batteries.Recycling.RBTree.WF
_private.Batteries.Recycling.RBTree.WF.0.RBTree.RBNode.del.match_1.splitter : (motive : RBTree.RBColor → Sort u_1) →
  (x : RBTree.RBColor) → (Unit → motive RBTree.RBColor.black) → (Unit → motive RBTree.RBColor.red) → motive x
-- Std.Net.Addr
Std.Net.IPv4Addr.mk.inj : ∀ {octets octets_1 : Vector UInt8 4}, { octets := octets } = { octets := octets_1 } → octets = octets_1
-- Mathlib.Geometry.Manifold.Instances.Sphere
stereoInvFun.eq_1 : ∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : InnerProductSpace ℝ E] {v : E} (hv : ‖v‖ = 1) (w : ↥(ℝ ∙ v)ᗮ),
  stereoInvFun hv w = ⟨stereoInvFunAux v ↑w, ⋯⟩
-- Mathlib.Analysis.ODE.PicardLindelof
ODE.FunSpace.compProj_apply : ∀ {E : Type u_1} [inst : NormedAddCommGroup E] {tmin tmax : ℝ} {t₀ : ↑(Set.Icc tmin tmax)} {x₀ : E} {r L : NNReal}
  {α : ODE.FunSpace t₀ x₀ r L} {t : ℝ}, α.compProj t = α.toFun (Set.projIcc tmin tmax ⋯ t)