mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.CategoryTheory.Bicategory.NaturalTransformation.Oplax
CategoryTheory.Oplax.OplaxTrans.whiskerRight_naturality_id : ∀ {B : Type u₁} [inst : CategoryTheory.Bicategory B] {C : Type u₂} [inst_1 : CategoryTheory.Bicategory C]
  {F G : CategoryTheory.OplaxFunctor B C} (η : CategoryTheory.Oplax.OplaxTrans F G) {a : B} {a' : C} (f : G.obj a ⟶ a'),
  CategoryTheory.CategoryStruct.comp
      (CategoryTheory.Bicategory.whiskerRight (η.naturality (CategoryTheory.CategoryStruct.id a)) f)
      (CategoryTheory.CategoryStruct.comp
        (CategoryTheory.Bicategory.associator (η.app a) (G.map (CategoryTheory.CategoryStruct.id a)) f).hom
        (CategoryTheory.Bicategory.whiskerLeft (η.app a) (CategoryTheory.Bicategory.whiskerRight (G.mapId a) f))) =
    CategoryTheory.CategoryStruct.comp
      (CategoryTheory.Bicategory.whiskerRight (CategoryTheory.Bicategory.whiskerRight (F.mapId a) (η.app a)) f)
      (CategoryTheory.CategoryStruct.comp
        (CategoryTheory.Bicategory.whiskerRight (CategoryTheory.Bicategory.leftUnitor (η.app a)).hom f)
        (CategoryTheory.CategoryStruct.comp
          (CategoryTheory.Bicategory.whiskerRight (CategoryTheory.Bicategory.rightUnitor (η.app a)).inv f)
          (CategoryTheory.Bicategory.associator (η.app a) (CategoryTheory.CategoryStruct.id (G.obj a)) f).hom))
-- Mathlib.Data.Finset.Sort
Finset.orderEmbOfCardLe.eq_1 : ∀ {α : Type u_1} [inst : LinearOrder α] (s : Finset α) {k : ℕ} (h : k ≤ s.card),
  s.orderEmbOfCardLe h = RelEmbedding.trans (Fin.castLEOrderEmb h) (s.orderEmbOfFin ⋯)
-- Mathlib.AlgebraicGeometry.EllipticCurve.NormalForms
WeierstrassCurve.b₂_of_isCharTwoJNeZeroNF : ∀ {R : Type u_1} [inst : CommRing R] (W : WeierstrassCurve R) [W.IsCharTwoJNeZeroNF], W.b₂ = 1 + 4 * W.a₂
-- Mathlib.CategoryTheory.WithTerminal.Basic
/-- `WithTerminal.star` is terminal.  -/
CategoryTheory.WithTerminal.starTerminal : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] → CategoryTheory.Limits.IsTerminal CategoryTheory.WithTerminal.star
-- Mathlib.Algebra.Quaternion
QuaternionAlgebra.imK_smul : ∀ {S : Type u_1} {R : Type u_3} {c₁ c₂ c₃ : R} [inst : SMul S R] (s : S) (a : QuaternionAlgebra R c₁ c₂ c₃),
  (s • a).imK = s • a.imK
-- Mathlib.Topology.Order.Lattice
ContinuousWithinAt.sup : ∀ {L : Type u_1} {X : Type u_2} [inst : TopologicalSpace L] [inst_1 : TopologicalSpace X] [inst_2 : Max L]
  [ContinuousSup L] {f g : X → L} {s : Set X} {x : X},
  ContinuousWithinAt f s x → ContinuousWithinAt g s x → ContinuousWithinAt (fun a => f a ⊔ g a) s x
-- Mathlib.Algebra.Quaternion
QuaternionAlgebra.imJ_intCast : ∀ {R : Type u_3} {c₁ c₂ c₃ : R} [inst : AddCommGroupWithOne R] (z : ℤ), (↑z).imJ = 0
-- Init.Data.Slice.Array.Lemmas
Array.start_mkSlice_rio : ∀ {α : Type u_1} {xs : Array α} {hi : ℕ}, (Std.Rio.Sliceable.mkSlice xs *...hi).start = 0
-- Mathlib.LinearAlgebra.Matrix.MvPolynomial
/-- Any matrix `A` can be expressed as the evaluation of `Matrix.mvPolynomialX`.

