mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.CategoryTheory.Bicategory.Functor.Pseudofunctor
CategoryTheory.Pseudofunctor.mapComp_assoc_right_hom : ∀ {B : Type u₁} [inst : CategoryTheory.Bicategory B] {C : Type u₂} [inst_1 : CategoryTheory.Bicategory C]
  (F : CategoryTheory.Pseudofunctor B C) {a b c d : B} (f : a ⟶ b) (g : b ⟶ c) (h : c ⟶ d),
  CategoryTheory.CategoryStruct.comp (F.mapComp f (CategoryTheory.CategoryStruct.comp g h)).hom
      (CategoryTheory.Bicategory.whiskerLeft (F.map f) (F.mapComp g h).hom) =
    CategoryTheory.CategoryStruct.comp (F.map₂ (CategoryTheory.Bicategory.associator f g h).inv)
      (CategoryTheory.CategoryStruct.comp (F.mapComp (CategoryTheory.CategoryStruct.comp f g) h).hom
        (CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.whiskerRight (F.mapComp f g).hom (F.map h))
          (CategoryTheory.Bicategory.associator (F.map f) (F.map g) (F.map h)).hom))
-- Mathlib.AlgebraicGeometry.EllipticCurve.DivisionPolynomial.Basic
WeierstrassCurve.ψ_two : ∀ {R : Type r} [inst : CommRing R] (W : WeierstrassCurve R), W.ψ 2 = W.ψ₂
-- Mathlib.Combinatorics.Matroid.Sum
Matroid.Finitary.sigma : ∀ {ι : Type u_1} {α : ι → Type u_2} {M : (i : ι) → Matroid (α i)},
  (∀ (i : ι), (M i).Finitary) → (Matroid.sigma M).Finitary
-- Std.Do.Triple.SpecLemmas
_private.Std.Do.Triple.SpecLemmas.0.Std.Do.PredTrans.pushOption.match_1.eq_1 : ∀ {α : Type u_1} (motive : Option α → Sort u_2) (a : α) (h_1 : (a : α) → motive (some a)) (h_2 : Unit → motive none),
  (match some a with
    | some a => h_1 a
    | none => h_2 ()) =
    h_1 a
-- Mathlib.ModelTheory.Semantics
FirstOrder.Language.BoundedFormula.alls.eq_2 : ∀ {L : FirstOrder.Language} {α : Type u'} (_n : ℕ) (φ : L.BoundedFormula α (_n + 1)), φ.alls = φ.all.alls
-- Mathlib.Topology.Compactness.CountablyCompact
/-- The empty set is countably compact.  -/
isCountablyCompact_empty : ∀ {E : Type u_2} [inst : TopologicalSpace E], IsCountablyCompact ∅
-- Mathlib.Algebra.Homology.ShortComplex.ModuleCat
CategoryTheory.ShortComplex.moduleCat_exact_iff_ker_sub_range : ∀ {R : Type u} [inst : Ring R] (S : CategoryTheory.ShortComplex (ModuleCat R)),
  S.Exact ↔ (ModuleCat.Hom.hom S.g).ker ≤ (ModuleCat.Hom.hom S.f).range
-- Mathlib.CategoryTheory.FiberedCategory.BasedCategory
CategoryTheory.BasedFunctor.comp_id : ∀ {𝒮 : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} 𝒮] {𝒳 : CategoryTheory.BasedCategory 𝒮}
  {𝒴 : CategoryTheory.BasedCategory 𝒮} (F : CategoryTheory.BasedFunctor 𝒳 𝒴),
  F.comp (CategoryTheory.BasedFunctor.id 𝒴) = F
-- Init.Data.UInt.Lemmas
USize.le_iff_toFin_le : ∀ {a b : USize}, a ≤ b ↔ a.toFin ≤ b.toFin
-- Mathlib.Data.Rat.Cast.Order
Rat.preimage_cast_Ici : ∀ {K : Type u_5} [inst : Field K] [inst_1 : LinearOrder K] [IsStrictOrderedRing K] (q : ℚ),
  Rat.cast ⁻¹' Set.Ici ↑q = Set.Ici q
