mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Tactic.Translate.Reorder
_private.Mathlib.Tactic.Translate.Reorder.0.Array.map_unattach.match_1.splitter : {α : Type u_1} →
  {P : α → Prop} → (motive : Subtype P → Sort u_2) → (x : Subtype P) → ((x : α) → (h : P x) → motive ⟨x, h⟩) → motive x
-- Mathlib.CategoryTheory.Limits.Shapes.Images
CategoryTheory.Limits.MonoFactorisation.compMono_m : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {X Y : C} {f : X ⟶ Y}
  (F : CategoryTheory.Limits.MonoFactorisation f) {Y' : C} (g : Y ⟶ Y') [inst_1 : CategoryTheory.Mono g],
  (F.compMono g).m = CategoryTheory.CategoryStruct.comp F.m g
-- Lean.Elab.MutualDef
_private.Lean.Elab.MutualDef.0.Lean.Elab.Term.MutualClosure.mkLetRecClosureFor : Lean.Elab.Term.LetRecToLift → Array Lean.FVarId → Lean.Elab.TermElabM Lean.Elab.Term.MutualClosure.LetRecClosure
-- Mathlib.Analysis.Calculus.ContDiff.Defs
_private.Mathlib.Analysis.Calculus.ContDiff.Defs.0.ContDiffWithinAt.match_1.eq_2 : ∀ (motive : WithTop ℕ∞ → Sort u_1) (n : ℕ∞) (h_1 : Unit → motive none) (h_2 : (n : ℕ∞) → motive (some n)),
  (match some n with
    | none => h_1 ()
    | some n => h_2 n) =
    h_2 n
-- Mathlib.Data.List.TakeDrop
List.tail_drop_eq_drop_tail : ∀ {α : Type u} (l : List α) (n : ℕ), (List.drop n l).tail = List.drop n l.tail
-- Std.Data.HashSet.RawLemmas
Std.HashSet.Raw.mem_diff_iff : ∀ {α : Type u} [inst : BEq α] [inst_1 : Hashable α] {m₁ m₂ : Std.HashSet.Raw α} [EquivBEq α] [LawfulHashable α],
  m₁.WF → m₂.WF → ∀ {k : α}, k ∈ m₁ \ m₂ ↔ k ∈ m₁ ∧ k ∉ m₂
-- Mathlib.Combinatorics.SimpleGraph.Walk.Decomp
SimpleGraph.Walk.support_dropUntil_suffix_support : ∀ {V : Type u} {G : SimpleGraph V} {v w u : V} [inst : DecidableEq V] (p : G.Walk v w) (h : u ∈ p.support),
  (p.dropUntil u h).support <:+ p.support
-- Lean.Meta.Tactic.Grind.Arith.Linear.Types
Lean.Meta.Grind.Arith.Linear.RingEqCnstr.mk : Lean.Grind.CommRing.Poly → Lean.Meta.Grind.Arith.Linear.RingEqCnstrProof → Lean.Meta.Grind.Arith.Linear.RingEqCnstr
-- Mathlib.CategoryTheory.Quotient
CategoryTheory.Congruence.mk : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] {r : HomRel C}
  [toIsStableUnderPrecomp : CategoryTheory.HomRel.IsStableUnderPrecomp r]
  [toIsStableUnderPostcomp : CategoryTheory.HomRel.IsStableUnderPostcomp r],
  (∀ {X Y : C}, Equivalence r) → CategoryTheory.Congruence r
-- Mathlib.Analysis.Normed.Group.Real
Real.enorm_ofReal_of_nonneg : ∀ {a : ℝ}, 0 ≤ a → ‖ENNReal.ofReal a‖ₑ = ‖a‖ₑ
-- Mathlib.Algebra.Homology.ShortComplex.SnakeLemma
/-- When `L₀₂` and `L₃₂` are trivial, `δ` defines an isomorphism `L₀₃ ≅ L₃₁`.  -/
CategoryTheory.ShortComplex.SnakeInput.δIso : {C : Type u_1} →
  [inst : CategoryTheory.Category.{v_1, u_1} C] →
    [inst_1 : CategoryTheory.Abelian C] →
      (S : CategoryTheory.ShortComplex.SnakeInput C) →
        CategoryTheory.Limits.IsZero S.L₀.X₂ → CategoryTheory.Limits.IsZero S.L₃.X₂ → (S.L₀.X₃ ≅ S.L₃.X₁)