This is of particular use when `MvPolynomial (m × n) R` is an integral domain but `S` is
not, as if the `MvPolynomial.eval₂` can be pulled to the outside of a goal, it can be solved in
under cancellative assumptions.  -/
Matrix.mvPolynomialX_map_eval₂ : ∀ {m : Type u_1} {n : Type u_2} {R : Type u_3} {S : Type u_4} [inst : CommSemiring R] [inst_1 : CommSemiring S]
  (f : R →+* S) (A : Matrix m n S), (Matrix.mvPolynomialX m n R).map (MvPolynomial.eval₂ f fun p => A p.1 p.2) = A
-- Mathlib.Data.Ordmap.Invariants
_private.Mathlib.Data.Ordmap.Invariants.0.Ordnode.mem.match_1.eq_3 : ∀ (motive : Ordering → Sort u_1) (h_1 : Unit → motive Ordering.lt) (h_2 : Unit → motive Ordering.eq)
  (h_3 : Unit → motive Ordering.gt),
  (match Ordering.gt with
    | Ordering.lt => h_1 ()
    | Ordering.eq => h_2 ()
    | Ordering.gt => h_3 ()) =
    h_3 ()
-- Mathlib.Analysis.SpecialFunctions.Trigonometric.Angle
Real.Angle.sin_zero : Real.Angle.sin 0 = 0
-- Mathlib.CategoryTheory.SmallObject.Iteration.Basic
CategoryTheory.SmallObject.SuccStruct.Iteration.mk.injEq : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {J : Type w} {Φ : CategoryTheory.SmallObject.SuccStruct C}
  [inst_1 : LinearOrder J] [inst_2 : SuccOrder J] [inst_3 : OrderBot J]
  [inst_4 : CategoryTheory.Limits.HasIterationOfShape J C] [inst_5 : WellFoundedLT J] {j : J}
  (F : CategoryTheory.Functor (↑(Set.Iic j)) C) (obj_bot : F.obj ⟨⊥, ⋯⟩ = Φ.X₀)
  (arrowSucc_eq :
    ∀ (i : J) (hi : i < j), CategoryTheory.SmallObject.SuccStruct.arrowSucc F i hi = Φ.toSuccArrow (F.obj ⟨i, ⋯⟩))
  (arrowMap_limit :
    ∀ (i : J) (hi : Order.IsSuccLimit i) (hij : i ≤ j) (k : J) (hk : k < i),
      CategoryTheory.SmallObject.SuccStruct.arrowMap F k i ⋯ hij =
        CategoryTheory.SmallObject.SuccStruct.arrowι (CategoryTheory.SmallObject.restrictionLT F hij) hi k hk)
  (F_1 : CategoryTheory.Functor (↑(Set.Iic j)) C) (obj_bot_1 : F_1.obj ⟨⊥, ⋯⟩ = Φ.X₀)
  (arrowSucc_eq_1 :
    ∀ (i : J) (hi : i < j), CategoryTheory.SmallObject.SuccStruct.arrowSucc F_1 i hi = Φ.toSuccArrow (F_1.obj ⟨i, ⋯⟩))
  (arrowMap_limit_1 :
    ∀ (i : J) (hi : Order.IsSuccLimit i) (hij : i ≤ j) (k : J) (hk : k < i),
      CategoryTheory.SmallObject.SuccStruct.arrowMap F_1 k i ⋯ hij =
        CategoryTheory.SmallObject.SuccStruct.arrowι (CategoryTheory.SmallObject.restrictionLT F_1 hij) hi k hk),
  ({ F := F, obj_bot := obj_bot, arrowSucc_eq := arrowSucc_eq, arrowMap_limit := arrowMap_limit } =
      { F := F_1, obj_bot := obj_bot_1, arrowSucc_eq := arrowSucc_eq_1, arrowMap_limit := arrowMap_limit_1 }) =
    (F = F_1)
-- Mathlib.Algebra.MvPolynomial.Basic
MvPolynomial.coeff_C : ∀ {R : Type u} {σ : Type u_1} [inst : CommSemiring R] [inst_1 : DecidableEq σ] (m : σ →₀ ℕ) (a : R),
  MvPolynomial.coeff m (MvPolynomial.C a) = if 0 = m then a else 0
-- Mathlib.Combinatorics.SimpleGraph.CompleteMultipartite
SimpleGraph.CompleteEquipartiteSubgraph.mk.sizeOf_spec : ∀ {V : Type u_1} {G : SimpleGraph V} {r t : ℕ} [inst : SizeOf V] (parts : Finset (Finset V))
  (card_parts : parts.card = r ∨ t = 0) (card_mem_parts : ∀ {p : Finset V}, p ∈ parts → p.card = t)
  (isCompleteBetween : (↑parts).Pairwise fun x1 x2 => G.IsCompleteBetween ↑x1 ↑x2),
  sizeOf
      { parts := parts, card_parts := card_parts, card_mem_parts := card_mem_parts,
        isCompleteBetween := isCompleteBetween } =
    1 + sizeOf parts + sizeOf card_parts