-- Mathlib.Algebra.Order.Module.PositiveLinearMap
PositiveLinearMap.map_nonneg : ∀ {R : Type u_1} {E₁ : Type u_2} {E₂ : Type u_3} [inst : Semiring R] [inst_1 : AddCommMonoid E₁]
  [inst_2 : PartialOrder E₁] [inst_3 : AddCommMonoid E₂] [inst_4 : PartialOrder E₂] [inst_5 : Module R E₁]
  [inst_6 : Module R E₂] (f : E₁ →ₚ[R] E₂) {x : E₁}, 0 ≤ x → 0 ≤ f x
-- Mathlib.Data.Nat.Digits.Defs
Nat.digits_zero_of_eq_zero : ∀ {b : ℕ}, b ≠ 0 → ∀ {L : List ℕ}, Nat.ofDigits b L = 0 → ∀ l ∈ L, l = 0
-- Std.Data.DTreeMap.Internal.Lemmas
Std.DTreeMap.Internal.Impl.getKey!_union_of_contains_eq_false_right : ∀ {α : Type u} {β : α → Type v} {instOrd : Ord α} {m₁ m₂ : Std.DTreeMap.Internal.Impl α β} [inst : Inhabited α]
  [Std.TransOrd α] (h₁ : m₁.WF) (h₂ : m₂.WF) {k : α},
  Std.DTreeMap.Internal.Impl.contains k m₂ = false → (m₁.union m₂ ⋯ ⋯).getKey! k = m₁.getKey! k
-- Mathlib.LinearAlgebra.TensorProduct.Tower
/-- The heterobasic version of `leftComm` coincides with the regular version.  -/
TensorProduct.AlgebraTensorModule.leftComm_eq : ∀ (R : Type uR) {M : Type uM} {P : Type uP} {Q : Type uQ} [inst : CommSemiring R] [inst_1 : AddCommMonoid M]
  [inst_2 : Module R M] [inst_3 : AddCommMonoid P] [inst_4 : AddCommMonoid Q] [inst_5 : Module R Q]
  [inst_6 : Module R P], TensorProduct.AlgebraTensorModule.leftComm R R M P Q = TensorProduct.leftComm R M P Q
-- Std.Async.Signal
/-- Abort signal.

Notes:
- SIGABRT is not catchable if generated by certain runtime functions, such as abort or assertion failure.
- On Windows, watchers can be created for SIGABRT, but they never receive the signal.
 -/
