mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.MeasureTheory.OuterMeasure.Induced
MeasureTheory.inducedOuterMeasure_eq_extend : ∀ {α : Type u_1} [inst : MeasurableSpace α] {m : (s : Set α) → MeasurableSet s → ENNReal} (m0 : m ∅ ⋯ = 0),
  (∀ ⦃f : ℕ → Set α⦄ (hm : ∀ (i : ℕ), MeasurableSet (f i)),
      Pairwise (Function.onFun Disjoint f) → m (⋃ i, f i) ⋯ = ∑' (i : ℕ), m (f i) ⋯) →
    ∀ {s : Set α}, MeasurableSet s → (MeasureTheory.inducedOuterMeasure m ⋯ m0) s = MeasureTheory.extend m s
-- Std.Http.Data.Body.Basic
/-- Typeclass for values that can be read as HTTP body streams.
 -/
Std.Http.Body : Type → Type
-- Mathlib.Algebra.Group.Equiv.TypeTags
AddEquiv.toMultiplicative_symm_apply_symm_apply : ∀ {G : Type u_2} {H : Type u_3} [inst : AddZeroClass G] [inst_1 : AddZeroClass H]
  (f : Multiplicative G ≃* Multiplicative H) (a : H),
  (AddEquiv.toMultiplicative.symm f).symm a = (AddMonoidHom.toMultiplicative.symm f.symm.toMonoidHom) a
-- Mathlib.Order.Filter.AtTopBot.Basic
/-- The `atTop` filter for `↑(Ioi a)` comes from the `atTop` filter in the ambient order.  -/
Filter.atTop_Ioi_eq : ∀ {α : Type u_3} [inst : Preorder α] [IsDirectedOrder α] (a : α), Filter.atTop = Filter.comap Subtype.val Filter.atTop
-- Std.Sync.Broadcast
_private.Std.Sync.Broadcast.0.Std.Slot.mk : {α : Type} → Option α → ℕ → ℕ → Std.Slot✝ α
-- Mathlib.Algebra.Homology.TotalComplexSymmetry
HomologicalComplex₂.totalFlipIso.eq_1 : ∀ {C : Type u_1} {I₁ : Type u_2} {I₂ : Type u_3} {J : Type u_4} [inst : CategoryTheory.Category.{v_1, u_1} C]
  [inst_1 : CategoryTheory.Preadditive C] {c₁ : ComplexShape I₁} {c₂ : ComplexShape I₂}
  (K : HomologicalComplex₂ C c₁ c₂) (c : ComplexShape J) [inst_2 : TotalComplexShape c₁ c₂ c]
  [inst_3 : TotalComplexShape c₂ c₁ c] [inst_4 : TotalComplexShapeSymmetry c₁ c₂ c] [inst_5 : K.HasTotal c]
  [inst_6 : DecidableEq J], K.totalFlipIso c = HomologicalComplex.Hom.isoOfComponents (K.totalFlipIsoX c) ⋯
-- Mathlib.Data.ENat.Basic
ENat.eq_top_of_pow : ∀ {a : ℕ∞} (n : ℕ), a ^ n = ⊤ → a = ⊤
-- Mathlib.Algebra.Group.Even
even_toAdd_iff : ∀ {α : Type u_2} [inst : Add α] {a : Multiplicative α}, Even (Multiplicative.toAdd a) ↔ IsSquare a
-- Mathlib.MeasureTheory.Measure.EverywherePos
/-- Any compact set contained in `s \ μ.everywherePosSubset s` has zero measure.  -/
MeasureTheory.Measure.measure_eq_zero_of_subset_sdiff_everywherePosSubset : ∀ {α : Type u_1} [inst : TopologicalSpace α] [inst_1 : MeasurableSpace α] {μ : MeasureTheory.Measure α} {s k : Set α},
  IsCompact k → k ⊆ s \ μ.everywherePosSubset s → μ k = 0
-- Mathlib.RingTheory.Smooth.Locus
/-- `Algebra.smoothLocus R A` is the set of primes `p` of `A`
such that `Aₚ` is formally smooth over `R`.  -/
Algebra.smoothLocus : (R : Type u_1) → (A : Type u_2) → [inst : CommRing R] → [inst_1 : CommRing A] → [Algebra R A] → Set (PrimeSpectrum A)
-- Mathlib.CategoryTheory.Limits.Shapes.RegularMono
/-- A regular epimorphism in `Cᵒᵖ` induces a regular monomorphism in `C`.  -/
CategoryTheory.RegularEpi.unop : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    {X Y : Cᵒᵖ} → {f : X ⟶ Y} → CategoryTheory.RegularEpi f → CategoryTheory.RegularMono f.unop
-- Std.Data.TreeMap.Raw.Lemmas
Std.TreeMap.Raw.getKey!_insertMany_list_of_mem : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Std.TreeMap.Raw α β cmp} [Std.TransCmp cmp]
  [inst : Inhabited α],
  t.WF →
    ∀ {l : List (α × β)} {k k' : α},
      cmp k k' = Ordering.eq →
        List.Pairwise (fun a b => ¬cmp a.1 b.1 = Ordering.eq) l →
          k ∈ List.map Prod.fst l → (t.insertMany l).getKey! k' = k
-- Mathlib.Order.Basic
/-- Transfer a `Preorder` on `β` to a `Preorder` on `α` using a function `f : α → β`.

See also `Function.Injective.preorder` when only the proof fields need to be transferred.

See note [reducible non-instances].  -/
Preorder.lift : {α : Type u_2} → {β : Type u_3} → [Preorder β] → (α → β) → Preorder α
-- Mathlib.Algebra.Order.Floor.Extended
ENat.floor_add_one : ∀ (r : ENNReal), ⌊r + 1⌋ₑ = ⌊r⌋ₑ + 1
-- Mathlib.CategoryTheory.Functor.CurryingThree
CategoryTheory.Functor.curry₃ObjProdComp_inv_app_app_app : ∀ {C₁ : Type u_1} {C₂ : Type u_2} {C₃ : Type u_4} {D₁ : Type u_6} {D₂ : Type u_7} {D₃ : Type u_8} {E : Type u_9}
  [inst : CategoryTheory.Category.{v_1, u_1} C₁] [inst_1 : CategoryTheory.Category.{v_2, u_2} C₂]
  [inst_2 : CategoryTheory.Category.{v_3, u_4} C₃] [inst_3 : CategoryTheory.Category.{v_6, u_6} D₁]
  [inst_4 : CategoryTheory.Category.{v_7, u_7} D₂] [inst_5 : CategoryTheory.Category.{v_8, u_8} D₃]
  [inst_6 : CategoryTheory.Category.{v_9, u_9} E] (F₁ : CategoryTheory.Functor C₁ D₁)
  (F₂ : CategoryTheory.Functor C₂ D₂) (F₃ : CategoryTheory.Functor C₃ D₃) (G : CategoryTheory.Functor (D₁ × D₂ × D₃) E)
  (X : C₁) (X_1 : C₂) (X_2 : C₃),
  (((F₁.curry₃ObjProdComp F₂ F₃ G).inv.app X).app X_1).app X_2 =
    CategoryTheory.CategoryStruct.id
      ((((CategoryTheory.Functor.curry₃.obj ((F₁.prod (F₂.prod F₃)).comp G)).obj X).obj X_1).obj X_2)
-- Mathlib.SetTheory.Cardinal.Basic
Cardinal.isStrongLimit_aleph0 : Cardinal.aleph0.IsStrongLimit
-- Lean.Data.SMap
/-- Move from stage 1 into stage 2.  -/
Lean.SMap.switch : {α : Type u} → {β : Type v} → [inst : BEq α] → [inst_1 : Hashable α] → Lean.SMap α β → Lean.SMap α β
-- Mathlib.Algebra.Homology.Homotopy
HomologicalComplex.homotopyEquivalences.of_isIso : ∀ {ι : Type u_1} {V : Type u} [inst : CategoryTheory.Category.{v, u} V] [inst_1 : CategoryTheory.Preadditive V]
  {c : ComplexShape ι} {C D : HomologicalComplex V c} (f : C ⟶ D) [CategoryTheory.IsIso f],
  HomologicalComplex.homotopyEquivalences V c f
-- Mathlib.Combinatorics.SimpleGraph.Walk.Operations
SimpleGraph.Walk.reverseAux_eq_reverse_append : ∀ {V : Type u} {G : SimpleGraph V} {u v w : V} (p : G.Walk u v) (q : G.Walk u w), p.reverseAux q = p.reverse.append q
-- Mathlib.CategoryTheory.Limits.MorphismProperty
/-- If `P` is closed under colimits of shape `J` in `Comma L R`, then when `D` has
a colimit in `Comma L R`, the forgetful functor creates this colimit.  -/
CategoryTheory.MorphismProperty.Comma.forgetCreatesColimitOfClosed : {T : Type u_1} →
  [inst : CategoryTheory.Category.{v_1, u_1} T] →
    (P : CategoryTheory.MorphismProperty T) →
      {A : Type u_2} →
        {B : Type u_3} →
          {J : Type u_4} →
            [inst_1 : CategoryTheory.Category.{v_2, u_2} A] →
              [inst_2 : CategoryTheory.Category.{v_3, u_3} B] →
                [inst_3 : CategoryTheory.Category.{v_4, u_4} J] →
                  {L : CategoryTheory.Functor A T} →
                    {R : CategoryTheory.Functor B T} →
                      (D : CategoryTheory.Functor J (CategoryTheory.MorphismProperty.Comma L R P ⊤ ⊤)) →
                        [(CategoryTheory.MorphismProperty.commaObj L R P).IsClosedUnderColimitsOfShape J] →
                          [CategoryTheory.Limits.HasColimit
                                (D.comp (CategoryTheory.MorphismProperty.Comma.forget L R P ⊤ ⊤))] →
                            CategoryTheory.CreatesColimit D (CategoryTheory.MorphismProperty.Comma.forget L R P ⊤ ⊤)
-- Mathlib.Algebra.Order.BigOperators.Group.Finset
Finset.prod_le_one' : ∀ {ι : Type u_1} {N : Type u_5} [inst : CommMonoid N] [inst_1 : Preorder N] {f : ι → N} {s : Finset ι} [MulLeftMono N],
  (∀ i ∈ s, f i ≤ 1) → ∏ i ∈ s, f i ≤ 1
-- Mathlib.CategoryTheory.Limits.Shapes.BinaryBiproducts
/-- A binary bicone for a pair of objects `P Q : C` consists of the cone point `X`,
maps from `X` to both `P` and `Q`, and maps from both `P` and `Q` to `X`,
so that `inl ≫ fst = 𝟙 P`, `inl ≫ snd = 0`, `inr ≫ fst = 0`, and `inr ≫ snd = 𝟙 Q`  -/
CategoryTheory.Limits.BinaryBicone.inr_fst_assoc : ∀ {C : Type uC} [inst : CategoryTheory.Category.{uC', uC} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  {P Q : C} (self : CategoryTheory.Limits.BinaryBicone P Q) {Z : C} (h : P ⟶ Z),
  CategoryTheory.CategoryStruct.comp self.inr (CategoryTheory.CategoryStruct.comp self.fst h) =
    CategoryTheory.CategoryStruct.comp 0 h
-- Mathlib.Order.SuccPred.Basic
Order.Ioc_pred_left_eq_insert_of_not_isMin : ∀ {α : Type u_1} [inst : LinearOrder α] [inst_1 : PredOrder α] {a b : α},
  b ≤ a → ¬IsMin b → Set.Ioc (Order.pred b) a = insert b (Set.Ioc b a)
-- Mathlib.Topology.Algebra.Module.Alternating.Topology
ContinuousAlternatingMap.uniformContinuous_restrictScalars : ∀ {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} {ι : Type u_4} [inst : NormedField 𝕜] [inst_1 : AddCommGroup E]
  [inst_2 : Module 𝕜 E] [inst_3 : TopologicalSpace E] [inst_4 : AddCommGroup F] [inst_5 : Module 𝕜 F]
  [inst_6 : UniformSpace F] [inst_7 : IsUniformAddGroup F] (𝕜' : Type u_5) [inst_8 : NontriviallyNormedField 𝕜']
  [inst_9 : NormedAlgebra 𝕜' 𝕜] [inst_10 : Module 𝕜' E] [inst_11 : IsScalarTower 𝕜' 𝕜 E] [inst_12 : Module 𝕜' F]
  [inst_13 : IsScalarTower 𝕜' 𝕜 F] [ContinuousSMul 𝕜 E], UniformContinuous (ContinuousAlternatingMap.restrictScalars 𝕜')
-- Init.Data.FloatArray.Basic
_private.Init.Data.FloatArray.Basic.0.FloatArray.forIn.loop : {β : Type v} →
  {m : Type v → Type w} →
    [Monad m] → (as : FloatArray) → (Float → β → m (ForInStep β)) → (i : ℕ) → i ≤ as.size → β → m β
-- Mathlib.CategoryTheory.Limits.Shapes.Images
CategoryTheory.Limits.image.factorThruImage_preComp_assoc : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {X Y : C} (f : X ⟶ Y) {Z : C} (g : Y ⟶ Z)
  [inst_1 : CategoryTheory.Limits.HasImage g]
  [inst_2 : CategoryTheory.Limits.HasImage (CategoryTheory.CategoryStruct.comp f g)] {Z_1 : C}
  (h : CategoryTheory.Limits.image g ⟶ Z_1),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.factorThruImage (CategoryTheory.CategoryStruct.comp f g))
      (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.image.preComp f g) h) =
    CategoryTheory.CategoryStruct.comp f
      (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.factorThruImage g) h)
