mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.CategoryTheory.Sites.PseudofunctorSheafOver
CategoryTheory.GrothendieckTopology.pseudofunctorOver_toPrelaxFunctor_toPrelaxFunctorStruct_toPrefunctor_map_toFunctor_obj_obj_obj : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] (J : CategoryTheory.GrothendieckTopology C) (A : Type u')
  [inst_1 : CategoryTheory.Category.{v', u'} A] {X Y : CategoryTheory.LocallyDiscrete Cᵒᵖ} (f : X ⟶ Y)
  (X_1 : CategoryTheory.Sheaf (J.over (Opposite.unop X.as)) A) (X_2 : (CategoryTheory.Over (Opposite.unop Y.as))ᵒᵖ),
  (((J.pseudofunctorOver A).map f).toFunctor.obj X_1).obj.obj X_2 =
    X_1.obj.obj (Opposite.op ((CategoryTheory.Over.map f.as.unop).obj (Opposite.unop X_2)))
-- Mathlib.Algebra.Ring.Subsemiring.Defs
/-- A subsemiring of a `NonAssocSemiring` inherits a `NonAssocSemiring` structure  -/
Subsemiring.toNonAssocSemiring : {R : Type u} → [inst : NonAssocSemiring R] → (s : Subsemiring R) → NonAssocSemiring ↥s
-- Mathlib.Algebra.Polynomial.Degree.Defs
Polynomial.withBotSucc_degree_eq_natDegree_add_one : ∀ {R : Type u} [inst : Semiring R] {p : Polynomial R}, p ≠ 0 → p.degree.succ = p.natDegree + 1
-- Mathlib.RingTheory.Extension.Cotangent.Basis
_private.Mathlib.RingTheory.Extension.Cotangent.Basis.0.Algebra.Generators.PresentationOfFreeCotangent.Aux.mk.sizeOf_spec : ∀ {R : Type u_1} {S : Type u_2} [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : Algebra R S] {ι : Type u_4}
  {P : Algebra.Generators R S ι} {σ : Type u_5} {b : Module.Basis σ S P.toExtension.Cotangent} [inst_3 : SizeOf R]
  [inst_4 : SizeOf S] [inst_5 : SizeOf ι] [inst_6 : SizeOf σ] (f : P.toExtension.Cotangent → ↥P.toExtension.ker)
  (hf : ∀ (b : P.toExtension.Cotangent), Algebra.Extension.Cotangent.mk (f b) = b) (g : P.Ring) (hgmem : g - 1 ∈ P.ker)
  (hg : g • P.ker ≤ Ideal.span (Set.range (Subtype.val ∘ f ∘ ⇑b))),
  sizeOf { f := f, hf := hf, g := g, hgmem := hgmem, hg := hg } = 1 + sizeOf g + sizeOf hgmem
-- Mathlib.Data.TwoPointing
TwoPointing.prop_snd : TwoPointing.prop.toProd.2 = True
-- Mathlib.Algebra.Homology.SpectralObject.Cycles
CategoryTheory.Abelian.SpectralObject.cokernelSequenceOpcycles_X₂ : ∀ {C : Type u_1} {ι : Type u_2} [inst : CategoryTheory.Category.{v_1, u_1} C]
  [inst_1 : CategoryTheory.Category.{v_2, u_2} ι] [inst_2 : CategoryTheory.Abelian C]
  (X : CategoryTheory.Abelian.SpectralObject C ι) {i j k : ι} (f : i ⟶ j) (g : j ⟶ k) (n₀ n₁ : ℤ)
  (hn₁ : autoParam (n₀ + 1 = n₁) CategoryTheory.Abelian.SpectralObject.cokernelSequenceOpcycles._auto_1),
  (X.cokernelSequenceOpcycles f g n₀ n₁ hn₁).X₂ = (X.H n₁).obj (CategoryTheory.ComposableArrows.mk₁ f)
-- Mathlib.Topology.Algebra.Group.OpenMapping
/-- Consider a sigma-compact group acting continuously and transitively on a Baire space. Then
the orbit map is open. This is a version of the open mapping theorem, valid notably for the
action of a sigma-compact locally compact group on a locally compact space.  -/
isOpenMap_smul_of_sigmaCompact : ∀ {G : Type u_1} {X : Type u_2} [inst : TopologicalSpace G] [inst_1 : TopologicalSpace X] [inst_2 : Group G]
  [IsTopologicalGroup G] [inst_4 : MulAction G X] [SigmaCompactSpace G] [BaireSpace X] [T2Space X] [ContinuousSMul G X]
  [MulAction.IsPretransitive G X] (x : X), IsOpenMap fun g => g • x
-- Mathlib.Algebra.Group.Pointwise.Finset.Basic
Finset.nsmul_eq_empty : ∀ {α : Type u_2} [inst : DecidableEq α] [inst_1 : AddMonoid α] {s : Finset α} {n : ℕ}, n • s = ∅ ↔ s = ∅ ∧ n ≠ 0
-- Lean.Meta.Tactic.Grind.EMatch
Lean.Meta.Grind.EMatch.instInhabitedCnstr.default : Lean.Meta.Grind.EMatch.Cnstr
-- Mathlib.Topology.Connected.PathConnected
IsPathConnected.mem_pathComponent : ∀ {X : Type u_1} [inst : TopologicalSpace X] {x y : X} {F : Set X},
  IsPathConnected F → x ∈ F → y ∈ F → y ∈ pathComponent x
-- Mathlib.Algebra.Notation.Pi.Defs
Pi.smul_comp : ∀ {ι : Type u_1} {α : Type u_2} {β : Type u_3} {M : Type u_7} [inst : SMul α M] (a : α) (f : β → M) (g : ι → β),
  (a • f) ∘ g = a • f ∘ g
-- Mathlib.Combinatorics.Enumerative.Composition
Composition.boundaries.eq_1 : ∀ {n : ℕ} (c : Composition n), c.boundaries = Finset.map c.boundary.toEmbedding Finset.univ
-- Mathlib.Topology.Algebra.FilterBasis
GroupFilterBasis.subset_mul_self : ∀ {G : Type u} [inst : Group G] (B : GroupFilterBasis G) {U : Set G}, U ∈ B → U ⊆ U * U
-- Std.Do.WP.Monad
/-- `WP.wp` preserves `map`.  -/
Std.Do.WPMonad.wp_map : ∀ {m : Type u → Type v} {ps : Std.Do.PostShape} {α β : Type u} [inst : Monad m] [inst_1 : Std.Do.WPMonad m ps]
  (f : α → β) (x : m α), Std.Do.wp (f <$> x) = f <$> Std.Do.wp x
-- Mathlib.Order.Hom.Bounded
/-- `BotHomClass F α β` states that `F` is a type of `⊥`-preserving morphisms.

You should extend this class when you extend `BotHom`.  -/
BotHomClass : (F : Type u_6) → (α : outParam (Type u_7)) → (β : outParam (Type u_8)) → [Bot α] → [Bot β] → [FunLike F α β] → Prop
-- Mathlib.SetTheory.Ordinal.Principal
/-- **Alias** of `Ordinal.isPrincipal_add_iff_add_left_eq_self`. -/
Ordinal.principal_add_iff_add_left_eq_self : ∀ {o : Ordinal.{u}}, Ordinal.IsPrincipal (fun x1 x2 => x1 + x2) o ↔ ∀ a < o, a + o = o
-- Mathlib.Topology.Algebra.ContinuousAffineMap
ContinuousAffineMap.instMulAction : {R : Type u_1} →
  {V : Type u_2} →
    {W : Type u_3} →
      {P : Type u_4} →
        [inst : Ring R] →
          [inst_1 : AddCommGroup V] →
            [inst_2 : Module R V] →
              [inst_3 : TopologicalSpace P] →
                [inst_4 : AddTorsor V P] →
                  [inst_5 : AddCommGroup W] →
                    [inst_6 : Module R W] →
                      {S : Type u_10} →
                        [inst_7 : TopologicalSpace W] →
                          [inst_8 : Monoid S] →
                            [inst_9 : DistribMulAction S W] →
                              [SMulCommClass R S W] → [ContinuousConstSMul S W] → MulAction S (P →ᴬ[R] W)
-- Mathlib.Algebra.Category.AlgCat.Monoidal
AlgCat.hom_inv_associator : ∀ {R : Type u} [inst : CommRing R] {M N K : AlgCat R},
  AlgCat.Hom.hom (CategoryTheory.MonoidalCategoryStruct.associator M N K).inv =
    ↑(Algebra.TensorProduct.assoc R R R ↑M ↑N ↑K).symm
-- Mathlib.CategoryTheory.SmallObject.IsCardinalForSmallObjectArgument
CategoryTheory.SmallObject.πObj_naturality : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] (I : CategoryTheory.MorphismProperty C) (κ : Cardinal.{w})
  [inst_1 : Fact κ.IsRegular] [inst_2 : OrderBot κ.ord.ToType] [inst_3 : I.IsCardinalForSmallObjectArgument κ]
  {f g : CategoryTheory.Arrow C} (φ : f ⟶ g),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.SmallObject.objMap I κ φ)
      (CategoryTheory.SmallObject.πObj I κ g.hom) =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.SmallObject.πObj I κ f.hom) (CategoryTheory.Arrow.Hom.right φ)