-- Mathlib.Topology.Algebra.InfiniteSum.NatInt
/-- If `f₀, f₁, f₂, ...` and `g₀, g₁, g₂, ...` are both multipliable then so is the
`ℤ`-indexed sequence: `..., g₂, g₁, g₀, f₀, f₁, f₂, ...` (with `f₀` at the `0`-th position).  -/
Multipliable.int_rec : ∀ {M : Type u_1} [inst : CommMonoid M] [inst_1 : TopologicalSpace M] [ContinuousMul M] {f g : ℕ → M},
  Multipliable f → Multipliable g → Multipliable fun t => Int.rec f g t
-- Init.Data.List.Lemmas
List.append_concat : ∀ {α : Type u_1} {a : α} {l₁ l₂ : List α}, l₁ ++ l₂.concat a = (l₁ ++ l₂).concat a
-- Mathlib.Algebra.Order.Monovary
monovaryOn_inv_left : ∀ {ι : Type u_1} {α : Type u_2} {β : Type u_3} [inst : CommGroup α] [inst_1 : Preorder α] [IsOrderedMonoid α]
  [inst_3 : PartialOrder β] {s : Set ι} {f : ι → α} {g : ι → β}, MonovaryOn f⁻¹ g s ↔ AntivaryOn f g s
-- Mathlib.Topology.Algebra.GroupWithZero
Homeomorph.mulLeft₀_symm_apply : ∀ {α : Type u_1} [inst : TopologicalSpace α] [inst_1 : GroupWithZero α] [inst_2 : SeparatelyContinuousMul α] (c : α)
  (hc : c ≠ 0), ⇑(Homeomorph.mulLeft₀ c hc).symm = fun x => c⁻¹ * x
-- Mathlib.Topology.NhdsWithin
nhdsSetWithin_prod_le : ∀ {α : Type u_1} {β : Type u_2} [inst : TopologicalSpace α] [inst_1 : TopologicalSpace β] {s s' : Set α} {t t' : Set β},
  nhdsSetWithin (s ×ˢ t) (s' ×ˢ t') ≤ nhdsSetWithin s s' ×ˢ nhdsSetWithin t t'
-- Mathlib.Data.List.InsertIdx
List.eq_or_mem_of_mem_insertIdx : ∀ {α : Type u} {l : List α} {n : ℕ} {a b : α}, a ∈ l.insertIdx n b → a = b ∨ a ∈ l
-- Lean.Data.Lsp.LanguageFeatures
Lean.Lsp.SemanticTokensParams.mk.inj : ∀ {textDocument textDocument_1 : Lean.Lsp.TextDocumentIdentifier},
  { textDocument := textDocument } = { textDocument := textDocument_1 } → textDocument = textDocument_1
-- Lean.Meta.Match.Match
Lean.Meta.Match.MkMatcherInput.numDiscrs : Lean.Meta.Match.MkMatcherInput → ℕ
-- Mathlib.CategoryTheory.Limits.FunctorCategory.Shapes.Images
CategoryTheory.FunctorToTypes.monoFactorisation_I : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] {F G : CategoryTheory.Functor C (Type u)} (f : F ⟶ G),
  (CategoryTheory.FunctorToTypes.monoFactorisation f).I = (CategoryTheory.Subfunctor.range f).toFunctor
-- Mathlib.Probability.Kernel.Composition.IntegralCompProd
ProbabilityTheory.Kernel.lintegral_fn_integral_sub : ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} {E : Type u_4} {mα : MeasurableSpace α} {mβ : MeasurableSpace β}
  {mγ : MeasurableSpace γ} [inst : NormedAddCommGroup E] {a : α} {κ : ProbabilityTheory.Kernel α β}
  [ProbabilityTheory.IsSFiniteKernel κ] {η : ProbabilityTheory.Kernel (α × β) γ} [ProbabilityTheory.IsSFiniteKernel η]
  [inst_3 : NormedSpace ℝ E] ⦃f g : β × γ → E⦄ (F : E → ENNReal),
  MeasureTheory.Integrable f ((κ.compProd η) a) →
    MeasureTheory.Integrable g ((κ.compProd η) a) →
      ∫⁻ (x : β), F (∫ (y : γ), f (x, y) - g (x, y) ∂η (a, x)) ∂κ a =
        ∫⁻ (x : β), F (∫ (y : γ), f (x, y) ∂η (a, x) - ∫ (y : γ), g (x, y) ∂η (a, x)) ∂κ a