-- Mathlib.Order.Lattice
ULift.instSemilatticeSup.eq_1 : ∀ {α : Type u} [inst : SemilatticeSup α],
  ULift.instSemilatticeSup = Function.Injective.semilatticeSup ULift.down ⋯ ⋯ ⋯ ⋯
-- Mathlib.Analysis.Polynomial.Basic
Polynomial.isLittleO_atBot_of_degree_lt : ∀ {𝕜 : Type u_1} [inst : NormedField 𝕜] [inst_1 : LinearOrder 𝕜] [IsStrictOrderedRing 𝕜] (P Q : Polynomial 𝕜)
  [OrderTopology 𝕜], P.degree < Q.degree → (fun x => Polynomial.eval x P) =o[Filter.atBot] fun x => Polynomial.eval x Q
-- Mathlib.Probability.Independence.InfinitePi
MeasureTheory.Measure.map_infinitePi_infinitePi_of_inj : ∀ {ι : Type u_1} {α : Type u_4} {Ω : ι → Type u_5} {mΩ : (i : ι) → MeasurableSpace (Ω i)}
  {P : (i : ι) → MeasureTheory.Measure (Ω i)} [∀ (i : ι), MeasureTheory.IsProbabilityMeasure (P i)] {f : α → ι},
  Function.Injective f →
    MeasureTheory.Measure.map (fun ω i => ω (f i)) (MeasureTheory.Measure.infinitePi P) =
      MeasureTheory.Measure.infinitePi fun i => P (f i)
-- Lean.Meta.Match.Basic
Lean.Meta.Match.Problem : Type
-- Init.Data.Nat.Div.Lemmas
/-- If `(a + b) % c = c - 1`, then `a % c + b % c < c`, because `a % c + b % c` can not reach `2*c - 1`.  -/
Nat.mod_add_mod_lt_of_add_mod_eq_sub_one : ∀ {c a b : ℕ}, 0 < c → (a + b) % c = c - 1 → a % c + b % c < c
-- Mathlib.RingTheory.Extension.Cotangent.BaseChange
/-- If `T` is flat over `R`, there is a `T`-linear isomorphism
`T ⊗[R] P.Cotangent ≃ₗ[T] (P.baseChange).Cotangent`.  -/
Algebra.Extension.tensorCotangentOfFlat : {R : Type u_1} →
  {S : Type u_2} →
    [inst : CommRing R] →
      [inst_1 : CommRing S] →
        [inst_2 : Algebra R S] →
          (P : Algebra.Extension R S) →
            (T : Type u_3) →
              [inst_3 : CommRing T] →
                [inst_4 : Algebra R T] → [Module.Flat R T] → TensorProduct R T P.Cotangent ≃ₗ[T] P.baseChange.Cotangent
-- Mathlib.Order.Defs.PartialOrder
lt_of_le_of_lt' : ∀ {α : Type u_1} [inst : Preorder α] {a b c : α}, b ≤ a → c < b → c < a
-- Std.Data.DHashMap.Lemmas
Std.DHashMap.Equiv.getKeyD_eq : ∀ {α : Type u} {β : α → Type v} {x : BEq α} {x_1 : Hashable α} {m₁ m₂ : Std.DHashMap α β} [EquivBEq α]
  [LawfulHashable α] {k fallback : α}, m₁.Equiv m₂ → m₁.getKeyD k fallback = m₂.getKeyD k fallback
-- Mathlib.Topology.OpenPartialHomeomorph.Defs
OpenPartialHomeomorph.invOn : ∀ {X : Type u_1} {Y : Type u_3} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y]
  (e : OpenPartialHomeomorph X Y), Set.InvOn (↑e.symm) (↑e) e.source e.target
-- Mathlib.CategoryTheory.ShrinkYoneda
CategoryTheory.shrinkYoneda.congr_simp : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.LocallySmall.{w, v, u} C],
  CategoryTheory.shrinkYoneda.{w, v, u} = CategoryTheory.shrinkYoneda.{w, v, u}
