mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Analysis.Normed.Order.Hom.Basic
GroupSeminormClass.toSeminormedCommGroup.eq_1 : ∀ {F : Type u_1} {α : Type u_2} [inst : FunLike F α ℝ] [inst_1 : CommGroup α] [inst_2 : GroupSeminormClass F α ℝ]
  (f : F),
  GroupSeminormClass.toSeminormedCommGroup f =
    { toNorm := (GroupSeminormClass.toSeminormedGroup f).toNorm,
      toGroup := (GroupSeminormClass.toSeminormedGroup f).toGroup, mul_comm := ⋯,
      toPseudoMetricSpace := (GroupSeminormClass.toSeminormedGroup f).toPseudoMetricSpace, dist_eq := ⋯ }
-- Mathlib.CategoryTheory.Triangulated.Subcategory
CategoryTheory.ObjectProperty.trW.shift : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Limits.HasZeroObject C]
  [inst_2 : CategoryTheory.HasShift C ℤ] [inst_3 : CategoryTheory.Preadditive C]
  [inst_4 : ∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive] [inst_5 : CategoryTheory.Pretriangulated C]
  {P : CategoryTheory.ObjectProperty C} [P.IsStableUnderShift ℤ] {X₁ X₂ : C} {f : X₁ ⟶ X₂},
  P.trW f → ∀ (n : ℤ), P.trW ((CategoryTheory.shiftFunctor C n).map f)
-- Mathlib.Analysis.Analytic.Order
Nat.cast_analyticOrderNatAt : ∀ {𝕜 : Type u_1} {E : Type u_2} [inst : NontriviallyNormedField 𝕜] [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {f : 𝕜 → E} {z₀ : 𝕜},
  analyticOrderAt f z₀ ≠ ⊤ → ↑(analyticOrderNatAt f z₀) = analyticOrderAt f z₀
-- Mathlib.NumberTheory.ModularForms.SlashInvariantForms
SlashInvariantFormClass.slash_action_eq : ∀ {F : Type u_1} {Γ : outParam (Subgroup (GL (Fin 2) ℝ))} {k : outParam ℤ} {inst : FunLike F UpperHalfPlane ℂ}
  [self : SlashInvariantFormClass F Γ k] (f : F), ∀ γ ∈ Γ, SlashAction.map k γ ⇑f = ⇑f
-- Init.Data.UInt.Lemmas
UInt16.toUInt64_neg : ∀ (a : UInt16), (-a).toUInt64 = -a.toUInt64 % 65536
-- Mathlib.MeasureTheory.Function.SimpleFunc
MeasureTheory.SimpleFunc.FinMeasSupp.map_iff : ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} {m : MeasurableSpace α} [inst : Zero β] [inst_1 : Zero γ]
  {μ : MeasureTheory.Measure α} {f : MeasureTheory.SimpleFunc α β} {g : β → γ},
  (∀ {b : β}, g b = 0 ↔ b = 0) → ((MeasureTheory.SimpleFunc.map g f).FinMeasSupp μ ↔ f.FinMeasSupp μ)
-- Mathlib.CategoryTheory.GradedObject.Trifunctor
CategoryTheory.GradedObject.mapTrifunctorObj_obj_map : ∀ {C₁ : Type u_1} {C₂ : Type u_2} {C₃ : Type u_3} {C₄ : Type u_4} [inst : CategoryTheory.Category.{v_1, u_1} C₁]
  [inst_1 : CategoryTheory.Category.{v_2, u_2} C₂] [inst_2 : CategoryTheory.Category.{v_3, u_3} C₃]
  [inst_3 : CategoryTheory.Category.{v_4, u_4} C₄]
  (F : CategoryTheory.Functor C₁ (CategoryTheory.Functor C₂ (CategoryTheory.Functor C₃ C₄))) {I₁ : Type u_7}
  (X₁ : CategoryTheory.GradedObject I₁ C₁) (I₂ : Type u_8) (I₃ : Type u_9) (X₂ : CategoryTheory.GradedObject I₂ C₂)
  {x x_1 : CategoryTheory.GradedObject I₃ C₃} (φ : x ⟶ x_1) (x_2 : I₁ × I₂ × I₃),
  ((CategoryTheory.GradedObject.mapTrifunctorObj F X₁ I₂ I₃).obj X₂).map φ x_2 =
    ((F.obj (X₁ x_2.1)).obj (X₂ x_2.2.1)).map (φ x_2.2.2)