-- Mathlib.Algebra.Lie.Basic
LieEquiv.symm_apply_apply : ∀ {R : Type u} {L₁ : Type v} {L₂ : Type w} [inst : CommRing R] [inst_1 : LieRing L₁] [inst_2 : LieRing L₂]
  [inst_3 : LieAlgebra R L₁] [inst_4 : LieAlgebra R L₂] (e : L₁ ≃ₗ⁅R⁆ L₂) (x : L₁), e.symm (e x) = x
-- Init.Data.BitVec.Basic
BitVec.ofBool_true : BitVec.ofBool true = 1
-- Mathlib.Analysis.SpecialFunctions.RegularizedHypergeometric
/-- The regularized hypergeometric series with `a = b = 0` is exponential series.  -/
Complex.regularizedHGFunSeries_zero_zero : Complex.regularizedHGFunSeries 0 0 = NormedSpace.expSeries ℂ ℂ
-- Mathlib.RingTheory.Ideal.GoingUp
Ideal.IsIntegral.isMaximal_of_isMaximal_comap : ∀ {R : Type u_1} [inst : CommRing R] {A : Type u_3} [inst_1 : CommRing A] [inst_2 : Algebra R A]
  [Algebra.IsIntegral R A] (I : Ideal A) [I.IsPrime], (Ideal.comap (algebraMap R A) I).IsMaximal → I.IsMaximal
-- Mathlib.RingTheory.LocalProperties.Exactness
exact_of_isLocalized_maximal : ∀ {R : Type u_1} {M : Type u_2} {N : Type u_3} {L : Type u_4} [inst : CommSemiring R] [inst_1 : AddCommMonoid M]
  [inst_2 : Module R M] [inst_3 : AddCommMonoid N] [inst_4 : Module R N] [inst_5 : AddCommMonoid L]
  [inst_6 : Module R L] (Mₚ : (P : Ideal R) → [P.IsMaximal] → Type u_6)
  [inst_7 : (P : Ideal R) → [inst : P.IsMaximal] → AddCommMonoid (Mₚ P)]
  [inst_8 : (P : Ideal R) → [inst_8 : P.IsMaximal] → Module R (Mₚ P)]
  (f : (P : Ideal R) → [inst_9 : P.IsMaximal] → M →ₗ[R] Mₚ P)
  [inst_9 : ∀ (P : Ideal R) [inst_9 : P.IsMaximal], IsLocalizedModule.AtPrime P (f P)]
  (Nₚ : (P : Ideal R) → [P.IsMaximal] → Type u_7)
  [inst_10 : (P : Ideal R) → [inst : P.IsMaximal] → AddCommMonoid (Nₚ P)]
  [inst_11 : (P : Ideal R) → [inst_11 : P.IsMaximal] → Module R (Nₚ P)]
  (g : (P : Ideal R) → [inst_12 : P.IsMaximal] → N →ₗ[R] Nₚ P)
  [inst_12 : ∀ (P : Ideal R) [inst_12 : P.IsMaximal], IsLocalizedModule.AtPrime P (g P)]
  (Lₚ : (P : Ideal R) → [P.IsMaximal] → Type u_8)
  [inst_13 : (P : Ideal R) → [inst : P.IsMaximal] → AddCommMonoid (Lₚ P)]
  [inst_14 : (P : Ideal R) → [inst_14 : P.IsMaximal] → Module R (Lₚ P)]
  (h : (P : Ideal R) → [inst_15 : P.IsMaximal] → L →ₗ[R] Lₚ P)
  [inst_15 : ∀ (P : Ideal R) [inst_15 : P.IsMaximal], IsLocalizedModule.AtPrime P (h P)] (F : M →ₗ[R] N)
  (G : N →ₗ[R] L),
  (∀ (J : Ideal R) [inst_16 : J.IsMaximal],
      Function.Exact ⇑((IsLocalizedModule.map J.primeCompl (f J) (g J)) F)
        ⇑((IsLocalizedModule.map J.primeCompl (g J) (h J)) G)) →
    Function.Exact ⇑F ⇑G
-- Mathlib.Topology.ContinuousMap.Algebra
ContinuousMap.instSemiringOfIsTopologicalSemiring : {α : Type u_1} →
  {β : Type u_2} →
    [inst : TopologicalSpace α] →
      [inst_1 : TopologicalSpace β] → [inst_2 : Semiring β] → [IsTopologicalSemiring β] → Semiring C(α, β)