Std.Async.Signal.sigabrt : Std.Async.Signal
-- Mathlib.Algebra.Homology.SpectralObject.Page
CategoryTheory.Abelian.SpectralObject.EIsoH_hom_naturality : ∀ {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 : ι} (f : i ⟶ j) {i' j' : ι} (f' : i' ⟶ j')
  (α : CategoryTheory.ComposableArrows.mk₁ f ⟶ CategoryTheory.ComposableArrows.mk₁ f')
  (β :
    CategoryTheory.ComposableArrows.mk₃ (CategoryTheory.CategoryStruct.id i) f (CategoryTheory.CategoryStruct.id j) ⟶
      CategoryTheory.ComposableArrows.mk₃ (CategoryTheory.CategoryStruct.id i') f'
        (CategoryTheory.CategoryStruct.id j'))
  (n₀ n₁ n₂ : ℤ),
  autoParam (β = CategoryTheory.ComposableArrows.homMk₃ (α.app 0) (α.app 0) (α.app 1) (α.app 1) ⋯ ⋯ ⋯)
      CategoryTheory.Abelian.SpectralObject.EIsoH_hom_naturality._auto_1 →
    ∀ (hn₁ : autoParam (n₀ + 1 = n₁) CategoryTheory.Abelian.SpectralObject.EIsoH_hom_naturality._auto_3)
      (hn₂ : autoParam (n₁ + 1 = n₂) CategoryTheory.Abelian.SpectralObject.EIsoH_hom_naturality._auto_5),
      CategoryTheory.CategoryStruct.comp
          (X.map (CategoryTheory.CategoryStruct.id i) f (CategoryTheory.CategoryStruct.id j)
            (CategoryTheory.CategoryStruct.id i') f' (CategoryTheory.CategoryStruct.id j') β n₀ n₁ n₂ hn₁ hn₂)
          (X.EIsoH f' n₀ n₁ n₂ hn₁ hn₂).hom =
        CategoryTheory.CategoryStruct.comp (X.EIsoH f n₀ n₁ n₂ hn₁ hn₂).hom ((X.H n₁).map α)
-- Mathlib.RingTheory.Ideal.Operations
/-- The product of a finite number of elements in the commutative semiring `R` lies in the
prime ideal `p` if and only if at least one of those elements is in `p`.  -/
Ideal.IsPrime.prod_mem_iff : ∀ {R : Type u} {ι : Type u_1} [inst : CommSemiring R] {s : Finset ι} {x : ι → R} {p : Ideal R} [hp : p.IsPrime],
  ∏ i ∈ s, x i ∈ p ↔ ∃ i ∈ s, x i ∈ p
-- Mathlib.CategoryTheory.Limits.Preserves.Shapes.Images
/-- If a functor preserves limit spans and colimit cospans, then it preserves images.
 -/
CategoryTheory.PreservesImage.iso : {A : Type u₁} →
  {B : Type u₂} →
    [inst : CategoryTheory.Category.{v₁, u₁} A] →
      [inst_1 : CategoryTheory.Category.{v₂, u₂} B] →
        [CategoryTheory.Limits.HasEqualizers A] →
          [inst_3 : CategoryTheory.Limits.HasImages A] →
            [CategoryTheory.StrongEpiCategory B] →
              [inst_5 : CategoryTheory.Limits.HasImages B] →
                (L : CategoryTheory.Functor A B) →
                  [∀ {X Y Z : A} (f : X ⟶ Z) (g : Y ⟶ Z),
                        CategoryTheory.Limits.PreservesLimit (CategoryTheory.Limits.cospan f g) L] →
                    [∀ {X Y Z : A} (f : X ⟶ Y) (g : X ⟶ Z),
                          CategoryTheory.Limits.PreservesColimit (CategoryTheory.Limits.span f g) L] →
                      {X Y : A} →
                        (f : X ⟶ Y) → CategoryTheory.Limits.image (L.map f) ≅ L.obj (CategoryTheory.Limits.image f)
-- Mathlib.Topology.Path
Path.mk.congr_simp : ∀ {X : Type u_1} [inst : TopologicalSpace X] {x y : X} (toContinuousMap toContinuousMap_1 : C(↑unitInterval, X))
  (e_toContinuousMap : toContinuousMap = toContinuousMap_1) (source' : toContinuousMap.toFun 0 = x)
  (target' : toContinuousMap.toFun 1 = y),
  { toContinuousMap := toContinuousMap, source' := source', target' := target' } =
    { toContinuousMap := toContinuousMap_1, source' := ⋯, target' := ⋯ }
-- Mathlib.Topology.Convenient.GeneratedBy
TopologicalSpace.generatedBy_generatedBy : ∀ {ι : Type t} {X : ι → Type u} [inst : (i : ι) → TopologicalSpace (X i)] (Y : Type u_1) [inst_1 : TopologicalSpace Y],
  TopologicalSpace.generatedBy X = TopologicalSpace.generatedBy X
-- Mathlib.LinearAlgebra.QuadraticForm.Signature
QuadraticForm.sigPos_add_sigNeg_add_radical : ∀ {M : Type u_2} [inst : AddCommGroup M] {𝕜 : Type u_4} [inst_1 : Field 𝕜] [inst_2 : LinearOrder 𝕜]
  [inst_3 : Module 𝕜 M] {Q : QuadraticForm 𝕜 M} [IsStrictOrderedRing 𝕜] [FiniteDimensional 𝕜 M],
  sigPos Q + sigNeg Q + Module.finrank 𝕜 ↥(QuadraticMap.radical Q) = Module.finrank 𝕜 M
-- Mathlib.LinearAlgebra.AffineSpace.AffineSubspace.Defs
AffineSubspace.coe_iInf : ∀ {k : Type u_1} {V : Type u_2} {P : Type u_3} [inst : Ring k] [inst_1 : AddCommGroup V] [inst_2 : Module k V]
  [S : AddTorsor V P] {ι : Sort u_4} (s : ι → AffineSubspace k P), ↑(iInf s) = ⋂ i, ↑(s i)
-- Mathlib.Algebra.Homology.HomotopyCategory.MappingCone
CochainComplex.mappingCone.d_snd_v' : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v, u_1} C] [inst_1 : CategoryTheory.Preadditive C]
  {F G : CochainComplex C ℤ} (φ : F ⟶ G) [inst_2 : HomologicalComplex.HasHomotopyCofiber φ] (n : ℤ),
  CategoryTheory.CategoryStruct.comp ((CochainComplex.mappingCone φ).d (n - 1) n)
      ((CochainComplex.mappingCone.snd φ).v n n ⋯) =
    CategoryTheory.CategoryStruct.comp ((↑(CochainComplex.mappingCone.fst φ)).v (n - 1) n ⋯) (φ.f n) +
      CategoryTheory.CategoryStruct.comp ((CochainComplex.mappingCone.snd φ).v (n - 1) (n - 1) ⋯) (G.d (n - 1) n)
-- Mathlib.Order.PiLex
Pi.toLex_update_lt_self_iff : ∀ {ι : Type u_1} {β : ι → Type u_2} [inst : LinearOrder ι] {x : (i : ι) → β i} {i : ι} {a : β i}
  [inst_1 : (i : ι) → PartialOrder (β i)] [WellFoundedLT ι], toLex (Function.update x i a) < toLex x ↔ a < x i
-- Lean.Meta.Closure
Lean.Meta.Closure.MkValueTypeClosureResult.mk.inj : ∀ {levelParams : Array Lean.Name} {type value : Lean.Expr} {levelArgs : Array Lean.Level} {exprArgs : Array Lean.Expr}
  {levelParams_1 : Array Lean.Name} {type_1 value_1 : Lean.Expr} {levelArgs_1 : Array Lean.Level}
  {exprArgs_1 : Array Lean.Expr},
  { levelParams := levelParams, type := type, value := value, levelArgs := levelArgs, exprArgs := exprArgs } =
      { levelParams := levelParams_1, type := type_1, value := value_1, levelArgs := levelArgs_1,
        exprArgs := exprArgs_1 } →
    levelParams = levelParams_1 ∧ type = type_1 ∧ value = value_1 ∧ levelArgs = levelArgs_1 ∧ exprArgs = exprArgs_1
-- Mathlib.RingTheory.MatrixPolynomialAlgebra
matPolyEquiv_diagonal_X : ∀ {R : Type u_1} [inst : CommSemiring R] {n : Type w} [inst_1 : DecidableEq n] [inst_2 : Fintype n],
  matPolyEquiv (Matrix.diagonal fun x => Polynomial.X) = Polynomial.X
-- Mathlib.Algebra.Homology.HomotopyCategory.ShortExact
CochainComplex.mappingCone.map_descShortComplex : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Abelian C]
  (S₁ S₂ : CategoryTheory.ShortComplex (CochainComplex C ℤ)) (f : S₁ ⟶ S₂),
  CategoryTheory.CategoryStruct.comp (CochainComplex.mappingCone.map S₁.f S₂.f f.τ₁ f.τ₂ ⋯)
      (CochainComplex.mappingCone.descShortComplex S₂) =
    CategoryTheory.CategoryStruct.comp (CochainComplex.mappingCone.descShortComplex S₁) f.τ₃
-- Mathlib.GroupTheory.Finiteness
Submonoid.fg_iff_add_fg : ∀ {M : Type u_1} [inst : Monoid M] (P : Submonoid M), P.FG ↔ (Submonoid.toAddSubmonoid P).FG
-- Init.Data.Nat.Bitwise.Lemmas
Nat.shiftRight_or_distrib : ∀ {i a b : ℕ}, (a ||| b) >>> i = a >>> i ||| b >>> i
-- Mathlib.MeasureTheory.Constructions.BorelSpace.Metrizable
/-- If the indicator functions of measurable sets `Aᵢ` converge to the indicator function of
a set `A` along a nontrivial countably generated filter, then `A` is also measurable.  -/
measurableSet_of_tendsto_indicator : ∀ {α : Type u_3} [inst : MeasurableSpace α] {A : Set α} {ι : Type u_4} (L : Filter ι) [L.IsCountablyGenerated]
  {As : ι → Set α} [L.NeBot],
  (∀ (i : ι), MeasurableSet (As i)) → (∀ (x : α), ∀ᶠ (i : ι) in L, x ∈ As i ↔ x ∈ A) → MeasurableSet A
-- Mathlib.Logic.Equiv.Defs
Equiv.equivCongr_trans : ∀ {α : Sort u} {β : Sort v} {γ : Sort w} {δ : Sort u_1} {ε : Sort u_2} {ζ : Sort u_3} (ab : α ≃ β) (de : δ ≃ ε)
  (bc : β ≃ γ) (ef : ε ≃ ζ), (ab.equivCongr de).trans (bc.equivCongr ef) = (ab.trans bc).equivCongr (de.trans ef)
-- Mathlib.CategoryTheory.Generator.Basic
CategoryTheory.HasCoseparator.mk : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C],
  (∃ G, CategoryTheory.IsCoseparator G) → CategoryTheory.HasCoseparator C
-- Mathlib.Algebra.Polynomial.Div
/-- The largest power of `X - C a` which divides `p`.  -/
Polynomial.rootMultiplicity : {R : Type u} → [inst : Ring R] → R → Polynomial R → ℕ
-- Mathlib.RingTheory.Ideal.Colon
Submodule.colon_finsetInf : ∀ {R : Type u_1} {M : Type u_2} [inst : Semiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M] {S : Set M}
  {ι : Type u_3} (s : Finset ι) (f : ι → Submodule R M), (s.inf f).colon S = s.inf fun i => (f i).colon S
-- Mathlib.Algebra.Group.Units.Basic
isAddUnit_of_subsingleton : ∀ {M : Type u_1} [inst : AddMonoid M] [Subsingleton M] (a : M), IsAddUnit a
-- Mathlib.Algebra.Group.Subgroup.Actions
Subgroup.instMulAction.eq_1 : ∀ {G : Type u_1} {α : Type u_2} [inst : Group G] [inst_1 : MulAction G α] {S : Subgroup G},
  Subgroup.instMulAction =
    { toSemigroupAction := (Submonoid.instMulActionSubtypeMem S).toSemigroupAction, one_smul := ⋯ }
-- Mathlib.Analysis.Normed.Operator.Mul
/-- This is a mixin class for non-unital normed algebras which states that the left-regular
representation of the algebra on itself is isometric. Every unital normed algebra with `‖1‖ = 1` is
a regular normed algebra (see `NormedAlgebra.instRegularNormedAlgebra`). In addition, so is every
C⋆-algebra, non-unital included (see `CStarRing.instRegularNormedAlgebra`), but there are yet other
examples. Any algebra with an approximate identity (e.g., `L¹`) is also regular.

This is a useful class because it gives rise to a nice norm on the unitization; in particular it is
a C⋆-norm when the norm on `A` is a C⋆-norm.  -/
RegularNormedAlgebra : (𝕜 : Type u_1) →
  [inst : NontriviallyNormedField 𝕜] →
    (R : Type u_3) →
      [inst_1 : NonUnitalSeminormedRing R] →
        [inst_2 : NormedSpace 𝕜 R] → [IsScalarTower 𝕜 R R] → [SMulCommClass 𝕜 R R] → Prop
-- Mathlib.Algebra.Homology.DerivedCategory.Ext.Basic
/-- An Ext-group in an abelian category `C`, defined as a `Type w` when `[HasExt.{w} C]`.  -/
CategoryTheory.Abelian.Ext : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    [inst_1 : CategoryTheory.Abelian C] → [CategoryTheory.HasExt C] → C → C → ℕ → Type w
-- Std.Time.Internal.UnitVal
Std.Time.Internal.UnitVal.instLE : {α : ℚ} → LE (Std.Time.Internal.UnitVal α)
-- Mathlib.CategoryTheory.Monad.Basic
/-- An isomorphism of comonads gives a natural isomorphism of the underlying functors.
 -/
CategoryTheory.ComonadIso.toNatIso : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] → {M N : CategoryTheory.Comonad C} → (M ≅ N) → (M.toFunctor ≅ N.toFunctor)
-- Mathlib.Data.Rat.Lemmas
Rat.add_intCast_den : ∀ (q : ℚ) (n : ℤ), (q + ↑n).den = q.den
-- Mathlib.CategoryTheory.Sites.Coverage
CategoryTheory.Coverage.instPartialOrder : {C : Type u_1} → [inst : CategoryTheory.Category.{v_1, u_1} C] → PartialOrder (CategoryTheory.Coverage C)
-- Mathlib.MeasureTheory.Function.L1Space.Integrable
MeasureTheory.integrable_right_of_integrable_add_of_nonneg : ∀ {α : Type u_1} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} {f g : α → ℝ},
  MeasureTheory.AEStronglyMeasurable f μ →
    0 ≤ᵐ[μ] f → 0 ≤ᵐ[μ] g → MeasureTheory.Integrable (f + g) μ → MeasureTheory.Integrable g μ
-- Std.Data.DTreeMap.Internal.Model
_private.Std.Data.DTreeMap.Internal.Model.0.Std.DTreeMap.Internal.Impl.get.match_1.eq_1 : ∀ {α : Type u_1} {β : α → Type u_2} [inst : Ord α] (k : α)
  (motive : (t : Std.DTreeMap.Internal.Impl α β) → k ∈ t → Sort u_3) (size : ℕ) (k' : α) (v' : β k')
  (l r : Std.DTreeMap.Internal.Impl α β) (hlk : k ∈ Std.DTreeMap.Internal.Impl.inner size k' v' l r)
  (h_1 :
    (size : ℕ) →
      (k' : α) →
        (v' : β k') →
          (l r : Std.DTreeMap.Internal.Impl α β) →
            (hlk : k ∈ Std.DTreeMap.Internal.Impl.inner size k' v' l r) →
              motive (Std.DTreeMap.Internal.Impl.inner size k' v' l r) hlk),
  (match Std.DTreeMap.Internal.Impl.inner size k' v' l r, hlk with
    | Std.DTreeMap.Internal.Impl.inner size k' v' l r, hlk => h_1 size k' v' l r hlk) =
    h_1 size k' v' l r hlk
-- Mathlib.RingTheory.DedekindDomain.Different
Submodule.traceDual.congr_simp : ∀ (A : Type u_1) (K : Type u_2) {L : Type u} {B : Type u_3} [inst : CommRing A] [inst_1 : Field K] [inst_2 : CommRing B]
  [inst_3 : Field L] [inst_4 : Algebra A K] [inst_5 : Algebra B L] [inst_6 : Algebra A B] [inst_7 : Algebra K L]
  [inst_8 : Algebra A L] [inst_9 : IsScalarTower A K L] [inst_10 : IsScalarTower A B L] (I I_1 : Submodule B L),
  I = I_1 → Submodule.traceDual A K I = Submodule.traceDual A K I_1
-- Mathlib.RingTheory.AdjoinRoot
AdjoinRoot.lift.congr_simp : ∀ {R : Type u_1} {S : Type u_2} [inst : CommRing R] {f : Polynomial R} [inst_1 : CommRing S] (i i_1 : R →+* S)
  (e_i : i = i_1) (x x_1 : S) (e_x : x = x_1) (h : Polynomial.eval₂ i x f = 0),
  AdjoinRoot.lift i x h = AdjoinRoot.lift i_1 x_1 ⋯
-- Mathlib.Algebra.Order.Interval.Finset.Basic
Finset.image_add_right_Ioc : ∀ {α : Type u_2} [inst : AddCommMonoid α] [inst_1 : PartialOrder α] [IsOrderedCancelAddMonoid α] [ExistsAddOfLE α]
  [inst_4 : LocallyFiniteOrder α] [inst_5 : DecidableEq α] (a b c : α),
  Finset.image (fun x => x + c) (Finset.Ioc a b) = Finset.Ioc (a + c) (b + c)
-- Mathlib.SetTheory.Ordinal.Basic
Cardinal.card_typein_lt : ∀ {α : Type u} {r : α → α → Prop} [inst : IsWellOrder α r] (x : α),
  (Cardinal.mk α).ord = Ordinal.type r → ((Ordinal.typein r).toRelEmbedding x).card < Cardinal.mk α
-- Mathlib.Analysis.Calculus.FDeriv.Congr
Filter.EventuallyEq.hasStrictFDerivAt_iff : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : AddCommGroup E] [inst_2 : Module 𝕜 E]
  [inst_3 : TopologicalSpace E] {F : Type u_3} [inst_4 : AddCommGroup F] [inst_5 : Module 𝕜 F]
  [inst_6 : TopologicalSpace F] {f₀ f₁ : E → F} {f₀' f₁' : E →L[𝕜] F} {x : E},
  f₀ =ᶠ[nhds x] f₁ → (∀ (y : E), f₀' y = f₁' y) → (HasStrictFDerivAt f₀ f₀' x ↔ HasStrictFDerivAt f₁ f₁' x)
-- Mathlib.Order.Interval.Finset.Basic
/-- **Alias** of the reverse direction of `Finset.Ico_eq_empty_iff`. -/
Finset.Ico_eq_empty : ∀ {α : Type u_2} {a b : α} [inst : Preorder α] [inst_1 : LocallyFiniteOrder α], ¬a < b → Finset.Ico a b = ∅
-- Mathlib.CategoryTheory.Localization.CalculusOfFractions
/-- A left fraction from `X : C` to `Y : C` for `W : MorphismProperty C` consists of the
datum of an object `Y' : C` and maps `f : X ⟶ Y'` and `s : Y ⟶ Y'` such that `W s`.  -/
CategoryTheory.MorphismProperty.LeftFraction : {C : Type u_1} →
  [inst : CategoryTheory.Category.{v_1, u_1} C] → CategoryTheory.MorphismProperty C → C → C → Type (max u_1 v_1)
-- Mathlib.Algebra.Notation.Pi.Basic
/-- The function supported at `i`, with value `x` there, and `1` elsewhere.  -/
Pi.mulSingle : {ι : Type u_1} → {M : ι → Type u_6} → [(i : ι) → One (M i)] → [DecidableEq ι] → (i : ι) → M i → (j : ι) → M j
-- Mathlib.CategoryTheory.Sites.SheafCohomology.MayerVietoris
CategoryTheory.GrothendieckTopology.MayerVietorisSquare.δ_toBiprod : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {J : CategoryTheory.GrothendieckTopology C}
  [inst_1 : CategoryTheory.HasWeakSheafify J (Type v)] [inst_2 : CategoryTheory.HasSheafify J AddCommGrpCat]
  [inst_3 : CategoryTheory.HasExt (CategoryTheory.Sheaf J AddCommGrpCat)] (S : J.MayerVietorisSquare)
  (F : CategoryTheory.Sheaf J AddCommGrpCat) (n₀ n₁ : ℕ) (h : n₀ + 1 = n₁),
  CategoryTheory.CategoryStruct.comp (S.δ F n₀ n₁ h) (S.toBiprod F n₁) = 0
-- Mathlib.FieldTheory.PolynomialGaloisGroup
Polynomial.instFintypeGal : {F : Type u_1} → [inst : Field F] → (p : Polynomial F) → Fintype p.Gal
-- Mathlib.Algebra.Homology.HomologicalComplex
/-- The isomorphism from `(mk X₀ X₁ X₂ d₀ d₁ s succ).X (n + 3)` that is given by
the inductive construction.  -/
ChainComplex.mkXIso : {V : Type u} →
  [inst : CategoryTheory.Category.{v, u} V] →
    [inst_1 : CategoryTheory.Limits.HasZeroMorphisms V] →
      (X₀ X₁ X₂ : V) →
        (d₀ : X₁ ⟶ X₀) →
          (d₁ : X₂ ⟶ X₁) →
            (s : CategoryTheory.CategoryStruct.comp d₁ d₀ = 0) →
              (succ :
                  (S : CategoryTheory.ShortComplex V) →
                    (X₃ : V) ×' (d₂ : X₃ ⟶ S.X₁) ×' CategoryTheory.CategoryStruct.comp d₂ S.f = 0) →
                (n : ℕ) →
                  (ChainComplex.mk X₀ X₁ X₂ d₀ d₁ s succ).X (n + 3) ≅
                    (succ
                        { X₁ := (ChainComplex.mk X₀ X₁ X₂ d₀ d₁ s succ).X (n + 2),
                          X₂ := (ChainComplex.mk X₀ X₁ X₂ d₀ d₁ s succ).X (n + 1),
                          X₃ := (ChainComplex.mk X₀ X₁ X₂ d₀ d₁ s succ).X n,
                          f := (ChainComplex.mk X₀ X₁ X₂ d₀ d₁ s succ).d (n + 2) (n + 1),
                          g := (ChainComplex.mk X₀ X₁ X₂ d₀ d₁ s succ).d (n + 1) n, zero := ⋯ }).fst
-- Mathlib.Data.Set.Pairwise.Basic
Set.Pairwise.inter_left : ∀ {α : Type u_1} {r : α → α → Prop} {s : Set α}, s.Pairwise r → ∀ (t : Set α), (s ∩ t).Pairwise r
-- Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Unique
StarAlgHom.realContinuousMapOfNNReal_apply : ∀ {X : Type u_1} [inst : TopologicalSpace X] {A : Type u_2} [inst_1 : Ring A] [inst_2 : StarRing A]
  [inst_3 : Algebra ℝ A] (φ : C(X, NNReal) →⋆ₐ[NNReal] A) (f : C(X, ℝ)),
  φ.realContinuousMapOfNNReal f = φ f.toNNReal - φ (-f).toNNReal
-- Mathlib.Logic.Encodable.Basic
Directed.sequence.eq_2 : ∀ {α : Type u_1} {β : Type u_2} [inst : Encodable α] [inst_1 : Inhabited α] {r : β → β → Prop} (f : α → β)
  (hf : Directed r f) (n : ℕ),
  Directed.sequence f hf n.succ =
    match Encodable.decode n with
    | none => Classical.choose ⋯
    | some a => Classical.choose ⋯
-- Mathlib.Data.Set.Subsingleton
Set.univ_eq_true_false : Set.univ = {True, False}
-- Std.Time.Zoned.ZoneRules
Std.Time.TimeZone.Transition.mk.inj : ∀ {time : Std.Time.Second.Offset} {localTimeType : Std.Time.TimeZone.LocalTimeType} {time_1 : Std.Time.Second.Offset}
  {localTimeType_1 : Std.Time.TimeZone.LocalTimeType},
  { time := time, localTimeType := localTimeType } = { time := time_1, localTimeType := localTimeType_1 } →
    time = time_1 ∧ localTimeType = localTimeType_1
-- Std.Tactic.BVDecide.Bitblast.BVExpr.Circuit.Impl.Operations.Udiv
Std.Tactic.BVDecide.BVExpr.bitblast.blastUdiv.go : {α : Type} →
  [inst : Hashable α] →
    [inst_1 : DecidableEq α] →
      {w : ℕ} →
        (aig : Std.Sat.AIG α) →
          ℕ →
            aig.RefVec w →
              aig.RefVec w →
                ℕ →
                  ℕ → aig.RefVec w → aig.RefVec w → Std.Tactic.BVDecide.BVExpr.bitblast.blastUdiv.BlastUdivOutput aig w
-- Mathlib.Topology.Path
/-- Given a family of paths, one in each Xᵢ, we take their pointwise product to get a path in
Π i, Xᵢ.  -/
Path.pi : {ι : Type u_3} →
  {χ : ι → Type u_4} →
    [inst : (i : ι) → TopologicalSpace (χ i)] → {as bs : (i : ι) → χ i} → ((i : ι) → Path (as i) (bs i)) → Path as bs
-- Mathlib.LinearAlgebra.BilinearMap
LinearMap.domRestrict₂_apply : ∀ {R : Type u_1} {R₂ : Type u_2} {S : Type u_3} {S₂ : Type u_4} [inst : Semiring R] [inst_1 : Semiring R₂]
  [inst_2 : Semiring S] [inst_3 : Semiring S₂] {M : Type u_5} {N : Type u_7} {P : Type u_9} [inst_4 : AddCommMonoid M]
  [inst_5 : AddCommMonoid N] [inst_6 : AddCommMonoid P] [inst_7 : Module R M] [inst_8 : Module S N]
  [inst_9 : Module R₂ P] [inst_10 : Module S₂ P] [inst_11 : SMulCommClass S₂ R₂ P] {ρ₁₂ : R →+* R₂} {σ₁₂ : S →+* S₂}
  (f : M →ₛₗ[ρ₁₂] N →ₛₗ[σ₁₂] P) (q : Submodule S N) (x : M) (y : ↥q), ((f.domRestrict₂ q) x) y = (f x) ↑y
-- Lean.Setup
/-- The name of the module.  -/
Lean.ModuleSetup.name : Lean.ModuleSetup → Lean.Name
-- Mathlib.Algebra.Homology.HomologicalComplex
HomologicalComplex.Hom.isoApp_inv : ∀ {ι : Type u_1} {V : Type u} [inst : CategoryTheory.Category.{v, u} V]
  [inst_1 : CategoryTheory.Limits.HasZeroMorphisms V] {c : ComplexShape ι} {C₁ C₂ : HomologicalComplex V c}
  (f : C₁ ≅ C₂) (i : ι), (HomologicalComplex.Hom.isoApp f i).inv = f.inv.f i
-- Mathlib.Topology.LocallyConstant.Basic
LocallyConstant.ext_iff : ∀ {X : Type u_1} {Y : Type u_2} [inst : TopologicalSpace X] {f g : LocallyConstant X Y}, f = g ↔ ∀ (x : X), f x = g x