-- Init.Data.Iterators.Basic
/-- This theorem is used by a `decreasing_trivial` extension. It powers automatic termination proofs
with `IterM.finitelyManySteps`.
 -/
Std.Iter.TerminationMeasures.Finite.rel_of_yield : ∀ {α β : Type w} [inst : Std.Iterator α Id β] {it it' : Std.Iter β} {out : β},
  it.IsPlausibleStep (Std.IterStep.yield it' out) → { it := it'.toIterM }.Rel { it := it.toIterM }
-- Mathlib.Algebra.Homology.SpectralObject.HasSpectralSequence
CategoryTheory.Abelian.SpectralObject.coreE₂HomologicalNat_i₁ : ∀ (pq : ℕ × ℕ), CategoryTheory.Abelian.SpectralObject.coreE₂HomologicalNat.i₁ pq = WithBotTop.coe (-↑pq.2)
-- Mathlib.CategoryTheory.Join.Opposites
CategoryTheory.Join.InclLeftCompRightOpOpEquivFunctor_inv_app : ∀ (C : Type u₁) (D : Type u₂) [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  (X : C),
  (CategoryTheory.Join.InclLeftCompRightOpOpEquivFunctor C D).inv.app X =
    CategoryTheory.CategoryStruct.id (Opposite.op (CategoryTheory.Join.right (Opposite.op X)))
-- Mathlib.Logic.Nontrivial.Basic
Subsingleton.le : ∀ {α : Type u_1} [inst : Preorder α] [Subsingleton α] (x y : α), x ≤ y
-- Std.Data.ExtDHashMap.Lemmas
Std.ExtDHashMap.containsThenInsertIfNew.congr_simp : ∀ {α : Type u} {β : α → Type v} {x : BEq α} {x_1 : Hashable α} [inst : EquivBEq α] [inst_1 : LawfulHashable α]
  (m m_1 : Std.ExtDHashMap α β),
  m = m_1 → ∀ (a : α) (b b_1 : β a), b = b_1 → m.containsThenInsertIfNew a b = m_1.containsThenInsertIfNew a b_1
-- Mathlib.AlgebraicTopology.SimplicialSet.AnodyneExtensions.UnionProd
SSet.prodStdSimplex.pairingCore.IsType₂.type₁_eq_of_δ_eq : ∀ {m : ℕ} {k : Fin (m + 1)} {n : ℕ} {t : ((SSet.horn (m + 1) k.castSucc).unionProd (SSet.boundary n)).N}
  (ht : SSet.prodStdSimplex.pairingCore.IsType₂ t) (s : SSet.prodStdSimplex.pairingCore.Type₁ k n),
  s.δ = t → ∀ {d : ℕ} (hd : t.dim = d), ht.type₁ hd = s
-- Mathlib.Analysis.SpecialFunctions.BinaryEntropy
Real.strictConcaveOn_qaryEntropy : ∀ {q : ℕ}, StrictConcaveOn ℝ (Set.Icc 0 1) (Real.qaryEntropy q)
-- Init.Data.Int.Lemmas
Int.neg_zero : -0 = 0
-- Mathlib.Analysis.Calculus.ContDiff.Basic
/-- Iterated derivatives commute with left composition by continuous linear equivalences.  -/
ContinuousLinearEquiv.iteratedFDeriv_comp_left : ∀ {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} {G : Type u_4} [inst : NontriviallyNormedField 𝕜]
  [inst_1 : NormedAddCommGroup E] [inst_2 : NormedSpace 𝕜 E] [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F]
  [inst_5 : NormedAddCommGroup G] [inst_6 : NormedSpace 𝕜 G] {f : E → F} {x : E} (g : F ≃L[𝕜] G) {i : ℕ},
  iteratedFDeriv 𝕜 i (⇑g ∘ f) x = (↑g).compContinuousMultilinearMap (iteratedFDeriv 𝕜 i f x)
-- Lean.Elab.Do.Basic
Lean.Elab.Do.elabDoElems1 : Array Lean.DoElem → Lean.Elab.Do.DoElemCont → optParam Bool true → Lean.Elab.Do.DoElabM Lean.Expr
-- Mathlib.Order.Bounds.Basic
isLeast_union_iff : ∀ {α : Type u_1} [inst : Preorder α] {a : α} {s t : Set α},
  IsLeast (s ∪ t) a ↔ IsLeast s a ∧ a ∈ lowerBounds t ∨ a ∈ lowerBounds s ∧ IsLeast t a
-- Mathlib.Data.DFinsupp.Lex
DFinsupp.Lex.addRightMono : ∀ {ι : Type u_1} {α : ι → Type u_2} [inst : LinearOrder ι] [inst_1 : (i : ι) → AddMonoid (α i)]
  [inst_2 : (i : ι) → LinearOrder (α i)] [∀ (i : ι), AddRightStrictMono (α i)], AddRightMono (Lex (Π₀ (i : ι), α i))
-- Mathlib.MeasureTheory.VectorMeasure.Integral
MeasureTheory.VectorMeasure.Integrable.fun_finsetSum : ∀ {X : Type u_2} {E : Type u_4} {F : Type u_5} {mX : MeasurableSpace X} [inst : NormedAddCommGroup E]
  [inst_1 : NormedAddCommGroup F] {μ : MeasureTheory.VectorMeasure X F} {ι : Type u_8} (s : Finset ι) {f : ι → X → E},
  (∀ i ∈ s, μ.Integrable (f i)) → μ.Integrable fun x => ∑ i ∈ s, f i x
-- Mathlib.Order.Filter.Pointwise
Filter.NeBot.of_div_left : ∀ {α : Type u_2} [inst : Div α] {f g : Filter α}, (f / g).NeBot → f.NeBot
-- Mathlib.Combinatorics.Enumerative.Schroder
_private.Mathlib.Combinatorics.Enumerative.Schroder.0.Nat.largeSchroder.match_1.eq_1 : ∀ (motive : ℕ → Sort u_1) (h_1 : Unit → motive 0) (h_2 : (n : ℕ) → motive n.succ),
  (match 0 with
    | 0 => h_1 ()
    | n.succ => h_2 n) =
    h_1 ()
-- Lean.Meta.Tactic.Grind.Types
/-- The goal has been closed, and you can use `seq` to close the goal efficiently.
 -/
Lean.Meta.Grind.ActionResult.closed : List Lean.Meta.Grind.TGrind → Lean.Meta.Grind.ActionResult
-- Mathlib.CategoryTheory.Pi.Basic
CategoryTheory.Functor.pi'_obj : ∀ {I : Type w₀} {C : I → Type u₁} [inst : (i : I) → CategoryTheory.Category.{v₁, u₁} (C i)] {A : Type u₃}
  [inst_1 : CategoryTheory.Category.{v₃, u₃} A] (f : (i : I) → CategoryTheory.Functor A (C i)) (a : A) (i : I),
  (CategoryTheory.Functor.pi' f).obj a i = (f i).obj a
-- Mathlib.Topology.Category.LightProfinite.Sequence
/-- The continuous map from `ℕ∪{∞}` to `ℝ` sending `n` to `1/(n+1)` and `∞` to `0`.  -/
LightProfinite.natUnionInftyEmbedding : C(OnePoint ℕ, ℝ)
-- Mathlib.CategoryTheory.Limits.Cones
CategoryTheory.Limits.Cone.ext.congr_simp : ∀ {J : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} J] {C : Type u₃} [inst_1 : CategoryTheory.Category.{v₃, u₃} C]
  {F : CategoryTheory.Functor J C} {c c' : CategoryTheory.Limits.Cone F} (φ φ_1 : c.pt ≅ c'.pt) (e_φ : φ = φ_1)
  (w : ∀ (j : J), c.π.app j = CategoryTheory.CategoryStruct.comp φ.hom (c'.π.app j)),
  CategoryTheory.Limits.Cone.ext φ w = CategoryTheory.Limits.Cone.ext φ_1 ⋯
-- Mathlib.CategoryTheory.Abelian.NonPreadditive
/-- σ is a cokernel of Δ X.  -/
CategoryTheory.NonPreadditiveAbelian.isColimitσ : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    [inst_1 : CategoryTheory.NonPreadditiveAbelian C] →
      {X : C} →
        CategoryTheory.Limits.IsColimit
          (CategoryTheory.Limits.CokernelCofork.ofπ CategoryTheory.NonPreadditiveAbelian.σ ⋯)
-- Mathlib.Algebra.Divisibility.Units
IsRelPrime.of_mul_left_right : ∀ {α : Type u_1} [inst : CommMonoid α] {x y z : α}, IsRelPrime (x * y) z → IsRelPrime y z
-- Init.Data.List.Attach
List.pmap_map : ∀ {β : Type u_1} {γ : Type u_2} {α : Type u_3} {p : β → Prop} {g : (b : β) → p b → γ} {f : α → β} {l : List α}
  (H : ∀ a ∈ List.map f l, p a), List.pmap g (List.map f l) H = List.pmap (fun a h => g (f a) h) l ⋯
-- Mathlib.MeasureTheory.Measure.Decomposition.Lebesgue
MeasureTheory.Measure.measure_sub_singularPart : ∀ {α : Type u_1} {m : MeasurableSpace α} (μ ν : MeasureTheory.Measure α) [μ.HaveLebesgueDecomposition ν]
  [MeasureTheory.IsFiniteMeasure μ], μ - μ.singularPart ν = ν.withDensity (μ.rnDeriv ν)
-- Mathlib.FieldTheory.Galois.Abelian
instIsAbelianGalois : ∀ (K : Type u_1) [inst : Field K], IsAbelianGalois K K
-- Mathlib.Algebra.Group.Pointwise.Set.Basic
/-- **Alias** of the reverse direction of `Set.zero_notMem_sub_iff`. -/
Disjoint.zero_notMem_sub_set : ∀ {α : Type u_2} [inst : AddGroup α] {s t : Set α}, Disjoint s t → 0 ∉ s - t
-- Init.Grind.ToIntLemmas
Lean.Grind.ToInt.zero_eq : ∀ {α : Type u_1} {i : Lean.Grind.IntInterval} [inst : Lean.Grind.ToInt α i] [inst_1 : Zero α]
  [Lean.Grind.ToInt.Zero α i], ↑0 = 0
-- Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.NonUnital
NonUnitalClosedEmbeddingContinuousFunctionalCalculus.toNonUnitalContinuousFunctionalCalculus : ∀ {R : Type u_1} {A : Type u_2} {p : outParam (A → Prop)} {inst : CommSemiring R} {inst_1 : Nontrivial R}
  {inst_2 : StarRing R} {inst_3 : MetricSpace R} {inst_4 : IsTopologicalSemiring R} {inst_5 : ContinuousStar R}
  {inst_6 : NonUnitalRing A} {inst_7 : StarRing A} {inst_8 : TopologicalSpace A} {inst_9 : Module R A}
  {inst_10 : IsScalarTower R A A} {inst_11 : SMulCommClass R A A}
  [self : NonUnitalClosedEmbeddingContinuousFunctionalCalculus R A p], NonUnitalContinuousFunctionalCalculus R A p
-- Mathlib.SetTheory.Cardinal.Cofinality.Basic
Order.le_cof_iff : ∀ {α : Type u} [inst : Preorder α] {c : Cardinal.{u}}, c ≤ Order.cof α ↔ ∀ (s : Set α), IsCofinal s → c ≤ Cardinal.mk ↑s
-- Mathlib.Topology.Category.Stonean.Basic
Profinite.lift.congr_simp : ∀ {X Y : Profinite} {Z : Stonean} (e e_1 : Stonean.toProfinite.obj Z ⟶ Y),
  e = e_1 → ∀ (f f_1 : X ⟶ Y) (e_f : f = f_1) [inst : CategoryTheory.Epi f], Profinite.lift e f = Profinite.lift e_1 f_1
-- Mathlib.AlgebraicGeometry.OpenImmersion
AlgebraicGeometry.Scheme.Hom.appIso_inv_appLE : ∀ {X Y : AlgebraicGeometry.Scheme} (f : X ⟶ Y) [inst : AlgebraicGeometry.IsOpenImmersion f] {U V : X.Opens}
  (e : V ≤ (TopologicalSpace.Opens.map f.base).obj ((AlgebraicGeometry.Scheme.Hom.opensFunctor f).obj U)),
  CategoryTheory.CategoryStruct.comp (AlgebraicGeometry.Scheme.Hom.appIso f U).inv
      (AlgebraicGeometry.Scheme.Hom.appLE f ((AlgebraicGeometry.Scheme.Hom.opensFunctor f).obj U) V e) =
    X.presheaf.map (CategoryTheory.homOfLE ⋯).op
-- Mathlib.LinearAlgebra.QuadraticForm.Signature
sigPos_neg : ∀ {R : Type u_1} {M : Type u_2} [inst : AddCommGroup M] [inst_1 : CommRing R] [inst_2 : LinearOrder R]
  [inst_3 : Module R M] {Q : QuadraticForm R M}, sigPos (-Q) = sigNeg Q
-- Mathlib.Order.Interval.Finset.Basic
/-- **Alias** of the reverse direction of `Finset.Ioi_eq_empty`. -/
IsMax.finsetIoi_eq : ∀ {α : Type u_2} {a : α} [inst : Preorder α] [inst_1 : LocallyFiniteOrderTop α], IsMax a → Finset.Ioi a = ∅
-- Std.Data.DTreeMap.Raw.Basic
/-- Tries to retrieve the key-value pair with the largest key that is less than or equal to the
given key, panicking if no such pair exists.
 -/
Std.DTreeMap.Raw.getEntryLE! : {α : Type u} →
  {β : α → Type v} →
    {cmp : α → α → Ordering} → [Inhabited ((a : α) × β a)] → Std.DTreeMap.Raw α β cmp → α → (a : α) × β a
-- Mathlib.Algebra.Module.Equiv.Basic
AddEquiv.toIntLinearEquiv_toAddEquiv : ∀ {M : Type u_5} {M₂ : Type u_7} [inst : AddCommGroup M] [inst_1 : AddCommGroup M₂] {modM : Module ℤ M}
  {modM₂ : Module ℤ M₂} (e : M ≃+ M₂), ↑e.toIntLinearEquiv = e
-- Mathlib.RingTheory.Spectrum.Prime.Topology
PrimeSpectrum.isClosed_image_of_stableUnderSpecialization : ∀ {R : Type u_1} {S : Type u_2} [inst : CommSemiring R] [inst_1 : CommSemiring S] (f : R →+* S)
  (Z : Set (PrimeSpectrum S)),
  IsClosed Z → StableUnderSpecialization (PrimeSpectrum.comap f '' Z) → IsClosed (PrimeSpectrum.comap f '' Z)
-- Std.Data.ExtDTreeMap.Lemmas
Std.ExtDTreeMap.getKey?_alter_self : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t : Std.ExtDTreeMap α β cmp} [inst : Std.TransCmp cmp]
  [inst_1 : Std.LawfulEqCmp cmp] {k : α} {f : Option (β k) → Option (β k)},
  (t.alter k f).getKey? k = if (f (t.get? k)).isSome = true then some k else none
-- Mathlib.Topology.Compactness.Compact
isCompact_singleton : ∀ {X : Type u} [inst : TopologicalSpace X] {x : X}, IsCompact {x}
-- Mathlib.Topology.Algebra.InfiniteSum.Module
/-- Applying a continuous linear map commutes with taking an (infinite) sum.  -/
ContinuousLinearMap.hasSum : ∀ {ι : Type u_5} {R : Type u_7} {R₂ : Type u_8} {M : Type u_9} {M₂ : Type u_10} [inst : Semiring R]
  [inst_1 : Semiring R₂] [inst_2 : AddCommMonoid M] [inst_3 : Module R M] [inst_4 : AddCommMonoid M₂]
  [inst_5 : Module R₂ M₂] [inst_6 : TopologicalSpace M] [inst_7 : TopologicalSpace M₂] {σ : R →+* R₂}
  {L : SummationFilter ι} {f : ι → M} (φ : M →SL[σ] M₂) {x : M}, HasSum f x L → HasSum (fun b => φ (f b)) (φ x) L
-- Mathlib.Logic.Equiv.Prod
Equiv.sigmaProdDistrib_apply : ∀ {ι : Type u_9} (α : ι → Type u_10) (β : Type u_11) (p : ((i : ι) × α i) × β),
  (Equiv.sigmaProdDistrib α β) p = ⟨p.1.fst, (p.1.snd, p.2)⟩
-- Mathlib.RingTheory.Ideal.KrullsHeightTheorem
/-- In a Noetherian ring, the height of a principal ideal spanned by a non-unit non-zero-divisor
is one.  -/
Ideal.height_span_singleton_eq_one_of_mem_nonZeroDivisors : ∀ {R : Type u_1} [inst : CommRing R] [IsNoetherianRing R] {x : R},
  x ∈ nonZeroDivisors R → ¬IsUnit x → (Ideal.span {x}).height = 1
-- Mathlib.Data.Set.Countable
Set.not_countable_univ : ∀ {α : Type u} [Uncountable α], ¬Set.univ.Countable
-- Mathlib.MeasureTheory.Constructions.Pi
MeasureTheory.volume_measurePreserving_arrowProdEquivProdArrow : ∀ (α : Type u_4) (β : Type u_5) (γ : Type u_6) [inst : MeasureTheory.MeasureSpace α]
  [inst_1 : MeasureTheory.MeasureSpace β] [inst_2 : Fintype γ] [MeasureTheory.SigmaFinite MeasureTheory.volume]
  [MeasureTheory.SigmaFinite MeasureTheory.volume],
  MeasureTheory.MeasurePreserving (⇑(MeasurableEquiv.arrowProdEquivProdArrow α β γ)) MeasureTheory.volume
    MeasureTheory.volume
-- Mathlib.Analysis.Calculus.VectorField
/-- Product rule for Lie Brackets: given two vector fields `V W : E → E` and a function `f : E → 𝕜`,
we have `[V, f • W] = (df V) • W + f • [V, W]`
 -/
VectorField.lieBracketWithin_smul_right : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {V W : E → E} {s : Set E} {x : E} {f : E → 𝕜},
  DifferentiableWithinAt 𝕜 f s x →
    DifferentiableWithinAt 𝕜 W s x →
      UniqueDiffWithinAt 𝕜 s x →
        VectorField.lieBracketWithin 𝕜 V (fun y => f y • W y) s x =
          (fderivWithin 𝕜 f s x) (V x) • W x + f x • VectorField.lieBracketWithin 𝕜 V W s x
-- Mathlib.AlgebraicTopology.SimplicialObject.DeltaZeroIter
CategoryTheory.SimplicialObject.σ.eq_1 : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] (X : CategoryTheory.SimplicialObject C) {n : ℕ}
  (i : Fin (n + 1)), X.σ i = X.map (SimplexCategory.σ i).op
-- Batteries.CodeAction.Match
/-- From a constructor-name e.g. `Option.some` construct the corresponding match pattern, e.g.
`.some val`. We implement special cases for `Nat` and `List`, `Option` and `Bool` to e.g.
produce `n + 1` instead of `Nat.succ n`.  -/
Batteries.CodeAction.patternFromConstructor : Lean.Name → Lean.Environment → String → Bool → Bool → Option String
-- Mathlib.MeasureTheory.Constructions.BorelSpace.Real
measurable_coe_real_ereal : Measurable Real.toEReal
-- Mathlib.CategoryTheory.InducedCategory
CategoryTheory.InducedCategory.Hom.ext : ∀ {C : Type u₁} {D : Type u₂} {inst : CategoryTheory.Category.{v, u₂} D} {F : C → D}
  {X Y : CategoryTheory.InducedCategory D F} {x y : X.Hom Y}, x.hom = y.hom → x = y
-- Mathlib.Order.Interval.Set.Basic
Set.Iio_insert : ∀ {α : Type u_1} [inst : PartialOrder α] {a : α}, insert a (Set.Iio a) = Set.Iic a
-- Mathlib.Logic.Equiv.Nat
/-- An equivalence between `ℤ` and `ℕ`, through `ℤ ≃ ℕ ⊕ ℕ` and `ℕ ⊕ ℕ ≃ ℕ`.
 -/
Equiv.intEquivNat : ℤ ≃ ℕ
-- Mathlib.Topology.Homotopy.HomotopyGroup
genLoopEquivOfUnique.eq_1 : ∀ {X : Type u_2} [inst : TopologicalSpace X] {x : X} (N : Type u_3) [inst_1 : Unique N],
  genLoopEquivOfUnique N =
    { toFun := fun p => { toFun := fun t => p fun x => t, continuous_toFun := ⋯, source' := ⋯, target' := ⋯ },
      invFun := fun p => ⟨{ toFun := fun c => p (c default), continuous_toFun := ⋯ }, ⋯⟩, left_inv := ⋯,
      right_inv := ⋯ }
-- Mathlib.Data.Fintype.Basic
PLift.up.congr_simp : ∀ {α : Sort u} (down down_1 : α), down = down_1 → { down := down } = { down := down_1 }
-- Mathlib.Data.Matrix.Basis
Matrix.singleAddMonoidHom_apply : ∀ {m : Type u_2} {n : Type u_3} {α : Type u_7} [inst : DecidableEq m] [inst_1 : DecidableEq n]
  [inst_2 : AddCommMonoid α] (i : m) (j : n) (a : α), (Matrix.singleAddMonoidHom i j) a = Matrix.single i j a
-- Mathlib.GroupTheory.GroupExtension.Basic
GroupExtension.Section.exists_eq_mul_inl : ∀ {N : Type u_1} {G : Type u_2} [inst : Group N] [inst_1 : Group G] {E : Type u_3} [inst_2 : Group E]
  {S : GroupExtension N E G} (σ σ' : S.Section) (g : G), ∃ n, σ g = σ' g * S.inl n
-- Lean.Meta.Tactic.Grind.Injective
_private.Lean.Meta.Tactic.Grind.Injective.0.Lean.Meta.Grind.getSymbols.collectFnNames : Lean.Expr → Lean.MetaM Lean.NameSet
-- Mathlib.RingTheory.Jacobson.Radical
/-- The Jacobson radical of an `R`-module `M` is the infimum of all maximal submodules in `M`.  -/
Module.jacobson : (R : Type u_1) → (M : Type u_3) → [inst : Ring R] → [inst_1 : AddCommGroup M] → [inst_2 : Module R M] → Submodule R M
-- Mathlib.Order.OrdContinuous
RightOrdContinuous.eq_1 : ∀ {α : Type u} {β : Type v} [inst : Preorder α] [inst_1 : Preorder β] (f : α → β),
  RightOrdContinuous f = ∀ ⦃s : Set α⦄ ⦃x : α⦄, s.Nonempty → IsGLB s x → IsGLB (f '' s) (f x)
-- Mathlib.AlgebraicGeometry.Sites.Representability
AlgebraicGeometry.Scheme.LocalRepresentability.yonedaGluedToSheaf_app_comp : ∀ {F : CategoryTheory.Sheaf AlgebraicGeometry.Scheme.zariskiTopology (Type u)} {ι : Type u}
  {X : ι → AlgebraicGeometry.Scheme} {f : (i : ι) → CategoryTheory.yoneda.obj (X i) ⟶ F.obj}
  (hf : ∀ (i : ι), AlgebraicGeometry.IsOpenImmersion.presheaf (f i)) {V U : AlgebraicGeometry.Scheme} (γ : V ⟶ U)
  (α : U ⟶ (AlgebraicGeometry.Scheme.LocalRepresentability.glueData hf).glued),
  (CategoryTheory.ConcreteCategory.hom
        ((AlgebraicGeometry.Scheme.LocalRepresentability.yonedaGluedToSheaf hf).hom.app (Opposite.op V)))
      (CategoryTheory.CategoryStruct.comp γ α) =
    (CategoryTheory.ConcreteCategory.hom (F.obj.map γ.op))
      ((CategoryTheory.ConcreteCategory.hom
          ((AlgebraicGeometry.Scheme.LocalRepresentability.yonedaGluedToSheaf hf).hom.app (Opposite.op U)))
        α)
-- Mathlib.ModelTheory.Syntax
/-- The representation of a constant symbol as a term.  -/
FirstOrder.Language.Constants.term : {L : FirstOrder.Language} → {α : Type u'} → L.Constants → L.Term α
-- Mathlib.Combinatorics.SimpleGraph.Paths
SimpleGraph.Walk.IsCycle.count_support : ∀ {V : Type u} {G : SimpleGraph V} {v : V} [inst : DecidableEq V] {c : G.Walk v v},
  c.IsCycle → List.count v c.support = 2
-- Mathlib.MeasureTheory.Function.ConditionalExpectation.CondexpL1
MeasureTheory.condExpInd_empty : ∀ {α : Type u_1} {G : Type u_4} [inst : NormedAddCommGroup G] {m m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α}
  [inst_1 : NormedSpace ℝ G] {hm : m ≤ m0} [inst_2 : MeasureTheory.SigmaFinite (μ.trim hm)],
  MeasureTheory.condExpInd G hm μ ∅ = 0
-- Init.Data.List.Basic
/-- The head of a list is a member: `a ∈ a :: as`.  -/
List.Mem.head : ∀ {α : Type u} {a : α} (as : List α), List.Mem a (a :: as)
-- Mathlib.LinearAlgebra.CliffordAlgebra.SpinGroup
pinGroup.instStarMulSubtypeCliffordAlgebraMemSubmonoid : {R : Type u_1} →
  [inst : CommRing R] →
    {M : Type u_2} → [inst_1 : AddCommGroup M] → [inst_2 : Module R M] → {Q : QuadraticForm R M} → StarMul ↥(pinGroup Q)
-- Mathlib.Data.List.MinMax
List.minimum_le_coe_iff : ∀ {α : Type u_1} [inst : LinearOrder α] {l : List α} {a : α}, l.minimum ≤ ↑a ↔ ∃ b ∈ l, b ≤ a
-- Mathlib.CategoryTheory.Adjunction.Opposites
/-- If `F` is adjoint to `G.leftOp` then `G` is adjoint to `F.leftOp`.  -/
CategoryTheory.Adjunction.leftOp : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    {D : Type u₂} →
      [inst_1 : CategoryTheory.Category.{v₂, u₂} D] →
        {F : CategoryTheory.Functor C Dᵒᵖ} → {G : CategoryTheory.Functor D Cᵒᵖ} → (F ⊣ G.leftOp) → (G ⊣ F.leftOp)
-- Lean.Meta.LazyDiscrTree
/-- Check if a private declaration is accessible from the current environment.
- Local private declarations (defined in current module) are always accessible.
- Imported private declarations are accessible only in the module system with `import all`.
 -/
_private.Lean.Meta.LazyDiscrTree.0.Lean.Meta.LazyDiscrTree.isAccessiblePrivateName : Lean.Environment → Lean.Name → Bool
-- Init.Data.List.ControlImpl
List.flatMapM.match_1.congr_eq_1 : ∀ {α : Type u_1} {β : Type u_2} (motive : List α → List (List β) → Sort u_3) (x : List α) (x_1 : List (List β))
  (h_1 : (bs : List (List β)) → motive [] bs)
  (h_2 : (a : α) → (as : List α) → (bs : List (List β)) → motive (a :: as) bs) (bs : List (List β)),
  x = [] →
    x_1 = bs →
      (match x, x_1 with
        | [], bs => h_1 bs
        | a :: as, bs => h_2 a as bs) ≍
        h_1 bs
-- Mathlib.CategoryTheory.Square
CategoryTheory.Square.Hom.comm₂₄ : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {sq₁ sq₂ : CategoryTheory.Square C} (self : sq₁.Hom sq₂),
  CategoryTheory.CategoryStruct.comp sq₁.f₂₄ self.τ₄ = CategoryTheory.CategoryStruct.comp self.τ₂ sq₂.f₂₄
-- Mathlib.CategoryTheory.Monoidal.DayConvolution
/-- In a `LawfulDayConvolutionMonoidalCategoryStruct`, `ι.obj ((d ⊗ d') ⊗ d'')`
is a (triple) Day convolution of `(ι C V).obj d`, `(ι C V).obj d'` and
`(ι C V).obj d''`.  -/
CategoryTheory.MonoidalCategory.LawfulDayConvolutionMonoidalCategoryStruct.convolution₂' : (C : Type u₁) →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    (V : Type u₂) →
      [inst_1 : CategoryTheory.Category.{v₂, u₂} V] →
        [inst_2 : CategoryTheory.MonoidalCategory C] →
          [inst_3 : CategoryTheory.MonoidalCategory V] →
            (D : Type u₃) →
              [inst_4 : CategoryTheory.Category.{v₃, u₃} D] →
                [inst_5 : CategoryTheory.MonoidalCategoryStruct D] →
                  [inst_6 : CategoryTheory.MonoidalCategory.LawfulDayConvolutionMonoidalCategoryStruct C V D] →
                    (d d' d'' : D) →
                      CategoryTheory.MonoidalCategory.DayConvolution
                        (CategoryTheory.MonoidalCategory.DayConvolution.convolution
                          ((CategoryTheory.MonoidalCategory.LawfulDayConvolutionMonoidalCategoryStruct.ι C V D).obj d)
                          ((CategoryTheory.MonoidalCategory.LawfulDayConvolutionMonoidalCategoryStruct.ι C V D).obj d'))
                        ((CategoryTheory.MonoidalCategory.LawfulDayConvolutionMonoidalCategoryStruct.ι C V D).obj d'')