-- Mathlib.GroupTheory.Submonoid.Center
MulOpposite.op_mem_center_iff : ∀ {M : Type u_2} [inst : Mul M] {x : M}, MulOpposite.op x ∈ Set.center Mᵐᵒᵖ ↔ x ∈ Set.center M
-- Mathlib.Data.Finset.NoncommProd
Multiset.noncommFoldr_coe : ∀ {α : Type u_3} {β : Type u_4} (f : α → β → β) (l : List α)
  (comm : {x | x ∈ ↑l}.Pairwise fun x y => ∀ (b : β), f x (f y b) = f y (f x b)) (b : β),
  Multiset.noncommFoldr f (↑l) comm b = List.foldr f b l
-- Init.Data.SInt.Lemmas
Int32.pow_zero : ∀ (x : Int32), x ^ 0 = 1
-- Init.Data.Ord.Basic
/-- Constructs an `LT` instance from an `Ord` instance.
 -/
Ord.toLT : {α : Type u_1} → Ord α → LT α
-- Mathlib.LinearAlgebra.Span.Basic
LinearEquiv.toSpanNonzeroSingleton.congr_simp : ∀ (R : Type u_1) (M : Type u_4) [inst : Ring R] [inst_1 : IsDomain R] [inst_2 : AddCommGroup M] [inst_3 : Module R M]
  [inst_4 : Module.IsTorsionFree R M] (x : M) (h : x ≠ 0),
  LinearEquiv.toSpanNonzeroSingleton R M x h = LinearEquiv.toSpanNonzeroSingleton R M x h
-- Mathlib.RingTheory.GradedAlgebra.Homogeneous.Ideal
Ideal.homogeneousHull_eq_sInf : ∀ {ι : Type u_1} {σ : Type u_2} {A : Type u_3} [inst : Semiring A] [inst_1 : DecidableEq ι] [inst_2 : AddMonoid ι]
  [inst_3 : SetLike σ A] [inst_4 : AddSubmonoidClass σ A] (𝒜 : ι → σ) [inst_5 : GradedRing 𝒜] (I : Ideal A),
  Ideal.homogeneousHull 𝒜 I = sInf {J | I ≤ J.toIdeal}
-- Mathlib.Algebra.CharP.Invertible
/-- A natural number `t` is invertible in a semifield `K` of characteristic `p` if `p` does not
divide `t`.  -/
invertibleOfCharPNotDvd : {K : Type u_2} → [inst : Semifield K] → {p : ℕ} → [CharP K p] → {t : ℕ} → ¬p ∣ t → Invertible ↑t
-- Lean.Elab.Binders
Lean.Elab.Term.expandWhereDeclsOpt : Lean.Syntax → Lean.Syntax → Lean.MacroM Lean.Syntax
-- Mathlib.Order.Disjoint
codisjoint_iff_le_sup : ∀ {α : Type u_1} [inst : SemilatticeSup α] [inst_1 : OrderTop α] {a b : α}, Codisjoint a b ↔ ⊤ ≤ a ⊔ b
-- Mathlib.Order.BooleanAlgebra.Set
Set.ite_inter_compl_self : ∀ {α : Type u_1} (t s s' : Set α), t.ite s s' ∩ tᶜ = s' ∩ tᶜ
-- Mathlib.Algebra.SkewPolynomial.Basic
SkewPolynomial.coeff_one_zero : ∀ {R : Type u_1} [inst : Semiring R], SkewPolynomial.coeff 1 0 = 1
-- Mathlib.CategoryTheory.Limits.Preserves.Grothendieck
/-- If `colim` on a category `C` preserves limits of shape `J` and if it does so for `colim` on
every `F.obj c` for a functor `F : C ⥤ Cat`, then `colim` on `Grothendieck F` also preserves limits
of shape `J`.  -/
CategoryTheory.Limits.preservesLimitsOfShape_colim_grothendieck : ∀ (C : Type u₁) [inst : CategoryTheory.Category.{v₁, u₁} C] {H : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} H]
  {J : Type u₃} [inst_2 : CategoryTheory.Category.{v₃, u₃} J] (F : CategoryTheory.Functor C CategoryTheory.Cat)
  [inst_3 : CategoryTheory.Limits.HasColimitsOfShape C H] [CategoryTheory.Limits.HasLimitsOfShape J H]
  [inst_5 : ∀ (c : C), CategoryTheory.Limits.HasColimitsOfShape (↑(F.obj c)) H]
  [CategoryTheory.Limits.PreservesLimitsOfShape J CategoryTheory.Limits.colim]
  [∀ (c : C), CategoryTheory.Limits.PreservesLimitsOfShape J CategoryTheory.Limits.colim],
  CategoryTheory.Limits.PreservesLimitsOfShape J CategoryTheory.Limits.colim