-- Mathlib.CategoryTheory.Limits.Constructions.Over.Basic
CategoryTheory.Over.hasLimits : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {B : C} [CategoryTheory.Limits.HasWidePullbacks C],
  CategoryTheory.Limits.HasLimitsOfSize.{w, w, v, max u v} (CategoryTheory.Over B)
-- Mathlib.GroupTheory.GroupAction.MultiplePrimitivity
/-- An `n`-preprimitive action is `m`-preprimitive for `m ≤ n`.  -/
AddAction.isMultiplyPreprimitive_of_le : ∀ (M : Type u_1) (α : Type u_2) [inst : AddGroup M] [inst_1 : AddAction M α] {n : ℕ},
  AddAction.IsMultiplyPreprimitive M α n → ∀ {m : ℕ}, m ≤ n → ↑n ≤ ENat.card α → AddAction.IsMultiplyPreprimitive M α m
-- Mathlib.Data.Finset.Insert
Finset.insert_inj : ∀ {α : Type u_1} [inst : DecidableEq α] {s : Finset α} {a b : α}, a ∉ s → (insert a s = insert b s ↔ a = b)
-- Lean.Data.Lsp.Capabilities
Lean.Lsp.ServerCapabilities.hoverProvider : Lean.Lsp.ServerCapabilities → Bool
-- Init.Data.Bool
Bool.or_left_comm : ∀ (x y z : Bool), (x || (y || z)) = (y || (x || z))
-- Mathlib.MeasureTheory.Integral.Bochner.Basic
/-- **Markov's inequality** also known as **Chebyshev's first inequality**.  -/
MeasureTheory.mul_meas_ge_le_integral_of_nonneg : ∀ {α : Type u_1} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} {f : α → ℝ},
  0 ≤ᵐ[μ] f → MeasureTheory.Integrable f μ → ∀ (ε : ℝ), ε * μ.real {x | ε ≤ f x} ≤ ∫ (x : α), f x ∂μ