-- Mathlib.Geometry.Manifold.MFDeriv.NormedSpace
/-- `d% f x` (scoped to the `Manifold` namespace) elaborates to `mvfderiv I J f x`,
trying to determine `I` and `J` from the local context.  -/
Manifold.«termD%__» : Lean.ParserDescr
-- Mathlib.Analysis.InnerProductSpace.Defs
InnerProductSpace.Core.inner_zero_left : ∀ {𝕜 : Type u_1} {F : Type u_3} [inst : RCLike 𝕜] [inst_1 : AddCommGroup F] [inst_2 : Module 𝕜 F]
  [c : PreInnerProductSpace.Core 𝕜 F] (x : F), inner 𝕜 0 x = 0
-- Mathlib.Algebra.Colimit.Module
AddCommGroup.DirectLimit.congr_apply_of : ∀ {ι : Type u_2} [inst : Preorder ι] {G : ι → Type u_3} [inst_1 : (i : ι) → AddCommMonoid (G i)]
  {f : (i j : ι) → i ≤ j → G i →+ G j} [inst_2 : DecidableEq ι] {G' : ι → Type u_5}
  [inst_3 : (i : ι) → AddCommMonoid (G' i)] {f' : (i j : ι) → i ≤ j → G' i →+ G' j} (e : (i : ι) → G i ≃+ G' i)
  (he : ∀ (i j : ι) (h : i ≤ j), (e j).toAddMonoidHom.comp (f i j h) = (f' i j h).comp ↑(e i)) {i : ι} (g : G i),
  (AddCommGroup.DirectLimit.congr e he) ((AddCommGroup.DirectLimit.of G f i) g) =
    (AddCommGroup.DirectLimit.of G' f' i) ((e i) g)
-- Mathlib.Topology.Instances.EReal.Lemmas
EReal.continuous_coe_iff : ∀ {α : Type u_1} [inst : TopologicalSpace α] {f : α → ℝ}, (Continuous fun a => ↑(f a)) ↔ Continuous f
-- Mathlib.CategoryTheory.Limits.Shapes.Pullback.Cospan
CategoryTheory.Limits.cospan_right : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {X Y Z : C} (f : X ⟶ Z) (g : Y ⟶ Z),
  (CategoryTheory.Limits.cospan f g).obj CategoryTheory.Limits.WalkingCospan.right = Y
-- Mathlib.CategoryTheory.Sites.Whiskering
/-- Composing a functor which `HasSheafCompose`, yields a functor between sheaf categories.  -/
CategoryTheory.sheafCompose : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    {A : Type u₂} →
      [inst_1 : CategoryTheory.Category.{v₂, u₂} A] →
        {B : Type u₃} →
          [inst_2 : CategoryTheory.Category.{v₃, u₃} B] →
            (J : CategoryTheory.GrothendieckTopology C) →
              (F : CategoryTheory.Functor A B) →
                [J.HasSheafCompose F] → CategoryTheory.Functor (CategoryTheory.Sheaf J A) (CategoryTheory.Sheaf J B)
-- Std.Data.ExtDHashMap.Lemmas
Std.ExtDHashMap.Const.get!.congr_simp : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} {β : Type v} [inst : EquivBEq α] [inst_1 : LawfulHashable α]
  [inst_2 : Inhabited β] (m m_1 : Std.ExtDHashMap α fun x => β),
  m = m_1 → ∀ (a a_1 : α), a = a_1 → Std.ExtDHashMap.Const.get! m a = Std.ExtDHashMap.Const.get! m_1 a_1
-- Std.Time.Zoned.Database.TzIf
/-- The array of leap second records.
 -/
Std.Time.TimeZone.TZif.TZifV1.leapSeconds : Std.Time.TimeZone.TZif.TZifV1 → Array Std.Time.TimeZone.TZif.LeapSecond
-- Mathlib.Data.Finset.Prod
Finset.filter_product_left : ∀ {α : Type u_1} {β : Type u_2} {s : Finset α} {t : Finset β} (p : α → Prop) [inst : DecidablePred p],
  {x ∈ s ×ˢ t | p x.1} = Finset.filter p s ×ˢ t
-- Mathlib.Analysis.Normed.Ring.Basic
SeminormedCommRing.toSeminormedRing : {α : Type u_5} → [self : SeminormedCommRing α] → SeminormedRing α
-- Mathlib.CategoryTheory.MorphismProperty.OfObjectProperty
CategoryTheory.MorphismProperty.ofObjectProperty_inverseImage : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] (P Q : CategoryTheory.ObjectProperty C) {D : Type u_2}
  [inst_1 : CategoryTheory.Category.{v_2, u_2} D] (F : CategoryTheory.Functor D C),
  CategoryTheory.MorphismProperty.ofObjectProperty (P.inverseImage F) (Q.inverseImage F) =
    (CategoryTheory.MorphismProperty.ofObjectProperty P Q).inverseImage F
-- Mathlib.AlgebraicGeometry.Sites.Proetale
AlgebraicGeometry.Scheme.ProEt.instSubcanonicalTopology : ∀ (S : AlgebraicGeometry.Scheme), (AlgebraicGeometry.Scheme.ProEt.topology S).Subcanonical
-- Init.Data.Rat.Lemmas
Rat.mul_neg_iff_of_pos_left : ∀ {a b : ℚ}, 0 < a → (a * b < 0 ↔ b < 0)
-- Mathlib.Order.PartialSups
iSup_le_iSup_of_partialSups_le_partialSups : ∀ {α : Type u_1} {ι : Type u_3} [inst : Preorder ι] [inst_1 : LocallyFiniteOrderBot ι] [inst_2 : CompleteLattice α]
  {f g : ι → α}, partialSups f ≤ partialSups g → ⨆ i, f i ≤ ⨆ i, g i
-- Mathlib.Analysis.Normed.Module.Multilinear.Basic
/-- If a multilinear map satisfies an inequality `‖f m‖ ≤ C * ∏ i, ‖m i‖`, then it is
continuous.  -/
MultilinearMap.continuous_of_bound : ∀ {𝕜 : Type u} {ι : Type v} {E : ι → Type wE} {G : Type wG} [inst : NontriviallyNormedField 𝕜]
  [inst_1 : (i : ι) → SeminormedAddCommGroup (E i)] [inst_2 : (i : ι) → NormedSpace 𝕜 (E i)]
  [inst_3 : SeminormedAddCommGroup G] [inst_4 : NormedSpace 𝕜 G] [inst_5 : Fintype ι] (f : MultilinearMap 𝕜 E G)
  (C : ℝ), (∀ (m : (i : ι) → E i), ‖f m‖ ≤ C * ∏ i, ‖m i‖) → Continuous ⇑f
-- Mathlib.Analysis.InnerProductSpace.Adjoint
ContinuousLinearMap.adjoint.congr_simp : ∀ {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [inst : RCLike 𝕜] [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedAddCommGroup F] [inst_3 : InnerProductSpace 𝕜 E] [inst_4 : InnerProductSpace 𝕜 F]
  [inst_5 : CompleteSpace E] [inst_6 : CompleteSpace F], ContinuousLinearMap.adjoint = ContinuousLinearMap.adjoint
-- Mathlib.Algebra.Category.Grp.Basic
GrpCat.hasForgetToMonCat : CategoryTheory.HasForget₂ GrpCat MonCat
-- Lean.Parser.Extra
Lean.Parser.many1Indent.formatter : Lean.PrettyPrinter.Formatter → Lean.PrettyPrinter.Formatter
-- Lean.Data.NameMap.Basic
Lean.NameSet.instAppend : Append Lean.NameSet
-- Mathlib.Algebra.Group.WithOne.Defs
WithZero.instNegZeroClass : {α : Type u} → [Neg α] → NegZeroClass (WithZero α)
-- Mathlib.CategoryTheory.Limits.Shapes.Multiequalizer
CategoryTheory.Limits.MulticospanIndex.toPiForkFunctor_map_hom : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {J : CategoryTheory.Limits.MulticospanShape}
  (I : CategoryTheory.Limits.MulticospanIndex J C) {c : CategoryTheory.Limits.Fan I.left}
  (hc : CategoryTheory.Limits.IsLimit c) {d : CategoryTheory.Limits.Fan I.right} (hd : CategoryTheory.Limits.IsLimit d)
  {K₁ K₂ : CategoryTheory.Limits.Multifork I} (f : K₁ ⟶ K₂), ((I.toPiForkFunctor hc hd).map f).hom = f.hom
-- Batteries.Data.UInt
UInt16.toUInt64_toNat : ∀ (x : UInt16), x.toUInt64.toNat = x.toNat
-- Mathlib.Data.ZMod.Basic
ZMod.addOrderOf_one : ∀ (n : ℕ), addOrderOf 1 = n
-- Mathlib.GroupTheory.GroupAction.Blocks
AddAction.IsBlock.disjoint_vadd_left : ∀ {M : Type u_1} {X : Type u_2} [inst : AddMonoid M] [inst_1 : AddAction M X] {B : Set X} {s : Set M},
  AddAction.IsBlock M B → ¬B ⊆ s +ᵥ B → Disjoint (s +ᵥ B) B
-- Mathlib.CategoryTheory.MorphismProperty.Basic
/-- The `MorphismProperty C` satisfied by monomorphisms in `C`.  -/
CategoryTheory.MorphismProperty.monomorphisms : (C : Type u) → [inst : CategoryTheory.Category.{v, u} C] → CategoryTheory.MorphismProperty C
-- Std.Data.DHashMap.Internal.RawLemmas
_private.Std.Data.DHashMap.Internal.RawLemmas.0.Std.DHashMap.Raw.emptyWithCapacity.eq_1 : ∀ {α : Type u} {β : α → Type v} (capacity : ℕ),
  Std.DHashMap.Raw.emptyWithCapacity capacity = ↑(Std.DHashMap.Internal.Raw₀.emptyWithCapacity capacity)
-- Mathlib.CategoryTheory.Category.ULift
CategoryTheory.instSmallCategoryAsSmall : {C : Type u₁} → [inst : CategoryTheory.Category.{v₁, u₁} C] → CategoryTheory.SmallCategory (CategoryTheory.AsSmall C)
-- Init.SizeOf
Decidable.isFalse.sizeOf_spec : ∀ {p : Prop} [inst : SizeOf p] (h : ¬p), sizeOf (isFalse h) = 1
-- Mathlib.Algebra.BigOperators.Group.Finset.Piecewise
Finset.sum_update_of_notMem : ∀ {ι : Type u_1} {M : Type u_3} [inst : AddCommMonoid M] [inst_1 : DecidableEq ι] {s : Finset ι} {i : ι},
  i ∉ s → ∀ (f : ι → M) (b : M), ∑ x ∈ s, Function.update f i b x = ∑ x ∈ s, f x
-- Mathlib.Algebra.Homology.HomotopyCategory.Plus
/-- The pre-cylinder object attached to `K : Plus C`.  -/
CochainComplex.Plus.precylinder : {C : Type u_1} →
  [inst : CategoryTheory.Category.{v_1, u_1} C] →
    [inst_1 : CategoryTheory.Preadditive C] →
      [CategoryTheory.Limits.HasBinaryBiproducts C] → (K : CochainComplex.Plus C) → HomotopicalAlgebra.Precylinder K
-- Init.Data.UInt.Lemmas
UInt16.right_eq_add : ∀ {a b : UInt16}, b = a + b ↔ a = 0
-- Init.ShareCommon
ShareCommon.StateFactoryBuilder.mk.injEq : ∀ (Map : (α : Type) → Type → [BEq α] → [Hashable α] → Type)
  (mkMap : {α β : Type} → [inst : BEq α] → [inst_1 : Hashable α] → ℕ → Map α β)
  (mapFind? : {α β : Type} → [inst : BEq α] → [inst_1 : Hashable α] → Map α β → α → Option β)
  (mapInsert : {α β : Type} → [inst : BEq α] → [inst_1 : Hashable α] → Map α β → α → β → Map α β)
  (Set : (α : Type) → [BEq α] → [Hashable α] → Type)
  (mkSet : {α : Type} → [inst : BEq α] → [inst_1 : Hashable α] → ℕ → Set α)
  (setFind? : {α : Type} → [inst : BEq α] → [inst_1 : Hashable α] → Set α → α → Option α)
  (setInsert : {α : Type} → [inst : BEq α] → [inst_1 : Hashable α] → Set α → α → Set α)
  (Map_1 : (α : Type) → Type → [BEq α] → [Hashable α] → Type)
  (mkMap_1 : {α β : Type} → [inst : BEq α] → [inst_1 : Hashable α] → ℕ → Map_1 α β)
  (mapFind?_1 : {α β : Type} → [inst : BEq α] → [inst_1 : Hashable α] → Map_1 α β → α → Option β)
  (mapInsert_1 : {α β : Type} → [inst : BEq α] → [inst_1 : Hashable α] → Map_1 α β → α → β → Map_1 α β)
  (Set_1 : (α : Type) → [BEq α] → [Hashable α] → Type)
  (mkSet_1 : {α : Type} → [inst : BEq α] → [inst_1 : Hashable α] → ℕ → Set_1 α)
  (setFind?_1 : {α : Type} → [inst : BEq α] → [inst_1 : Hashable α] → Set_1 α → α → Option α)
  (setInsert_1 : {α : Type} → [inst : BEq α] → [inst_1 : Hashable α] → Set_1 α → α → Set_1 α),
  ({ Map := Map, mkMap := mkMap, mapFind? := mapFind?, mapInsert := mapInsert, Set := Set, mkSet := mkSet,
        setFind? := setFind?, setInsert := setInsert } =
      { Map := Map_1, mkMap := mkMap_1, mapFind? := mapFind?_1, mapInsert := mapInsert_1, Set := Set_1,
        mkSet := mkSet_1, setFind? := setFind?_1, setInsert := setInsert_1 }) =
    (Map = Map_1 ∧
      mkMap ≍ mkMap_1 ∧
        mapFind? ≍ mapFind?_1 ∧
          mapInsert ≍ mapInsert_1 ∧ Set = Set_1 ∧ mkSet ≍ mkSet_1 ∧ setFind? ≍ setFind?_1 ∧ setInsert ≍ setInsert_1)
-- Mathlib.LinearAlgebra.Matrix.Cartan
CartanMatrix.D_transpose : ∀ (n : ℕ), (CartanMatrix.D n).transpose = CartanMatrix.D n
-- Mathlib.Topology.CWComplex.Classical.Basic
Topology.RelCWComplex.nonempty_cellFrontier : ∀ {X : Type u_1} [t : TopologicalSpace X] {C : Set X} [inst : Topology.CWComplex C] {n : ℕ},
  n ≠ 0 → ∀ (j : Topology.RelCWComplex.cell C n), (Topology.RelCWComplex.cellFrontier n j).Nonempty
-- Mathlib.CategoryTheory.LiftingProperties.Basic
CategoryTheory.HasLiftingPropertyFixedBot.eq_1 : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] {A B X Y : C} (p : Y ⟶ X) (i : B ⟶ A) (t : X ⟶ A),
  CategoryTheory.HasLiftingPropertyFixedBot p i t = ∀ (b : Y ⟶ B) (sq : CategoryTheory.CommSq b p i t), sq.HasLift
-- Std.Data.TreeMap.Raw.Lemmas
Std.TreeMap.Raw.Equiv.getEntryLE?_eq : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t₁ t₂ : Std.TreeMap.Raw α β cmp} [Std.TransCmp cmp] {k : α},
  t₁.WF → t₂.WF → t₁.Equiv t₂ → t₁.getEntryLE? k = t₂.getEntryLE? k
-- Std.Data.TreeMap.Raw.Lemmas
Std.TreeMap.Raw.getElem?_insertIfNew : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Std.TreeMap.Raw α β cmp} [Std.TransCmp cmp],
  t.WF → ∀ {k a : α} {v : β}, (t.insertIfNew k v)[a]? = if cmp k a = Ordering.eq ∧ k ∉ t then some v else t[a]?
-- Mathlib.Analysis.Calculus.Deriv.Mul
deriv_smul : ∀ {𝕜 : Type u} [inst : NontriviallyNormedField 𝕜] {F : Type v} [inst_1 : NormedAddCommGroup F]
  [inst_2 : NormedSpace 𝕜 F] {f : 𝕜 → F} {x : 𝕜} {𝕜' : Type u_2} [inst_3 : NormedRing 𝕜'] [inst_4 : NormedAlgebra 𝕜 𝕜']
  [inst_5 : Module 𝕜' F] [IsBoundedSMul 𝕜' F] [IsScalarTower 𝕜 𝕜' F] {c : 𝕜 → 𝕜'},
  DifferentiableAt 𝕜 c x → DifferentiableAt 𝕜 f x → deriv (c • f) x = c x • deriv f x + deriv c x • f x
-- Mathlib.Data.Set.Insert
Set.insert_union_distrib : ∀ {α : Type u_1} (a : α) (s t : Set α), insert a (s ∪ t) = insert a s ∪ insert a t
-- Std.Data.TreeSet.Raw.Lemmas
Std.TreeSet.Raw.size_toArray : ∀ {α : Type u} {cmp : α → α → Ordering} {t : Std.TreeSet.Raw α cmp} [Std.TransCmp cmp], t.WF → t.toArray.size = t.size
-- Std.Data.TreeSet.Raw.Lemmas
Std.TreeSet.Raw.mem_union_of_right : ∀ {α : Type u} {cmp : α → α → Ordering} {t₁ t₂ : Std.TreeSet.Raw α cmp} [Std.TransCmp cmp],
  t₁.WF → t₂.WF → ∀ {k : α}, k ∈ t₂ → k ∈ t₁ ∪ t₂
-- Mathlib.Data.Int.Range
Int.decidableLELE : (P : ℤ → Prop) → [DecidablePred P] → (m n : ℤ) → Decidable (∀ (r : ℤ), m ≤ r → r ≤ n → P r)
-- Mathlib.ModelTheory.ElementarySubstructures
/-- A substructure is elementary when every formula applied to a tuple in the substructure
agrees with its value in the overall structure.  -/
FirstOrder.Language.Substructure.IsElementary : {L : FirstOrder.Language} → {M : Type u_1} → [inst : L.Structure M] → L.Substructure M → Prop
-- Mathlib.CategoryTheory.Functor.FullyFaithful
CategoryTheory.Functor.mapIso_injective : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  {X Y : C} (F : CategoryTheory.Functor C D) [F.Faithful], Function.Injective F.mapIso
-- Std.Data.DTreeMap.Internal.Lemmas
Std.DTreeMap.Internal.Impl.Equiv.getKey!_eq : ∀ {α : Type u} {β : α → Type v} {instOrd : Ord α} {t₁ t₂ : Std.DTreeMap.Internal.Impl α β} [Std.TransOrd α]
  [inst : Inhabited α], t₁.WF → t₂.WF → t₁.Equiv t₂ → ∀ {k : α}, t₁.getKey! k = t₂.getKey! k
-- Lean.Meta.ExprLens
_private.Lean.Meta.ExprLens.0.Lean.Meta.viewAux : {M : Type → Type} →
  [Monad M] →
    [MonadLiftT Lean.MetaM M] →
      [MonadControlT Lean.MetaM M] →
        [Lean.MonadError M] →
          {α : Type} → (Array Lean.Expr → Lean.Expr → M α) → Array Lean.Expr → List ℕ → Lean.Expr → M α
-- Std.Tactic.BVDecide.Bitblast.BoolExpr.Basic
Std.Tactic.BVDecide.BoolExpr.eval_const : ∀ {α : Type} {a : α → Bool} {b : Bool}, Std.Tactic.BVDecide.BoolExpr.eval a (Std.Tactic.BVDecide.BoolExpr.const b) = b
-- Mathlib.NumberTheory.SelbergSieve
/-- The set of natural numbers that is to be sifted. The fundamental lemma yields an upper bound
on the size of this set after the multiples of small primes have been removed.  -/
BoundingSieve.support : BoundingSieve → Finset ℕ
-- Std.Data.Iterators.Lemmas.Producers.Slice
Std.Slice.toList_eq_toList_iter : ∀ {γ : Type u} {α β : Type v} {s : Std.Slice γ} [inst : Std.ToIterator (Std.Slice γ) Id α β]
  [inst_1 : Std.Iterator α Id β] [Std.Iterators.Finite α Id], s.toList = s.iter.toList
-- Mathlib.Combinatorics.SimpleGraph.Copy
SimpleGraph.Copy.toHom_apply : ∀ {α : Type u_4} {β : Type u_5} {A : SimpleGraph α} {B : SimpleGraph β} (f : A.Copy B) (a : α), f.toHom a = f a