-- Mathlib.Combinatorics.SimpleGraph.Copy
/-- There's at least as many labelled copies of `H` in `G` than unlabelled ones.  -/
SimpleGraph.copyCount_le_labelledCopyCount : ∀ {V : Type u_1} {W : Type u_2} {G : SimpleGraph V} {H : SimpleGraph W} [inst : Fintype V] [inst_1 : Fintype W],
  G.copyCount H ≤ G.labelledCopyCount H
-- Mathlib.CategoryTheory.Action
CategoryTheory.ActionCategory.uncurry_obj : ∀ {X : Type u} {G : Type u_2} [inst : Group G] [inst_1 : MulAction G X] {H : Type u_3} [inst_2 : Group H]
  (F : G →* (X → H) ⋊[mulAutArrow] G) (sane : ∀ (g : G), (F g).right = g) (x : CategoryTheory.ActionCategory G X),
  (CategoryTheory.ActionCategory.uncurry F sane).obj x = ()
-- Lean.Elab.Binders
Lean.Elab.Term.expandFun : Lean.Macro
-- Std.Data.ExtDHashMap.Lemmas
Std.ExtDHashMap.getKey!_union : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} {β : α → Type v} {m₁ m₂ : Std.ExtDHashMap α β} [inst : EquivBEq α]
  [inst_1 : LawfulHashable α] [inst_2 : Inhabited α] {k : α}, (m₁ ∪ m₂).getKey! k = m₂.getKeyD k (m₁.getKey! k)
-- Mathlib.Order.Ideal
/-- This ideal is maximal in the collection of proper ideals.  -/
Order.Ideal.IsMaximal.maximal_proper : ∀ {P : Type u_1} {inst : LE P} {I : Order.Ideal P} [self : I.IsMaximal] ⦃J : Order.Ideal P⦄, I < J → ↑J = Set.univ
-- Mathlib.ModelTheory.DirectLimit
FirstOrder.Language.DirectLimit.of_f : ∀ {L : FirstOrder.Language} {ι : Type v} [inst : Preorder ι] {G : ι → Type w} [inst_1 : (i : ι) → L.Structure (G i)]
  {f : (i j : ι) → i ≤ j → L.Embedding (G i) (G j)} [inst_2 : IsDirectedOrder ι]
  [inst_3 : DirectedSystem G fun i j h => ⇑(f i j h)] [inst_4 : Nonempty ι] {i j : ι} {hij : i ≤ j} {x : G i},
  (FirstOrder.Language.DirectLimit.of L ι G f j) ((f i j hij) x) = (FirstOrder.Language.DirectLimit.of L ι G f i) x
-- Mathlib.Data.Finset.SDiff
Finset.sdiff_eq_sdiff_iff_inter_eq_inter : ∀ {α : Type u_1} [inst : DecidableEq α] {s t₁ t₂ : Finset α}, s \ t₁ = s \ t₂ ↔ s ∩ t₁ = s ∩ t₂
-- Mathlib.GroupTheory.GroupAction.Basic
AddAction.stabilizerEquivStabilizer_zero : ∀ {G : Type u_1} {α : Type u_2} [inst : AddGroup G] [inst_1 : AddAction G α] {a : α},
  AddAction.stabilizerEquivStabilizer ⋯ = AddEquiv.refl ↥(AddAction.stabilizer G a)
-- Batteries.Data.Stream
Std.Stream.snd_takeTR : ∀ {σ : Type u_1} {α : Type u_2} [inst : Std.Stream σ α] (s : σ) (n : ℕ), (Std.Stream.takeTR s n).2 = Std.Stream.drop s n
-- Std.Data.HashSet.RawLemmas
Std.HashSet.Raw.getD_diff : ∀ {α : Type u} [inst : BEq α] [inst_1 : Hashable α] {m₁ m₂ : Std.HashSet.Raw α} [EquivBEq α] [LawfulHashable α],
  m₁.WF → m₂.WF → ∀ {k fallback : α}, (m₁ \ m₂).getD k fallback = if k ∈ m₂ then fallback else m₁.getD k fallback
-- Mathlib.LinearAlgebra.Matrix.Determinant.Bird.Defs
BirdDet.birdDet_eq : ∀ {R : Type u_1} [inst : CommRing R] (n k : ℕ) (A : Array R),
  n = k + 1 → BirdDet.birdDet n A = (-1) ^ k * (BirdDet.stepEntry n A)^[k] (BirdDet.get n A) 0 0