-- Mathlib.LinearAlgebra.Matrix.Transvection
/-- Multiplying by all the matrices either in `listTransvecCol M` and `listTransvecRow M` kills
all the coefficients in the last row but the last one.  -/
Matrix.Pivot.listTransvecCol_mul_mul_listTransvecRow_last_col : ∀ {𝕜 : Type u_3} [inst : Field 𝕜] {r : ℕ} (M : Matrix (Fin r ⊕ Unit) (Fin r ⊕ Unit) 𝕜),
  M (Sum.inr ()) (Sum.inr ()) ≠ 0 →
    ∀ (i : Fin r),
      ((Matrix.Pivot.listTransvecCol M).prod * M * (Matrix.Pivot.listTransvecRow M).prod) (Sum.inr ()) (Sum.inl i) = 0
-- Mathlib.LinearAlgebra.Matrix.SesquilinearForm
dotProduct_toMatrix₂_mulVec : ∀ {R : Type u_1} {M₁ : Type u_6} {M₂ : Type u_7} {n : Type u_11} {m : Type u_12} [inst : CommSemiring R]
  [inst_1 : AddCommMonoid M₁] [inst_2 : Module R M₁] [inst_3 : AddCommMonoid M₂] [inst_4 : Module R M₂]
  {σ₁ σ₂ : R →+* R} [inst_5 : Fintype n] [inst_6 : Fintype m] [inst_7 : DecidableEq m] [inst_8 : DecidableEq n]
  (b₁ : Module.Basis n R M₁) (b₂ : Module.Basis m R M₂) (B : M₁ →ₛₗ[σ₁] M₂ →ₛₗ[σ₂] R) (x : n → R) (y : m → R),
  ⇑σ₁ ∘ x ⬝ᵥ ((LinearMap.toMatrix₂ b₁ b₂) B).mulVec (⇑σ₂ ∘ y) = (B (b₁.equivFun.symm x)) (b₂.equivFun.symm y)