-- Mathlib.Data.Finset.Max
Finset.isGLB_iff_isLeast : ∀ {α : Type u_2} [inst : LinearOrder α] (i : α) (s : Finset α), s.Nonempty → (IsGLB (↑s) i ↔ IsLeast (↑s) i)
-- Mathlib.Analysis.SpecialFunctions.ImproperIntegrals
integrableOn_Ioi_deriv_norm_ofReal_cpow : ∀ {s : ℂ} {t : ℝ},
  0 < t → s.re ≤ 0 → MeasureTheory.IntegrableOn (deriv fun x => ‖↑x ^ s‖) (Set.Ioi t) MeasureTheory.volume
-- Mathlib.Algebra.Algebra.Operations
Submodule.map_unop_mul : ∀ {R : Type u} [inst : CommSemiring R] {A : Type v} [inst_1 : Semiring A] [inst_2 : Algebra R A]
  (M N : Submodule R Aᵐᵒᵖ),
  Submodule.map (↑(MulOpposite.opLinearEquiv R).symm) (M * N) =
    Submodule.map (↑(MulOpposite.opLinearEquiv R).symm) N * Submodule.map (↑(MulOpposite.opLinearEquiv R).symm) M
-- Std.Data.Internal.List.Associative
Std.Internal.List.Const.getValue!_alterKey : ∀ {α : Type u} [inst : BEq α] {β : Type v} [EquivBEq α] {k k' : α} [inst_2 : Inhabited β] {f : Option β → Option β}
  (l : List ((_ : α) × β)),
  Std.Internal.List.DistinctKeys l →
    Std.Internal.List.getValue! k' (Std.Internal.List.Const.alterKey k f l) =
      if (k == k') = true then (f (Std.Internal.List.getValue? k l)).get! else Std.Internal.List.getValue! k' l
-- Mathlib.Analysis.Calculus.LineDeriv.Basic
HasLineDerivWithinAt.congr_of_eventuallyEq : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {F : Type u_2} [inst_1 : NormedAddCommGroup F]
  [inst_2 : NormedSpace 𝕜 F] {E : Type u_3} [inst_3 : NormedAddCommGroup E] [inst_4 : NormedSpace 𝕜 E] {f f₁ : E → F}
  {f' : F} {s : Set E} {x v : E},
  HasLineDerivWithinAt 𝕜 f f' s x v → f₁ =ᶠ[nhdsWithin x s] f → f₁ x = f x → HasLineDerivWithinAt 𝕜 f₁ f' s x v
-- Mathlib.Algebra.Order.Floor.Ring
Int.natCast_ceil_eq_ceil : ∀ {R : Type u_2} [inst : Ring R] [inst_1 : LinearOrder R] [inst_2 : FloorRing R] {a : R}, 0 ≤ a → ↑⌈a⌉₊ = ⌈a⌉
-- Mathlib.CategoryTheory.Monoidal.Closed.Basic
CategoryTheory.MonoidalClosed.internalHomAdjunction₂_adj : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.MonoidalCategory C]
  [inst_2 : CategoryTheory.MonoidalClosed C] (x : C),
  CategoryTheory.MonoidalClosed.internalHomAdjunction₂.adj x = CategoryTheory.ihom.adjunction x
-- Mathlib.Algebra.Algebra.Defs
Algebra.mk : {R : Type u} →
  {A : Type v} →
    [inst : CommSemiring R] →
      [inst_1 : Semiring A] →
        [toSMul : SMul R A] →
          (algebraMap : R →+* A) →
            (∀ (r : R) (x : A), algebraMap r * x = x * algebraMap r) →
              (∀ (r : R) (x : A), r • x = algebraMap r * x) → Algebra R A
-- Mathlib.RingTheory.Polynomial.UniqueFactorization
Polynomial.uniqueFactorizationMonoid : ∀ {D : Type u} [inst : CommRing D] [UniqueFactorizationMonoid D], UniqueFactorizationMonoid (Polynomial D)
-- Mathlib.AlgebraicGeometry.EllipticCurve.Projective.Basic
WeierstrassCurve.Projective.map_polynomialY : ∀ {R : Type r} [inst : CommRing R] (W' : WeierstrassCurve.Projective R) {S : Type s} [inst_1 : CommRing S]
  (f : R →+* S), (W'.map f).polynomialY = (MvPolynomial.map f) W'.polynomialY
-- Mathlib.Algebra.Group.Subsemigroup.Membership
AddSubsemigroup.instIsAddCommutative_iSup : ∀ {M : Type u_2} [inst : Add M] {ι : Type u_3} [inst_1 : Preorder ι] [IsDirectedOrder ι] (S : ι →o AddSubsemigroup M)
  [hS : ∀ (i : ι), IsAddCommutative ↥(S i)], IsAddCommutative ↥(⨆ i, S i)
-- Mathlib.LinearAlgebra.PiTensorProduct.Basic
PiTensorProduct.map_update_smul : ∀ {ι : Type u_1} {R : Type u_4} [inst : CommSemiring R] {s : ι → Type u_7} [inst_1 : (i : ι) → AddCommMonoid (s i)]
  [inst_2 : (i : ι) → Module R (s i)] {t : ι → Type u_11} [inst_3 : (i : ι) → AddCommMonoid (t i)]
  [inst_4 : (i : ι) → Module R (t i)] (f : (i : ι) → s i →ₗ[R] t i) [inst_5 : DecidableEq ι] (i : ι) (c : R)
  (u : s i →ₗ[R] t i),
  PiTensorProduct.map (Function.update f i (c • u)) = c • PiTensorProduct.map (Function.update f i u)
-- Mathlib.Topology.Neighborhoods
IsOpen.inter_closure : ∀ {X : Type u} [inst : TopologicalSpace X] {s t : Set X}, IsOpen s → s ∩ closure t ⊆ closure (s ∩ t)
-- Mathlib.Algebra.BigOperators.Group.Multiset.Defs
Multiset.sum_eq_foldl : ∀ {M : Type u_3} [inst : AddCommMonoid M] (s : Multiset M), s.sum = Multiset.foldl (fun x1 x2 => x1 + x2) 0 s
-- Init.Data.Rat.Lemmas
Rat.le_refl : ∀ {a : ℚ}, a ≤ a
-- Lean.Meta.Tactic.Grind.EMatchTheorem
_private.Lean.Meta.Tactic.Grind.EMatchTheorem.0.Lean.Meta.Grind.NormalizePattern.normalizePattern : Lean.Expr → Lean.Meta.Grind.NormalizePattern.M✝ Lean.Expr
-- Mathlib.LinearAlgebra.TensorPower.Basic
_private.Mathlib.LinearAlgebra.TensorPower.Basic.0.TensorPower.«term_ₜ*_» : Lean.TrailingParserDescr
-- Mathlib.RingTheory.MatrixAlgebra
MatrixEquivTensor.toFunAlgHom_apply : ∀ (n : Type u_3) (R : Type u_5) (A : Type u_7) [inst : CommSemiring R] [inst_1 : Semiring A] [inst_2 : Algebra R A]
  [inst_3 : DecidableEq n] [inst_4 : Fintype n] (a : A) (m : Matrix n n R),
  (MatrixEquivTensor.toFunAlgHom n R A) (a ⊗ₜ[R] m) = a • m.map ⇑(algebraMap R A)
-- Lean.Data.Lsp.LanguageFeatures
Lean.Lsp.SignatureHelp.activeParameter? : Lean.Lsp.SignatureHelp → Option ℕ
-- Mathlib.Algebra.SkewMonoidAlgebra.Basic
/-- `single 1` as a `RingHom`  -/
SkewMonoidAlgebra.singleOneRingHom : {k : Type u_1} →
  {G : Type u_2} →
    [inst : Semiring k] → [inst_1 : Monoid G] → [inst_2 : MulSemiringAction G k] → k →+* SkewMonoidAlgebra k G
-- Std.Data.ExtDHashMap.Lemmas
Std.ExtDHashMap.Const.getD_eq_fallback_of_contains_eq_false : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} {β : Type v} {m : Std.ExtDHashMap α fun x => β} [inst : EquivBEq α]
  [inst_1 : LawfulHashable α] {a : α} {fallback : β},
  m.contains a = false → Std.ExtDHashMap.Const.getD m a fallback = fallback
-- Lean.Linter.Deprecated
Lean.Linter.DeprecationEntry.mk.sizeOf_spec : ∀ (newName? : Option Lean.Name) (text? since? : Option String),
  sizeOf { newName? := newName?, text? := text?, since? := since? } = 1 + sizeOf newName? + sizeOf text? + sizeOf since?
-- Mathlib.Algebra.Order.Disjointed
Monotone.disjointed_add_one : ∀ {α : Type u_1} {ι : Type u_2} [inst : GeneralizedBooleanAlgebra α] [inst_1 : LinearOrder ι]
  [inst_2 : LocallyFiniteOrderBot ι] [inst_3 : Add ι] [inst_4 : One ι] [SuccAddOrder ι] [NoMaxOrder ι] {f : ι → α},
  Monotone f → ∀ (i : ι), disjointed f (i + 1) = f (i + 1) \ f i
-- Std.Data.DHashMap.Internal.AssocList.Iterator
_private.Std.Data.DHashMap.Internal.AssocList.Iterator.0.Std.DHashMap.Internal.AssocList.instIteratorAssocListIteratorIdSigma.match_3.splitter : {α : Type u_2} →
  {β : α → Type u_1} →
    (motive : Std.IterM Id ((a : α) × β a) → Sort u_3) →
      (it : Std.IterM Id ((a : α) × β a)) →
        (Unit → motive { internalState := { l := Std.DHashMap.Internal.AssocList.nil } }) →
          ((k : α) →
              (v : β k) →
                (l : Std.DHashMap.Internal.AssocList α β) →
                  motive { internalState := { l := Std.DHashMap.Internal.AssocList.cons k v l } }) →
            motive it
-- Mathlib.GroupTheory.Nilpotent
/-- Nilpotency respects isomorphisms.  -/
Group.nilpotent_of_mulEquiv : ∀ {G : Type u_1} [inst : Group G] {G' : Type u_2} [inst_1 : Group G'] [_h : Group.IsNilpotent G] (f : G ≃* G'),
  Group.IsNilpotent G'
-- Init.Data.String.Lemmas.Order
String.Slice.Pos.ne_next : ∀ {s : String.Slice} {p : s.Pos} {h : p ≠ s.endPos}, p ≠ p.next h
-- Lean.ScopedEnvExtension
Lean.ScopedEnvExtension.Descr.mk.sizeOf_spec : ∀ {α β σ : Type} [inst : SizeOf α] [inst_1 : SizeOf β] [inst_2 : SizeOf σ]
  (name : autoParam Lean.Name Lean.ScopedEnvExtension.Descr.name._autoParam) (mkInitial : IO σ)
  (ofOLeanEntry : σ → α → Lean.ImportM β) (toOLeanEntry : β → α) (addEntry : σ → β → σ) (finalizeImport : σ → σ)
  (exportEntry? : Lean.Environment → α → Lean.OLeanEntries (Option α)),
  sizeOf
      { name := name, mkInitial := mkInitial, ofOLeanEntry := ofOLeanEntry, toOLeanEntry := toOLeanEntry,
        addEntry := addEntry, finalizeImport := finalizeImport, exportEntry? := exportEntry? } =
    1 + sizeOf name
-- Mathlib.Algebra.FiniteSupport.Basic
Function.hasFiniteMulSupport_fun_one : ∀ {α : Type u_1} {M : Type u_2} [inst : One M], Function.HasFiniteMulSupport 1
-- Mathlib.CategoryTheory.Limits.Shapes.Pullback.Pasting
CategoryTheory.Limits.inr_inl_pushoutRightPushoutInlIso_hom : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {W X Y Z : C} (f : X ⟶ Y) (g : X ⟶ Z) (f' : Y ⟶ W)
  [inst_1 : CategoryTheory.Limits.HasPushout f g]
  [inst_2 : CategoryTheory.Limits.HasPushout f' (CategoryTheory.Limits.pushout.inl f g)],
  CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pushout.inl f g)
      (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pushout.inr f' (CategoryTheory.Limits.pushout.inl f g))
        (CategoryTheory.Limits.pushoutRightPushoutInlIso f g f').hom) =
    CategoryTheory.CategoryStruct.comp f'
      (CategoryTheory.Limits.pushout.inl (CategoryTheory.CategoryStruct.comp f f') g)
-- Mathlib.Data.DFinsupp.BigOperators
MonoidHom.coe_dfinsuppProd : ∀ {ι : Type u} {β : ι → Type v} [inst : DecidableEq ι] {R : Type u_1} {S : Type u_2} [inst_1 : (i : ι) → Zero (β i)]
  [inst_2 : (i : ι) → (x : β i) → Decidable (x ≠ 0)] [inst_3 : MulOneClass R] [inst_4 : CommMonoid S]
  (f : Π₀ (i : ι), β i) (g : (i : ι) → β i → R →* S), ⇑(f.prod g) = f.prod fun a b => ⇑(g a b)
-- Mathlib.CategoryTheory.MorphismProperty.Comma
CategoryTheory.MorphismProperty.Comma.Hom.comp_left : ∀ {A : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} A] {B : Type u_2}
  [inst_1 : CategoryTheory.Category.{v_2, u_2} B] {T : Type u_3} [inst_2 : CategoryTheory.Category.{v_3, u_3} T]
  {L : CategoryTheory.Functor A T} {R : CategoryTheory.Functor B T} {P : CategoryTheory.MorphismProperty T}
  {Q : CategoryTheory.MorphismProperty A} {W : CategoryTheory.MorphismProperty B} [inst_3 : Q.IsStableUnderComposition]
  [inst_4 : W.IsStableUnderComposition] {X Y Z : CategoryTheory.MorphismProperty.Comma L R P Q W} (f : X.Hom Y)
  (g : Y.Hom Z), (f.comp g).left = CategoryTheory.CategoryStruct.comp f.left g.left
-- Mathlib.CategoryTheory.Monad.EquivMon
CategoryTheory.Monad.toMon_X : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] (M : CategoryTheory.Monad C), M.toMon.X = M.toFunctor
-- Std.Data.TreeSet.Raw.Basic
Std.TreeSet.Raw.instUnion : {α : Type u} → {cmp : α → α → Ordering} → Union (Std.TreeSet.Raw α cmp)
-- Mathlib.NumberTheory.Cyclotomic.Basic
isCyclotomicExtension_singleton_iff_eq_adjoin : ∀ (n : ℕ) [NeZero n] {A : Type u} {B : Type v} [inst : CommRing A] [inst_1 : CommRing B] [inst_2 : Algebra A B]
  [IsDomain B] (C : Subalgebra A B) {ζ : B}, IsPrimitiveRoot ζ n → (IsCyclotomicExtension {n} A ↥C ↔ C = A[ζ])
-- Mathlib.Analysis.Complex.Angle
/-- Chord-length is always less than arc-length.  -/
Complex.norm_sub_le_angle : ∀ {x y : ℂ}, ‖x‖ = 1 → ‖y‖ = 1 → ‖x - y‖ ≤ InnerProductGeometry.angle x y
-- Mathlib.Algebra.Homology.ShortComplex.RightHomology
CategoryTheory.ShortComplex.RightHomologyMapData.congr_φH : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  {S₁ S₂ : CategoryTheory.ShortComplex C} {φ : S₁ ⟶ S₂} {h₁ : S₁.RightHomologyData} {h₂ : S₂.RightHomologyData}
  {γ₁ γ₂ : CategoryTheory.ShortComplex.RightHomologyMapData φ h₁ h₂}, γ₁ = γ₂ → γ₁.φH = γ₂.φH
-- Mathlib.Algebra.Homology.ConcreteCategory
CategoryTheory.ShortComplex.ShortExact.δ_apply : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {FC : C → C → Type u_1} {CC : C → Type v}
  [inst_1 : (X Y : C) → FunLike (FC X Y) (CC X) (CC Y)] [inst_2 : CategoryTheory.ConcreteCategory C FC]
  [inst_3 : CategoryTheory.HasForget₂ C Ab] [inst_4 : CategoryTheory.Abelian C]
  [inst_5 : (CategoryTheory.forget₂ C Ab).Additive] [inst_6 : (CategoryTheory.forget₂ C Ab).PreservesHomology]
  {ι : Type u_2} {c : ComplexShape ι} {S : CategoryTheory.ShortComplex (HomologicalComplex C c)} (hS : S.ShortExact)
  (i j : ι) (hij : c.Rel i j) (x₃ : ↑((CategoryTheory.forget₂ C Ab).obj (S.X₃.X i)))
  (hx₃ : (CategoryTheory.ConcreteCategory.hom ((CategoryTheory.forget₂ C Ab).map (S.X₃.d i j))) x₃ = 0)
  (x₂ : ↑((CategoryTheory.forget₂ C Ab).obj (S.X₂.X i))),
  (CategoryTheory.ConcreteCategory.hom ((CategoryTheory.forget₂ C Ab).map (S.g.f i))) x₂ = x₃ →
    ∀ (x₁ : ↑((CategoryTheory.forget₂ C Ab).obj (S.X₁.X j)))
      (hx₁ :
        (CategoryTheory.ConcreteCategory.hom ((CategoryTheory.forget₂ C Ab).map (S.f.f j))) x₁ =
          (CategoryTheory.ConcreteCategory.hom ((CategoryTheory.forget₂ C Ab).map (S.X₂.d i j))) x₂)
      (k : ι) (hk : c.next j = k),
      (CategoryTheory.ConcreteCategory.hom ((CategoryTheory.forget₂ C Ab).map (hS.δ i j hij)))
          ((CategoryTheory.ConcreteCategory.hom ((CategoryTheory.forget₂ C Ab).map (S.X₃.homologyπ i)))
            (S.X₃.cyclesMk x₃ j ⋯ hx₃)) =
        (CategoryTheory.ConcreteCategory.hom ((CategoryTheory.forget₂ C Ab).map (S.X₁.homologyπ j)))
          (S.X₁.cyclesMk x₁ k hk ⋯)
-- Mathlib.LinearAlgebra.TensorAlgebra.Basic
TensorAlgebra.Rel.add : ∀ {R : Type u_1} [inst : CommSemiring R] {M : Type u_2} [inst_1 : AddCommMonoid M] [inst_2 : Module R M] {a b : M},
  TensorAlgebra.Rel R M (FreeAlgebra.ι R (a + b)) (FreeAlgebra.ι R a + FreeAlgebra.ι R b)
-- Mathlib.NumberTheory.LucasLehmer
LucasLehmer.sMod.eq_def : ∀ (p x : ℕ),
  LucasLehmer.sMod p x =
    match x with
    | 0 => 4 % (2 ^ p - 1)
    | i.succ => (LucasLehmer.sMod p i ^ 2 - 2) % (2 ^ p - 1)
-- Mathlib.GroupTheory.GroupAction.Basic
AddAction.orbitRel_le_snd : ∀ (G : Type u_1) (α : Type u_2) (β : Type u_3) [inst : AddGroup G] [inst_1 : AddAction G α] [inst_2 : AddAction G β],
  AddAction.orbitRel G (α × β) ≤ Setoid.comap Prod.snd (AddAction.orbitRel G β)
-- Std.Tactic.BVDecide.Bitblast.BVExpr.Circuit.Impl.Pred
Std.Tactic.BVDecide.BVPred.bitblast : (aig : Std.Sat.AIG Std.Tactic.BVDecide.BVBit) →
  Std.Tactic.BVDecide.BVExpr.WithCache Std.Tactic.BVDecide.BVPred aig → Std.Tactic.BVDecide.Return aig
-- Mathlib.CategoryTheory.Limits.Constructions.LimitsOfProductsAndEqualizers
CategoryTheory.Limits.hasFiniteColimits_of_hasInitial_and_pushouts : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasInitial C]
  [CategoryTheory.Limits.HasPushouts C], CategoryTheory.Limits.HasFiniteColimits C
-- Mathlib.Algebra.Order.Monoid.Unbundled.Basic
lt_mul_of_one_lt_of_lt' : ∀ {α : Type u_1} [inst : MulOneClass α] [inst_1 : Preorder α] [MulRightMono α] {a b c : α}, 1 < a → b < c → b < a * c
-- Init.Data.ByteArray.Lemmas
ByteArray.set_eq_push_extract_append_extract : ∀ {as : ByteArray} {i : ℕ} (h : i < as.size) {a : UInt8},
  as.set i a h = (as.extract 0 i).push a ++ as.extract (i + 1) as.size
-- Mathlib.Logic.Equiv.Basic
/-- If `α ≃ β`, then for any predicate `p : α → Prop` the subtype `{a // p a}` is equivalent
to the subtype `{b // p (e.symm b)}`. This version is used by `equiv_rw`.  -/
Equiv.subtypeEquivOfSubtype' : {α : Sort u_1} → {β : Sort u_4} → {p : α → Prop} → (e : α ≃ β) → { a // p a } ≃ { b // p (e.symm b) }
-- Mathlib.CategoryTheory.Monoidal.CommComon_
CategoryTheory.CommComon.instCategory : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    [inst_1 : CategoryTheory.MonoidalCategory C] →
      [inst_2 : CategoryTheory.BraidedCategory C] → CategoryTheory.Category.{v₁, max u₁ v₁} (CategoryTheory.CommComon C)
-- Mathlib.Algebra.Homology.Embedding.RestrictionHomology
/-- The isomorphism `(K.restriction e).opcycles j ≅ K.opcycles j'` when `e.f j = j'`
and the predecessors `i` and `i'` of `j` and `j'` satisfy `e.f i = i'`.  -/
HomologicalComplex.restrictionOpcyclesIso : {ι : 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 j : ι) →
                      c.prev j = i →
                        {i' j' : ι'} →
                          e.f i = i' →
                            e.f j = j' →
                              c'.prev j' = i' →
                                [inst_3 : K.HasHomology j'] →
                                  [inst_4 : (K.restriction e).HasHomology j] →
                                    (K.restriction e).opcycles j ≅ K.opcycles j'
-- Mathlib.MeasureTheory.Function.SimpleFunc
MeasureTheory.SimpleFunc.piecewise.congr_simp : ∀ {α : Type u_1} {β : Type u_2} [inst : MeasurableSpace α] (s s_1 : Set α) (e_s : s = s_1) (hs : MeasurableSet s)
  (f f_1 : MeasureTheory.SimpleFunc α β),
  f = f_1 →
    ∀ (g g_1 : MeasureTheory.SimpleFunc α β),
      g = g_1 → MeasureTheory.SimpleFunc.piecewise s hs f g = MeasureTheory.SimpleFunc.piecewise s_1 ⋯ f_1 g_1
-- Mathlib.Probability.Distributions.Uniform
/-- Alternative way of writing the uniformPDF.  -/
MeasureTheory.pdf.uniformPDF_ite : ∀ {E : Type u_1} [inst : MeasurableSpace E] {μ : MeasureTheory.Measure E} {s : Set E} {x : E},
  MeasureTheory.pdf.uniformPDF s x μ = if x ∈ s then (μ s)⁻¹ else 0
-- Mathlib.MeasureTheory.Function.L1Space.HasFiniteIntegral
MeasureTheory.lintegral_enorm_add_left : ∀ {α : Type u_1} {ε' : Type u_5} {ε'' : Type u_6} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α}
  [inst : ENorm ε'] [inst_1 : TopologicalSpace ε''] [inst_2 : ESeminormedAddMonoid ε''] {f : α → ε''},
  MeasureTheory.AEStronglyMeasurable f μ →
    ∀ (g : α → ε'), ∫⁻ (a : α), ‖f a‖ₑ + ‖g a‖ₑ ∂μ = ∫⁻ (a : α), ‖f a‖ₑ ∂μ + ∫⁻ (a : α), ‖g a‖ₑ ∂μ
-- Init.Data.Array.BasicAux
_private.Init.Data.Array.BasicAux.0.List.toArrayAux.eq_2 : ∀ {α : Type u_1} (x : Array α) (a : α) (as : List α), (a :: as).toArrayAux x = as.toArrayAux (x.push a)
-- Mathlib.Topology.UniformSpace.Basic
Filter.HasBasis.uniformity_prod : ∀ {α : Type ua} {β : Type ub} {ιa : Type u_2} {ιb : Type u_3} [inst : UniformSpace α] [inst_1 : UniformSpace β]
  {pa : ιa → Prop} {pb : ιb → Prop} {sa : ιa → SetRel α α} {sb : ιb → SetRel β β},
  (uniformity α).HasBasis pa sa →
    (uniformity β).HasBasis pb sb →
      (uniformity (α × β)).HasBasis (fun i => pa i.1 ∧ pb i.2) fun i => entourageProd (sa i.1) (sb i.2)
-- Mathlib.ModelTheory.FinitelyGenerated
FirstOrder.Language.Structure.CG.mk : ∀ {L : FirstOrder.Language} {M : Type u_1} [inst : L.Structure M], ⊤.CG → FirstOrder.Language.Structure.CG L M
-- Mathlib.ModelTheory.PartialEquiv
/-- Restriction of a partial equivalence to a substructure of the domain.  -/
FirstOrder.Language.PartialEquiv.domRestrict : {L : FirstOrder.Language} →
  {M : Type w} →
    {N : Type w'} →
      [inst : L.Structure M] →
        [inst_1 : L.Structure N] → (f : L.PartialEquiv M N) → {A : L.Substructure M} → A ≤ f.dom → L.PartialEquiv M N