-- Mathlib.Algebra.Group.Pointwise.Finset.Basic
Finset.image_pow_of_ne_zero : ∀ {F : Type u_1} {α : Type u_2} {β : Type u_3} [inst : DecidableEq α] [inst_1 : DecidableEq β] [inst_2 : Monoid α]
  [inst_3 : Monoid β] [inst_4 : FunLike F α β] [MulHomClass F α β] {n : ℕ},
  n ≠ 0 → ∀ (f : F) (s : Finset α), Finset.image (⇑f) (s ^ n) = Finset.image (⇑f) s ^ n
-- Std.Data.TreeMap.Lemmas
Std.TreeMap.maxKey?_insert : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Std.TreeMap α β cmp} [Std.TransCmp cmp] {k : α} {v : β},
  (t.insert k v).maxKey? = some (t.maxKey?.elim k fun k' => if (cmp k' k).isLE = true then k else k')
-- Mathlib.Data.Finset.Card
Finset.card_eq_succ : ∀ {α : Type u_1} {s : Finset α} {n : ℕ} [inst : DecidableEq α],
  s.card = n + 1 ↔ ∃ a t, a ∉ t ∧ insert a t = s ∧ t.card = n
-- Mathlib.Topology.Algebra.Group.Torsor
ContinuousWithinAt.sdiv : ∀ {V : Type u_1} {P : Type u_2} {α : Type u_3} [inst : Group V] [inst_1 : TopologicalSpace V] [inst_2 : Torsor V P]
  [inst_3 : TopologicalSpace P] [IsTopologicalTorsor P] [inst_5 : TopologicalSpace α] {f g : α → P} {x : α} {s : Set α},
  ContinuousWithinAt f s x → ContinuousWithinAt g s x → ContinuousWithinAt (fun x => f x /ₛ g x) s x