-- Mathlib.Analysis.Convex.StrictConvexSpace
/-- If `x` and `y` are two vectors in a strictly convex space have the same norm and the norm of
their sum is equal to the sum of their norms, then they are equal.  -/
eq_of_norm_eq_of_norm_add_eq : ∀ {E : Type u_2} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] [StrictConvexSpace ℝ E] {x y : E},
  ‖x‖ = ‖y‖ → ‖x + y‖ = ‖x‖ + ‖y‖ → x = y
-- Mathlib.Algebra.Group.Prod
AddEquiv.prodAddUnits.eq_1 : ∀ {M : Type u_3} {N : Type u_4} [inst : AddMonoid M] [inst_1 : AddMonoid N],
  AddEquiv.prodAddUnits =
    { toFun := ⇑((AddUnits.map (AddMonoidHom.fst M N)).prod (AddUnits.map (AddMonoidHom.snd M N))),
      invFun := fun u => { val := (↑u.1, ↑u.2), neg := (↑(-u.1), ↑(-u.2)), val_neg := ⋯, neg_val := ⋯ }, left_inv := ⋯,
      right_inv := ⋯, map_add' := ⋯ }
-- Mathlib.Algebra.Homology.ComplexShapeSigns
/-- the signs which appear in the vertical differential of the total complex  -/
ComplexShape.TensorSigns.ε' : {I : Type u_7} → {inst : AddMonoid I} → (c : ComplexShape I) → [self : c.TensorSigns] → Multiplicative I →* ℤˣ
-- Batteries.Tactic.PrintOpaques
/-- Collects the result of a `CollectOpaques` query.  -/
Batteries.Tactic.CollectOpaques.State : Type
-- Mathlib.Probability.Kernel.Composition.Comp
/-- The **Chapman-Kolmogorov equation**, integral version.  -/
ProbabilityTheory.Kernel.pow_add_apply_eq_lintegral : ∀ {α : Type u_1} {mα : MeasurableSpace α} (κ : ProbabilityTheory.Kernel α α) (m n : ℕ) (a : α) {s : Set α},
  MeasurableSet s → ((κ ^ (m + n)) a) s = ∫⁻ (b : α), ((κ ^ n) b) s ∂(κ ^ m) a
-- Mathlib.CategoryTheory.Adjunction.Basic
CategoryTheory.Adjunction.CoreHomEquiv.mk.inj : ∀ {C : Type u₁} {inst : CategoryTheory.Category.{v₁, u₁} C} {D : Type u₂} {inst_1 : CategoryTheory.Category.{v₂, u₂} D}
  {F : CategoryTheory.Functor C D} {G : CategoryTheory.Functor D C}
  {homEquiv : (X : C) → (Y : D) → (F.obj X ⟶ Y) ≃ (X ⟶ G.obj Y)}
  {homEquiv_naturality_left_symm :
    autoParam
      (∀ {X' X : C} {Y : D} (f : X' ⟶ X) (g : X ⟶ G.obj Y),
        (homEquiv X' Y).symm (CategoryTheory.CategoryStruct.comp f g) =
          CategoryTheory.CategoryStruct.comp (F.map f) ((homEquiv X Y).symm g))
      CategoryTheory.Adjunction.CoreHomEquiv.homEquiv_naturality_left_symm._autoParam}
  {homEquiv_naturality_right :
    autoParam
      (∀ {X : C} {Y Y' : D} (f : F.obj X ⟶ Y) (g : Y ⟶ Y'),
        (homEquiv X Y') (CategoryTheory.CategoryStruct.comp f g) =
          CategoryTheory.CategoryStruct.comp ((homEquiv X Y) f) (G.map g))
      CategoryTheory.Adjunction.CoreHomEquiv.homEquiv_naturality_right._autoParam}
  {homEquiv_1 : (X : C) → (Y : D) → (F.obj X ⟶ Y) ≃ (X ⟶ G.obj Y)}
  {homEquiv_naturality_left_symm_1 :
    autoParam
      (∀ {X' X : C} {Y : D} (f : X' ⟶ X) (g : X ⟶ G.obj Y),
        (homEquiv_1 X' Y).symm (CategoryTheory.CategoryStruct.comp f g) =
          CategoryTheory.CategoryStruct.comp (F.map f) ((homEquiv_1 X Y).symm g))
      CategoryTheory.Adjunction.CoreHomEquiv.homEquiv_naturality_left_symm._autoParam}
  {homEquiv_naturality_right_1 :
    autoParam
      (∀ {X : C} {Y Y' : D} (f : F.obj X ⟶ Y) (g : Y ⟶ Y'),
        (homEquiv_1 X Y') (CategoryTheory.CategoryStruct.comp f g) =
          CategoryTheory.CategoryStruct.comp ((homEquiv_1 X Y) f) (G.map g))
      CategoryTheory.Adjunction.CoreHomEquiv.homEquiv_naturality_right._autoParam},
  { homEquiv := homEquiv, homEquiv_naturality_left_symm := homEquiv_naturality_left_symm,
        homEquiv_naturality_right := homEquiv_naturality_right } =
      { homEquiv := homEquiv_1, homEquiv_naturality_left_symm := homEquiv_naturality_left_symm_1,
        homEquiv_naturality_right := homEquiv_naturality_right_1 } →
    homEquiv = homEquiv_1
-- Init.Data.BitVec.Bitblast
/-- Recursive addition of the elements in a flattened bitvec, starting from the `rem`-th element.  -/
_private.Init.Data.BitVec.Bitblast.0.BitVec.addRecAux : {l w : ℕ} → BitVec (l * w) → ℕ → BitVec w → BitVec w
-- Mathlib.SetTheory.Ordinal.Notation
ONote.NF.of_dvd_omega0 : ∀ {e : ONote} {n : ℕ+} {a : ONote},
  (e.oadd n a).NF → Ordinal.omega0 ∣ (e.oadd n a).repr → e.repr ≠ 0 ∧ Ordinal.omega0 ∣ a.repr
-- Mathlib.MeasureTheory.Integral.Prod
MeasureTheory.setIntegral_prod_swap : ∀ {α : Type u_1} {β : Type u_2} {E : Type u_3} [inst : MeasurableSpace α] [inst_1 : MeasurableSpace β]
  {μ : MeasureTheory.Measure α} {ν : MeasureTheory.Measure β} [inst_2 : NormedAddCommGroup E] [MeasureTheory.SFinite ν]
  [inst_4 : NormedSpace ℝ E] [MeasureTheory.SFinite μ] (s : Set α) (t : Set β) (f : α × β → E),
  ∫ (z : β × α) in t ×ˢ s, f z.swap ∂ν.prod μ = ∫ (z : α × β) in s ×ˢ t, f z ∂μ.prod ν
-- Mathlib.Algebra.Homology.SpectralObject.Homology
CategoryTheory.Abelian.SpectralObject.dKernelSequence_exact : ∀ {C : Type u_1} {ι : Type u_2} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Abelian C]
  [inst_2 : CategoryTheory.Category.{v_2, u_2} ι] (X : CategoryTheory.Abelian.SpectralObject C ι)
  {i₀ i₁ i₂ i₃ i₄ i₅ : ι} (f₁ : i₀ ⟶ i₁) (f₂ : i₁ ⟶ i₂) (f₃ : i₂ ⟶ i₃) (f₄ : i₃ ⟶ i₄) (f₅ : i₄ ⟶ i₅) (f₂₃ : i₁ ⟶ i₃)
  (h₂₃ : CategoryTheory.CategoryStruct.comp f₂ f₃ = f₂₃) (n₀ n₁ n₂ n₃ : ℤ)
  (hn₁ : autoParam (n₀ + 1 = n₁) CategoryTheory.Abelian.SpectralObject.dKernelSequence_exact._auto_1)
  (hn₂ : autoParam (n₁ + 1 = n₂) CategoryTheory.Abelian.SpectralObject.dKernelSequence_exact._auto_3)
  (hn₃ : autoParam (n₂ + 1 = n₃) CategoryTheory.Abelian.SpectralObject.dKernelSequence_exact._auto_5),
  (X.dKernelSequence f₁ f₂ f₃ f₄ f₅ f₂₃ h₂₃ n₀ n₁ n₂ n₃ ⋯ ⋯ ⋯).Exact
-- Mathlib.CategoryTheory.Limits.Shapes.Reflexive
_private.Mathlib.CategoryTheory.Limits.Shapes.Reflexive.0.CategoryTheory.Limits.WalkingParallelPair.inclusionWalkingReflexivePair.match_1.eq_1 : ∀ (motive : CategoryTheory.Limits.WalkingParallelPair → Sort u_1)
  (h_1 : Unit → motive CategoryTheory.Limits.WalkingParallelPair.one)
  (h_2 : Unit → motive CategoryTheory.Limits.WalkingParallelPair.zero),
  (match CategoryTheory.Limits.WalkingParallelPair.one with
    | CategoryTheory.Limits.WalkingParallelPair.one => h_1 ()
    | CategoryTheory.Limits.WalkingParallelPair.zero => h_2 ()) =
    h_1 ()
-- Std.Data.Internal.List.Associative
Std.Internal.List.getValue_filterMap : ∀ {α : Type u} [inst : BEq α] [inst_1 : EquivBEq α] {β : Type v} {γ : Type w} {f : α → β → Option γ}
  {l : List ((_ : α) × β)} {k : α} (hl : Std.Internal.List.DistinctKeys l)
  {h :
    Std.Internal.List.containsKey k (List.filterMap (fun p => Option.map (fun x => ⟨p.fst, x⟩) (f p.fst p.snd)) l) =
      true},
  Std.Internal.List.getValue k (List.filterMap (fun p => Option.map (fun x => ⟨p.fst, x⟩) (f p.fst p.snd)) l) h =
    (f (Std.Internal.List.getKey k l ⋯) (Std.Internal.List.getValue k l ⋯)).get ⋯
-- Mathlib.Algebra.Order.Group.Unbundled.Int
Int.natAbs_sub_ne_zero_iff : ∀ {i j : ℤ}, (i - j).natAbs ≠ 0 ↔ i ≠ j
-- Mathlib.CategoryTheory.Bicategory.Adjunction.Adj
CategoryTheory.Bicategory.Adj.associator_inv_τr : ∀ {B : Type u} [inst : CategoryTheory.Bicategory B] {a b c d : CategoryTheory.Bicategory.Adj B} (α : a ⟶ b) (β : b ⟶ c)
  (γ : c ⟶ d),
  (CategoryTheory.Bicategory.associator α β γ).inv.τr = (CategoryTheory.Bicategory.associator γ.r β.r α.r).inv
-- Mathlib.MeasureTheory.Function.AEEqFun
MeasureTheory.AEEqFun.compMeasurePreserving_mk : ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} [inst : MeasurableSpace α] {μ : MeasureTheory.Measure α}
  [inst_1 : TopologicalSpace γ] [inst_2 : MeasurableSpace β] {ν : MeasureTheory.Measure β} {f : α → β} {g : β → γ}
  (hg : MeasureTheory.AEStronglyMeasurable g ν) (hf : MeasureTheory.MeasurePreserving f μ ν),
  (MeasureTheory.AEEqFun.mk g hg).compMeasurePreserving f hf = MeasureTheory.AEEqFun.mk (g ∘ f) ⋯
-- Std.Data.DTreeMap.Raw.Lemmas
Std.DTreeMap.Raw.mem_of_mem_insertMany_list : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t : Std.DTreeMap.Raw α β cmp} [Std.TransCmp cmp]
  [inst : BEq α] [Std.LawfulBEqCmp cmp],
  t.WF → ∀ {l : List ((a : α) × β a)} {k : α}, k ∈ t.insertMany l → (List.map Sigma.fst l).contains k = false → k ∈ t
-- Mathlib.Algebra.Group.Hom.Defs
/-- Additive group homomorphisms preserve subtraction.  -/
AddMonoidHom.map_add_neg : ∀ {α : Type u_2} {β : Type u_3} [inst : AddGroup α] [inst_1 : SubtractionMonoid β] (f : α →+ β) (g h : α),
  f (g + -h) = f g + -f h
-- Mathlib.Data.Finset.Sups
Finset.infs_compls_eq_diffs : ∀ {α : Type u_2} [inst : BooleanAlgebra α] [inst_1 : DecidableEq α] (s t : Finset α), s ⊼ t.compls = s.diffs t
-- Lean.Elab.Do.Legacy
_private.Lean.Elab.Do.Legacy.0.Lean.Elab.Term.Do.convertTerminalActionIntoJmp.loop : Lean.Name → Array Lean.Elab.Term.Do.Var → Lean.Elab.Term.Do.Code → Lean.MacroM Lean.Elab.Term.Do.Code
-- Mathlib.Probability.Independence.Basic
ProbabilityTheory.iIndep.of_precomp : ∀ {Ω : Type u_1} {ι : Type u_2} {m : ι → MeasurableSpace Ω} {x : MeasurableSpace Ω} {μ : MeasureTheory.Measure Ω}
  {ι' : Type u_6} {g : ι' → ι},
  Function.Surjective g → ProbabilityTheory.iIndep (m ∘ g) μ → ProbabilityTheory.iIndep m μ
-- Mathlib.MeasureTheory.Measure.NullMeasurable
MeasureTheory.measure_preimage_snd_singleton_eq_sum : ∀ {α : Type u_2} {β : Type u_3} {m0 : MeasurableSpace α} [MeasurableSingletonClass α] {mβ : MeasurableSpace β}
  [MeasurableSingletonClass β] [inst : Fintype α] (μ : MeasureTheory.Measure (α × β)) (y : β),
  μ (Prod.snd ⁻¹' {y}) = ∑ x, μ {(x, y)}
-- Mathlib.NumberTheory.LSeries.Nonvanishing
_private.Mathlib.NumberTheory.LSeries.Nonvanishing.0.DirichletCharacter.one_add_I_mul_ne_one_or : ∀ {N : ℕ} (χ : DirichletCharacter ℂ N) {y : ℝ}, y ≠ 0 ∨ χ ≠ 1 → 1 + Complex.I * ↑y ≠ 1 ∨ χ ≠ 1
-- Mathlib.Combinatorics.Colex
Finset.Colex.lt_iff_max'_mem : ∀ {α : Type u_1} [inst : LinearOrder α] {s t : Colex (Finset α)},
  s < t ↔ ∃ (h : s ≠ t), (symmDiff (ofColex s) (ofColex t)).max' ⋯ ∈ ofColex t
-- Init.Data.Array.Perm
List.Perm.of_toArray_perm : ∀ {α : Type u_1} {as bs : List α}, as.toArray.Perm bs.toArray → as.Perm bs
-- Mathlib.Topology.UniformSpace.Equicontinuity
/-- A family `F : ι → X → α` of functions from a topological space to a uniform space is
*equicontinuous on `S : Set X`* if it is equicontinuous *within `S`* at each point of `S`.  -/
EquicontinuousOn : {ι : Type u_1} →
  {X : Type u_3} → {α : Type u_6} → [tX : TopologicalSpace X] → [uα : UniformSpace α] → (ι → X → α) → Set X → Prop
-- Mathlib.Topology.Algebra.Constructions
MulOpposite.instWeaklyLocallyCompactSpace : ∀ {M : Type u_1} [inst : TopologicalSpace M] [WeaklyLocallyCompactSpace M], WeaklyLocallyCompactSpace Mᵐᵒᵖ
-- Lean.MetavarContext
/-- Counter for setting the field `index` at `LevelMetavarDecl`.  -/
Lean.MetavarContext.lmvarCounter : Lean.MetavarContext → ℕ
-- Mathlib.Topology.Order.UpperLowerSetTopology
Topology.IsUpperSet.nhdsKer_eq_upperClosure : ∀ {α : Type u_1} [inst : Preorder α] [inst_1 : TopologicalSpace α] [Topology.IsUpperSet α] (s : Set α),
  nhdsKer s = ↑(upperClosure s)
-- Std.Data.HashSet.RawLemmas
Std.HashSet.Raw.size_inter_le_size_left : ∀ {α : Type u} [inst : BEq α] [inst_1 : Hashable α] {m₁ m₂ : Std.HashSet.Raw α} [EquivBEq α] [LawfulHashable α],
  m₁.WF → m₂.WF → (m₁ ∩ m₂).size ≤ m₁.size
-- Mathlib.Topology.Algebra.Monoid.Defs
continuous_const_add : ∀ {M : Type u_1} [inst : TopologicalSpace M] [inst_1 : Add M] [SeparatelyContinuousAdd M] (m : M),
  Continuous fun x => m + x
-- Mathlib.GroupTheory.Finiteness
AddGroup.FG.out : ∀ {H : Type u_4} {inst : AddGroup H} [self : AddGroup.FG H], ⊤.FG
-- Mathlib.Topology.EMetricSpace.Lipschitz
lipschitzOnWith_iff_restrict : ∀ {α : Type u} {β : Type v} [inst : PseudoEMetricSpace α] [inst_1 : PseudoEMetricSpace β] {K : NNReal} {s : Set α}
  {f : α → β}, LipschitzOnWith K f s ↔ LipschitzWith K (s.domRestrict f)
-- Init.Data.List.Basic
/-- Returns the index of the first element for which `p` returns `true`, or `none` if there is no such
element. The index is returned as a `Fin`, which guarantees that it is in bounds.

Examples:
* `[7, 6, 5, 8, 1, 2, 6].findFinIdx? (· < 5) = some (4 : Fin 7)`
* `[7, 6, 5, 8, 1, 2, 6].findFinIdx? (· < 1) = none`
 -/
List.findFinIdx? : {α : Type u} → (α → Bool) → (l : List α) → Option (Fin l.length)
-- Mathlib.Algebra.Star.Pointwise
Set.union_star : ∀ {α : Type u_1} {s t : Set α} [inst : Star α], star (s ∪ t) = star s ∪ star t
-- Init.Data.String.Pattern.Basic
String.Slice.Pattern.ToForwardSearcher.instInhabitedDefaultForwardSearcher.default : {ρ : Type} → {pat : ρ} → {s : String.Slice} → String.Slice.Pattern.ToForwardSearcher.DefaultForwardSearcher pat s
-- Mathlib.Topology.Homotopy.TopCat.Basic
TopCat.Homotopy.h_hom_apply : ∀ {X Y : TopCat} {f₀ f₁ : X ⟶ Y} (F : TopCat.Homotopy f₀ f₁)
  (p : ↑(CategoryTheory.MonoidalCategoryStruct.tensorObj X TopCat.I)),
  (CategoryTheory.ConcreteCategory.hom F.h) p = F (TopCat.I.homeomorph p.2, p.1)
-- Mathlib.Order.SuccPred.Basic
Order.pred_eq_csSup : ∀ {α : Type u_1} [inst : ConditionallyCompleteLattice α] [inst_1 : PredOrder α] [NoMinOrder α] (a : α),
  Order.pred a = sSup (Set.Iio a)
-- Std.Data.TreeMap.Raw.Lemmas
Std.TreeMap.Raw.minKeyD_insertIfNew_le_self : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Std.TreeMap.Raw α β cmp} [Std.TransCmp cmp],
  t.WF → ∀ {k : α} {v : β} {fallback : α}, (cmp ((t.insertIfNew k v).minKeyD fallback) k).isLE = true
-- Std.Data.DTreeMap.Internal.Lemmas
Std.DTreeMap.Internal.Impl.Const.get?_union : ∀ {α : Type u} {instOrd : Ord α} {β : Type v} {m₁ m₂ : Std.DTreeMap.Internal.Impl α fun x => β} [Std.TransOrd α]
  (h₁ : m₁.WF) (h₂ : m₂.WF) {k : α},
  Std.DTreeMap.Internal.Impl.Const.get? (m₁.union m₂ ⋯ ⋯) k =
    (Std.DTreeMap.Internal.Impl.Const.get? m₂ k).or (Std.DTreeMap.Internal.Impl.Const.get? m₁ k)
-- Init.Data.Nat.Gcd
Nat.gcd_sub_mul_left_right : ∀ {m n k : ℕ}, m * k ≤ n → m.gcd (n - m * k) = m.gcd n