-- Mathlib.Analysis.InnerProductSpace.LinearMap
/-- A linear map that preserves the inner product is a linear isometry.  -/
LinearMap.isometryOfInner : {𝕜 : Type u_1} →
  {E : Type u_2} →
    [inst : RCLike 𝕜] →
      [inst_1 : SeminormedAddCommGroup E] →
        [inst_2 : InnerProductSpace 𝕜 E] →
          {E' : Type u_7} →
            [inst_3 : SeminormedAddCommGroup E'] →
              [inst_4 : InnerProductSpace 𝕜 E'] →
                (f : E →ₗ[𝕜] E') → (∀ (x y : E), inner 𝕜 (f x) (f y) = inner 𝕜 x y) → E →ₗᵢ[𝕜] E'
-- Mathlib.MeasureTheory.Function.AEEqFun
/-- The class of `x ↦ (f x, g x)`.  -/
MeasureTheory.AEEqFun.pair : {α : Type u_1} →
  {β : Type u_2} →
    {γ : Type u_3} →
      [inst : MeasurableSpace α] →
        {μ : MeasureTheory.Measure α} →
          [inst_1 : TopologicalSpace β] → [inst_2 : TopologicalSpace γ] → (α →ₘ[μ] β) → (α →ₘ[μ] γ) → α →ₘ[μ] β × γ
-- Mathlib.CategoryTheory.Limits.Types.Limits
CategoryTheory.Limits.Types.Limit.w_apply : ∀ {J : Type v} [inst : CategoryTheory.Category.{w, v} J] {F : CategoryTheory.Functor J (Type u)}
  [inst_1 : CategoryTheory.Limits.HasLimit F] {j j' : J} {x : CategoryTheory.Limits.limit F} (f : j ⟶ j'),
  (CategoryTheory.ConcreteCategory.hom (F.map f))
      ((CategoryTheory.ConcreteCategory.hom (CategoryTheory.Limits.limit.π F j)) x) =
    (CategoryTheory.ConcreteCategory.hom (CategoryTheory.Limits.limit.π F j')) x
-- Mathlib.CategoryTheory.Triangulated.TStructure.TruncLEGT
CategoryTheory.Triangulated.TStructure.π_truncGTIsoTruncGE_inv : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Preadditive C]
  [inst_2 : CategoryTheory.Limits.HasZeroObject C] [inst_3 : CategoryTheory.HasShift C ℤ]
  [inst_4 : ∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive] [inst_5 : CategoryTheory.Pretriangulated C]
  (t : CategoryTheory.Triangulated.TStructure C) (a b : ℤ) (h : a + 1 = b),
  CategoryTheory.CategoryStruct.comp (t.truncGEπ b) (t.truncGTIsoTruncGE a b h).inv = t.truncGTπ a
-- Init.Control.ExceptCps
ExceptCpsT.instInhabited : {ε : Type u_1} → {m : Type u_1 → Type u_2} → {α : Type u_1} → [Inhabited ε] → Inhabited (ExceptCpsT ε m α)
-- Mathlib.Data.Nat.Factors
Nat.four_dvd_or_exists_odd_prime_and_dvd_of_two_lt : ∀ {n : ℕ}, 2 < n → 4 ∣ n ∨ ∃ p, Nat.Prime p ∧ p ∣ n ∧ Odd p
-- Mathlib.CategoryTheory.Monoidal.Braided.Multifunctor
CategoryTheory.BraidedCategory.Hexagon.functor₁₂₃'_obj_obj_obj : ∀ (C : Type u_1) [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.MonoidalCategory C]
  (X₁ X₂ X₃ : C),
  (((CategoryTheory.BraidedCategory.Hexagon.functor₁₂₃' C).obj X₁).obj X₂).obj X₃ =
    CategoryTheory.MonoidalCategoryStruct.tensorObj X₁ (CategoryTheory.MonoidalCategoryStruct.tensorObj X₂ X₃)
-- Mathlib.CategoryTheory.Limits.Types.Coproducts
CategoryTheory.Limits.CofanTypes.inj_injective_of_isColimit : ∀ {C : Type u} {F : C → Type v} {c : CategoryTheory.Limits.CofanTypes F},
  CategoryTheory.Functor.CoconeTypes.IsColimit c → ∀ (i : C), Function.Injective (c.inj i)
-- Mathlib.CategoryTheory.Sites.Hypercover.Zero
CategoryTheory.Precoverage.ZeroHypercover.instHasPullbacksPresieve₀OfHasPullbacks : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] (K : CategoryTheory.Precoverage C) [K.HasPullbacks] {X Y : C}
  (E : K.ZeroHypercover X) (f : Y ⟶ X), E.presieve₀.HasPullbacks f
-- Mathlib.Algebra.BigOperators.Field
Finset.dens_eq_sum_dens_fiberwise : ∀ {α : Type u_3} {β : Type u_4} [inst : Fintype β] {s : Finset α} [inst_1 : DecidableEq α] {f : β → α} {t : Finset β},
  Set.MapsTo f ↑t ↑s → t.dens = ∑ a ∈ s, {b ∈ t | f b = a}.dens
-- Std.Time.Date.Unit.Day
/-- Convert `Hour.Offset` into `Day.Offset`.
 -/
Std.Time.Day.Offset.ofHours : Std.Time.Hour.Offset → Std.Time.Day.Offset
-- Mathlib.Order.Sublattice
Sublattice.coe_sInf : ∀ {α : Type u_2} [inst : Lattice α] (S : Set (Sublattice α)), ↑(sInf S) = ⋂ L ∈ S, ↑L
-- Mathlib.Topology.Algebra.Group.Basic
nhdsAddHom_apply : ∀ {G : Type w} [inst : TopologicalSpace G] [inst_1 : AddGroup G] [inst_2 : IsTopologicalAddGroup G] (x : G),
  nhdsAddHom x = nhds x
-- Mathlib.RingTheory.Localization.Defs
IsLocalization.map_comp : ∀ {R : Type u_1} [inst : CommSemiring R] {M : Submonoid R} {S : Type u_2} [inst_1 : CommSemiring S]
  [inst_2 : Algebra R S] {P : Type u_3} [inst_3 : CommSemiring P] [inst_4 : IsLocalization M S] {g : R →+* P}
  {T : Submonoid P} {Q : Type u_4} [inst_5 : CommSemiring Q] [inst_6 : Algebra P Q] [inst_7 : IsLocalization T Q]
  (hy : M ≤ Submonoid.comap g T), (IsLocalization.map Q g hy).comp (algebraMap R S) = (algebraMap P Q).comp g
-- Mathlib.Geometry.Manifold.BumpFunction
SmoothBumpFunction.support_subset_source : ∀ {E : Type uE} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] {H : Type uH} [inst_2 : TopologicalSpace H]
  {I : ModelWithCorners ℝ E H} {M : Type uM} [inst_3 : TopologicalSpace M] [inst_4 : ChartedSpace H M] {c : M}
  (f : SmoothBumpFunction I c) [inst_5 : FiniteDimensional ℝ E], Function.support ↑f ⊆ (chartAt H c).source
-- Mathlib.Data.ZMod.Basic
ZMod.val_natCast : ∀ (n a : ℕ), (↑a).val = a % n