mathlib-initiative/mathlib-types huggingface dataset:
-- Lean.Meta.Tactic.Subst
Lean.Meta.subst? : Lean.MVarId → Lean.FVarId → Lean.MetaM (Option Lean.MVarId)
-- Mathlib.ModelTheory.Basic
FirstOrder.Language.Equiv.refl.eq_1 : ∀ (L : FirstOrder.Language) (M : Type w) [inst : L.Structure M],
  FirstOrder.Language.Equiv.refl L M = { toEquiv := Equiv.refl M, map_fun' := ⋯, map_rel' := ⋯ }
-- Mathlib.RingTheory.Valuation.ValuativeRel.Basic
ValuativeRel.instTransVle : {R : Type u_1} →
  [inst : Semiring R] → [inst_1 : ValuativeRel R] → Trans ValuativeRel.vle ValuativeRel.vle ValuativeRel.vle
-- Mathlib.Order.UpperLower.Fibration
/-- **Alias** of `Relation.Fibration.isLowerSet_image`. -/
IsLowerSet.image_fibration : ∀ {α : Type u_1} {β : Type u_2} {f : α → β} [inst : LE α] [inst_1 : LE β],
  Relation.Fibration (fun x1 x2 => x1 ≤ x2) (fun x1 x2 => x1 ≤ x2) f → ∀ {s : Set α}, IsLowerSet s → IsLowerSet (f '' s)
-- Mathlib.Data.Finsupp.Basic
Finsupp.sumElim_inl : ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} [inst : Zero γ] (f : α →₀ γ) (g : β →₀ γ) (x : α),
  (f.sumElim g) (Sum.inl x) = f x
-- Mathlib.CategoryTheory.Triangulated.Basic
/-- the first object of a triangle  -/
CategoryTheory.Pretriangulated.Triangle.obj₁ : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    [inst_1 : CategoryTheory.HasShift C ℤ] → CategoryTheory.Pretriangulated.Triangle C → C
-- Init.Data.BitVec.Lemmas
BitVec.neg_eq_zero_iff : ∀ {w : ℕ} {x : BitVec w}, -x = 0#w ↔ x = 0#w
-- Mathlib.Topology.MetricSpace.HausdorffDistance
/-- **Alias** of `Metric.hausdorffEDist_le_ediam`.

---

The Hausdorff distance is controlled by the diameter of the union.  -/
EMetric.hausdorffEdist_le_ediam : ∀ {α : Type u} [inst : PseudoEMetricSpace α] {s t : Set α},
  s.Nonempty → t.Nonempty → Metric.hausdorffEDist s t ≤ Metric.ediam (s ∪ t)
-- Std.Data.ExtDTreeMap.Basic
/-- Given a proof that such a mapping exists, retrieves the key-value pair with the smallest key that is
greater than or equal to the given key.
 -/
Std.ExtDTreeMap.Const.getEntryGE : {α : Type u} →
  {cmp : α → α → Ordering} →
    {β : Type v} →
      [inst : Std.TransCmp cmp] →
        (t : Std.ExtDTreeMap α (fun x => β) cmp) → (k : α) → (∃ a ∈ t, (cmp a k).isGE = true) → α × β
-- Mathlib.Condensed.Light.Sequence
_private.Mathlib.Condensed.Light.Sequence.0.InternalProjectivityProof.coverToFun_apply : ∀ {S : Type u_4} {T : Type u_5} {X : Type u_6} {Y : Type u_7} (i : Y → T) (π : T → S × Option X)
  (t : T ⊕ { xy // π (i xy.1) = π (i xy.2) }),
  InternalProjectivityProof.coverToFun✝ i π t =
    Sum.elim (fun t => ⟨(t, t), ⋯⟩) (fun xy => ⟨(i (↑xy).1, i (↑xy).2), ⋯⟩) t
-- Mathlib.Probability.Kernel.Disintegration.StandardBorel
ProbabilityTheory.Kernel.borelMarkovFromReal_apply : ∀ {α : Type u_1} {mα : MeasurableSpace α} (Ω : Type u_5) [inst : Nonempty Ω] [inst_1 : MeasurableSpace Ω]
  [inst_2 : StandardBorelSpace Ω] (η : ProbabilityTheory.Kernel α ℝ) (a : α),
  (ProbabilityTheory.Kernel.borelMarkovFromReal Ω η) a =
    if (η a) (Set.range (MeasureTheory.embeddingReal Ω))ᶜ = 0 then
      MeasureTheory.Measure.comap (MeasureTheory.embeddingReal Ω) (η a)
    else MeasureTheory.Measure.comap (MeasureTheory.embeddingReal Ω) (MeasureTheory.Measure.dirac (Exists.choose ⋯))
-- Mathlib.Data.Finset.Max
Finset.notMem_of_max_lt_coe : ∀ {α : Type u_2} [inst : LinearOrder α] {a : α} {s : Finset α}, s.max < ↑a → a ∉ s
-- Mathlib.Algebra.Order.Module.Defs
strictMono_smul_right_of_pos : ∀ {α : Type u_1} {β : Type u_2} {b : β} [inst : SMul α β] [inst_1 : Preorder α] [inst_2 : Preorder β] [inst_3 : Zero β]
  [SMulPosStrictMono α β], 0 < b → StrictMono fun x => x • b
-- Mathlib.LinearAlgebra.AffineSpace.Simplex.Centroid
/-- Reverse version of `faceOppositeCentroid_vsub_centroid_eq_smul_vsub`  -/
Affine.Simplex.centroid_vsub_faceOppositeCentroid_eq_smul_vsub : ∀ {k : Type u_1} {V : Type u_2} {P : Type u_3} [inst : DivisionRing k] [inst_1 : AddCommGroup V] [inst_2 : Module k V]
  [inst_3 : AddTorsor V P] {n : ℕ} [inst_4 : NeZero n] [CharZero k] (s : Affine.Simplex k P n) (i : Fin (n + 1)),
  s.centroid -ᵥ s.faceOppositeCentroid i = (↑n)⁻¹ • (s.points i -ᵥ s.centroid)
-- Mathlib.CategoryTheory.Limits.Presheaf
/-- If `F : C ⥤ Type w` and `C` is locally `w`-small, then `F` identifies to the colimit
of `(CategoryOfElements.π F).op ⋙ shrinkYoneda.{w}.flip`.  -/
CategoryTheory.Functor.Elements.isColimitCoconeπOpCompShrinkYonedaFlip : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    [inst_1 : CategoryTheory.LocallySmall.{w, v₁, u₁} C] →
      (F : CategoryTheory.Functor C (Type w)) →
        CategoryTheory.Limits.IsColimit (CategoryTheory.Functor.Elements.coconeπOpCompShrinkYonedaFlip F)
-- Mathlib.ModelTheory.Semantics
FirstOrder.Language.BoundedFormula.Realize.eq_4 : ∀ {L : FirstOrder.Language} {M : Type w} [inst : L.Structure M] {α : Type u'} (x : ℕ) (x_1 : α → M) (x_2 : Fin x → M)
  (f₁ f₂ : L.BoundedFormula α x), (f₁.imp f₂).Realize x_1 x_2 = (f₁.Realize x_1 x_2 → f₂.Realize x_1 x_2)
-- Mathlib.Algebra.Lie.Weights.Killing
LieAlgebra.restrict_killingForm : ∀ (R : Type u_1) (L : Type u_3) [inst : CommRing R] [inst_1 : LieRing L] [inst_2 : LieAlgebra R L]
  (H : LieSubalgebra R L), (killingForm R L).restrict H.toSubmodule = LieModule.traceForm R (↥H) L
-- Mathlib.CategoryTheory.ComposableArrows.Basic
CategoryTheory.Functor.mapComposableArrows_obj_obj : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] {D : Type u_2}
  [inst_1 : CategoryTheory.Category.{v_2, u_2} D] (G : CategoryTheory.Functor C D) (n : ℕ)
  (F : CategoryTheory.Functor (Fin (n + 1)) C) (X : Fin (n + 1)),
  ((G.mapComposableArrows n).obj F).obj X = G.obj (F.obj X)
-- Mathlib.Topology.Algebra.Constructions
AddUnits.isInducing_embedProduct : ∀ {M : Type u_1} [inst : TopologicalSpace M] [inst_1 : AddMonoid M], Topology.IsInducing ⇑(AddUnits.embedProduct M)
-- Mathlib.Data.ENat.Basic
ENat.sub_ne_top_iff : ∀ {a b : ℕ∞}, a - b ≠ ⊤ ↔ a ≠ ⊤ ∨ b = ⊤
-- Mathlib.Topology.MetricSpace.UniformConvergence
/-- The natural `EMetric` structure on `α →ᵤ β` given by `edist f g = ⨆ x, edist (f x) (g x)`.  -/
UniformFun.instPseudoEMetricSpace : {α : Type u_1} → {β : Type u_2} → [PseudoEMetricSpace β] → PseudoEMetricSpace (UniformFun α β)
-- Mathlib.CategoryTheory.Limits.Weighted.HasWeightedLimit
CategoryTheory.Functor.isLimitWeightedLimCone_fac : ∀ {J : Type u} [inst : CategoryTheory.Category.{v, u} J] {C : Type u'} [inst_1 : CategoryTheory.Category.{v', u'} C]
  (W : CategoryTheory.Functor J (Type w)) (F : CategoryTheory.Functor J C)
  [inst_2 : CategoryTheory.Limits.HasWeightedLimit W F] {Z : C} (π : ⦃j : J⦄ → W.obj j → (Z ⟶ F.obj j))
  (hπ :
    ∀ ⦃j₁ j₂ : J⦄ (x : W.obj j₁) (f : j₁ ⟶ j₂),
      CategoryTheory.CategoryStruct.comp (π x) (F.map f) = π ((CategoryTheory.ConcreteCategory.hom (W.map f)) x))
  ⦃j : J⦄ (x : W.obj j),
  CategoryTheory.CategoryStruct.comp ((W.isLimitWeightedLimCone F).lift π hπ) (W.weightedLimObjObjπ F x) = π x
-- Mathlib.LinearAlgebra.Complex.Module
Complex.instIsCentralScalarOfReal : ∀ {R : Type u_1} [inst : SMul R ℝ] [inst_1 : SMul Rᵐᵒᵖ ℝ] [IsCentralScalar R ℝ], IsCentralScalar R ℂ
-- Init.Data.Range.Polymorphic.UInt
UInt16.rxiHasSize_eq_toBitVec : ∀ {lo : BitVec 16}, Std.Rxi.HasSize.size { toBitVec := lo } = Std.Rxi.HasSize.size lo
-- Mathlib.CategoryTheory.Sites.DenseSubsite.Basic
CategoryTheory.Functor.IsCoverDense.restrictHomEquivHom.congr_simp : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] {D : Type u_2}
  [inst_1 : CategoryTheory.Category.{v_2, u_2} D] {K : CategoryTheory.GrothendieckTopology D} {A : Type u_4}
  [inst_2 : CategoryTheory.Category.{v_4, u_4} A] {G : CategoryTheory.Functor C D} [inst_3 : G.IsCoverDense K]
  [inst_4 : G.IsLocallyFull K] {ℱ : CategoryTheory.Functor Dᵒᵖ A} {ℱ' : CategoryTheory.Sheaf K A},
  CategoryTheory.Functor.IsCoverDense.restrictHomEquivHom = CategoryTheory.Functor.IsCoverDense.restrictHomEquivHom
-- Lean.Elab.MutualDef
_private.Lean.Elab.MutualDef.0.Lean.Elab.Term.MutualClosure.mkClosureForAux : Array Lean.FVarId → StateRefT' IO.RealWorld Lean.Elab.Term.MutualClosure.ClosureState Lean.Elab.TermElabM Unit
-- Mathlib.Algebra.BigOperators.Pi
Finset.sum_apply : ∀ {ι : Type u_1} {α : Type u_7} {M : α → Type u_8} [inst : (a : α) → AddCommMonoid (M a)] (a : α) (s : Finset ι)
  (g : ι → (a : α) → M a), (∑ c ∈ s, g c) a = ∑ c ∈ s, g c a
-- Std.Data.ExtDTreeMap.Basic
/-- Tries to retrieve the key-value pair with the largest key that is less than or equal to the
given key, returning `none` if no such pair exists.
 -/
Std.ExtDTreeMap.Const.getEntryLE? : {α : Type u} →
  {cmp : α → α → Ordering} → {β : Type v} → [Std.TransCmp cmp] → Std.ExtDTreeMap α (fun x => β) cmp → α → Option (α × β)
-- Mathlib.GroupTheory.GroupExtension.Defs
/-- See Note [custom simps projection].  -/
GroupExtension.Equiv.Simps.symm_apply : {N : Type u_1} →
  {E : Type u_2} →
    {G : Type u_3} →
      [inst : Group N] →
        [inst_1 : Group E] →
          [inst_2 : Group G] →
            {S : GroupExtension N E G} →
              {E' : Type u_4} → [inst_3 : Group E'] → {S' : GroupExtension N E' G} → S.Equiv S' → E' → E
-- Std.Data.DHashMap.RawLemmas
Std.DHashMap.Raw.get?_eq_some_getD : ∀ {α : Type u} {β : α → Type v} {m : Std.DHashMap.Raw α β} [inst : BEq α] [inst_1 : Hashable α] [inst_2 : LawfulBEq α],
  m.WF → ∀ {a : α} {fallback : β a}, a ∈ m → m.get? a = some (m.getD a fallback)
-- Std.Data.ExtTreeMap.Basic
/-- Tries to retrieve the largest key in the tree map, returning `none` if the map is empty.
 -/
Std.ExtTreeMap.maxKey? : {α : Type u} → {β : Type v} → {cmp : α → α → Ordering} → [Std.TransCmp cmp] → Std.ExtTreeMap α β cmp → Option α
-- Std.Data.HashSet.Basic
Std.HashSet.instInsert : {α : Type u} → {x : BEq α} → {x_1 : Hashable α} → Insert α (Std.HashSet α)
-- Std.Time.Zoned.RecurringRule
Std.Time.TimeZone.RecurringRule.mk : String → Std.Time.TimeZone.Offset → Option Std.Time.TimeZone.DaylightSavingRule → Std.Time.TimeZone.RecurringRule
-- Std.Data.DHashMap.Internal.Raw
Std.DHashMap.Internal.Raw.erase_eq : ∀ {α : Type u} {β : α → Type v} [inst : BEq α] [inst_1 : Hashable α] {m : Std.DHashMap.Raw α β} (h : m.WF) {a : α},
  m.erase a = ↑(Std.DHashMap.Internal.Raw₀.erase ⟨m, ⋯⟩ a)
-- Mathlib.FieldTheory.PurelyInseparable.Basic
Subalgebra.mem_perfectClosure_iff : ∀ {R : Type u_1} {A : Type u_2} [inst : CommSemiring R] [inst_1 : CommSemiring A] [inst_2 : Algebra R A] {p : ℕ}
  [inst_3 : ExpChar A p] {x : A}, x ∈ Subalgebra.perfectClosure R A p ↔ ∃ n, x ^ p ^ n ∈ (algebraMap R A).rangeS
-- Mathlib.Probability.Independence.Basic
ProbabilityTheory.IndepFun.comp₀ : ∀ {Ω : Type u_1} {β : Type u_6} {β' : Type u_7} {γ : Type u_8} {γ' : Type u_9} {_mΩ : MeasurableSpace Ω}
  {μ : MeasureTheory.Measure Ω} {f : Ω → β} {g : Ω → β'} {_mβ : MeasurableSpace β} {_mβ' : MeasurableSpace β'}
  {_mγ : MeasurableSpace γ} {_mγ' : MeasurableSpace γ'} {φ : β → γ} {ψ : β' → γ'},
  ProbabilityTheory.IndepFun f g μ →
    AEMeasurable f μ →
      AEMeasurable g μ →
        AEMeasurable φ (MeasureTheory.Measure.map f μ) →
          AEMeasurable ψ (MeasureTheory.Measure.map g μ) → ProbabilityTheory.IndepFun (φ ∘ f) (ψ ∘ g) μ
-- Mathlib.LinearAlgebra.RootSystem.BaseChange
RootPairing.restrictScalars'.congr_simp : ∀ {ι : Type u_1} {L : Type u_2} {M : Type u_3} {N : Type u_4} [inst : Field L] [inst_1 : AddCommGroup M]
  [inst_2 : AddCommGroup N] [inst_3 : Module L M] [inst_4 : Module L N] (P : RootPairing ι L M N) (K : Type u_5)
  [inst_5 : Field K] [inst_6 : Algebra K L] [inst_7 : Module K M] [inst_8 : Module K N] [inst_9 : IsScalarTower K L M]
  [inst_10 : IsScalarTower K L N] [inst_11 : P.IsBalanced] [inst_12 : P.IsValuedIn K],
  P.restrictScalars' K = P.restrictScalars' K
-- Mathlib.AlgebraicTopology.SimplexCategory.Augmented.Basic
AugmentedSimplexCategory.equivAugmentedSimplicialObject_counitIso_inv_app_left_app : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] (X : CategoryTheory.SimplicialObject.Augmented C)
  (X_1 : SimplexCategoryᵒᵖ),
  (AugmentedSimplexCategory.equivAugmentedSimplicialObject.counitIso.inv.app X).left.app X_1 =
    CategoryTheory.CategoryStruct.comp
      (CategoryTheory.CategoryStruct.id
        (match CategoryTheory.WithTerminal.incl.obj X_1 with
        | CategoryTheory.WithTerminal.of x => X.left.obj x
        | CategoryTheory.WithTerminal.star => X.right))
      (match CategoryTheory.WithTerminal.incl.obj X_1,
        match
          Opposite.unop
            (match CategoryTheory.WithTerminal.incl.obj X_1 with
            | CategoryTheory.WithTerminal.of x => Opposite.op (CategoryTheory.WithInitial.of (Opposite.unop x))
            | CategoryTheory.WithTerminal.star => Opposite.op CategoryTheory.WithInitial.star) with
        | CategoryTheory.WithInitial.of x => CategoryTheory.WithTerminal.of (Opposite.op x)
        | CategoryTheory.WithInitial.star => CategoryTheory.WithTerminal.star,
        (match CategoryTheory.WithTerminal.incl.obj X_1 with
          | CategoryTheory.WithTerminal.of x => CategoryTheory.Iso.refl (CategoryTheory.WithTerminal.of x)
          | CategoryTheory.WithTerminal.star => CategoryTheory.Iso.refl CategoryTheory.WithTerminal.star).inv with
      | CategoryTheory.WithTerminal.of a, CategoryTheory.WithTerminal.of a_1, f =>
        X.left.map (CategoryTheory.WithTerminal.down f)
      | CategoryTheory.WithTerminal.of x, CategoryTheory.WithTerminal.star, x_1 => X.hom.app x
      | CategoryTheory.WithTerminal.star, CategoryTheory.WithTerminal.star, x =>
        CategoryTheory.CategoryStruct.id X.right)
-- Mathlib.Algebra.TrivSqZeroExt.Basic
/-- The canonical `R`-linear projection `TrivSqZeroExt R M → M`.  -/
TrivSqZeroExt.sndHom : (R : Type u) →
  (M : Type v) → [inst : Semiring R] → [inst_1 : AddCommMonoid M] → [inst_2 : Module R M] → TrivSqZeroExt R M →ₗ[R] M
-- Lean.Meta.Tactic.Grind.ExtAttr
Lean.Meta.Grind.validateExtAttr : Lean.Name → Lean.CoreM Unit
-- Mathlib.Tactic.ByContra
_private.Mathlib.Tactic.ByContra.0.Mathlib.Tactic.ByContra.tacticTry_push_neg_at__ : Lean.ParserDescr
-- Mathlib.Data.Fintype.Order
Finite.ciInf_mono : ∀ {α : Type u_1} {ι : Type u_2} [Finite ι] [inst : ConditionallyCompleteLattice α] {f g : ι → α},
  (∀ (x : ι), f x ≤ g x) → iInf f ≤ iInf g
-- Mathlib.Algebra.Order.Interval.Set.Group
Set.sub_mem_Icc_iff_left : ∀ {α : Type u_1} [inst : AddCommGroup α] [inst_1 : PartialOrder α] [IsOrderedAddMonoid α] {a b c d : α},
  a - b ∈ Set.Icc c d ↔ a ∈ Set.Icc (c + b) (d + b)
-- Mathlib.MeasureTheory.VectorMeasure.Decomposition.Jordan
MeasureTheory.JordanDecomposition.neg_negPart : ∀ {α : Type u_1} [inst : MeasurableSpace α] (j : MeasureTheory.JordanDecomposition α), (-j).negPart = j.posPart
-- Mathlib.Topology.VectorBundle.Constructions
Bundle.Trivial.trivialization.coordChangeL : ∀ {𝕜 : Type u_1} (B : Type u_2) (F : Type u_3) [inst : NontriviallyNormedField 𝕜] [inst_1 : NormedAddCommGroup F]
  [inst_2 : NormedSpace 𝕜 F] [inst_3 : TopologicalSpace B] (b : B),
  Bundle.Trivialization.coordChangeL 𝕜 (Bundle.Trivial.trivialization B F) (Bundle.Trivial.trivialization B F) b =
    ContinuousLinearEquiv.refl 𝕜 F
-- Mathlib.GroupTheory.QuotientGroup.Defs
QuotientGroup.congr_refl : ∀ {G : Type u_1} [inst : Group G] (G' : Subgroup G) [inst_1 : G'.Normal]
  (he : optParam (Subgroup.map (↑(MulEquiv.refl G)) G' = G') ⋯),
  QuotientGroup.congr G' G' (MulEquiv.refl G) he = MulEquiv.refl (G ⧸ G')
-- Lean.InternalExceptionId
Lean.instBEqInternalExceptionId : BEq Lean.InternalExceptionId
-- Mathlib.Algebra.Field.Subfield.Basic
Subfield.mem_sInf : ∀ {K : Type u} [inst : DivisionRing K] {S : Set (Subfield K)} {x : K}, x ∈ sInf S ↔ ∀ p ∈ S, x ∈ p
-- Mathlib.Order.GaloisConnection.Defs
GaloisInsertion.mk.injEq : ∀ {α : Type u_2} {β : Type u_3} [inst : Preorder α] [inst_1 : Preorder β] {l : α → β} {u : β → α}
  (choice : (x : α) → u (l x) ≤ x → β) (gc : GaloisConnection l u) (le_l_u : ∀ (x : β), x ≤ l (u x))
  (choice_eq : ∀ (a : α) (h : u (l a) ≤ a), choice a h = l a) (choice_1 : (x : α) → u (l x) ≤ x → β)
  (gc_1 : GaloisConnection l u) (le_l_u_1 : ∀ (x : β), x ≤ l (u x))
  (choice_eq_1 : ∀ (a : α) (h : u (l a) ≤ a), choice_1 a h = l a),
  ({ choice := choice, gc := gc, le_l_u := le_l_u, choice_eq := choice_eq } =
      { choice := choice_1, gc := gc_1, le_l_u := le_l_u_1, choice_eq := choice_eq_1 }) =
    (choice = choice_1)
-- Mathlib.Logic.Equiv.Fintype
Equiv.extendSubtype_apply_of_not_mem : ∀ {α : Type u_1} {p q : α → Prop} [inst : DecidablePred p] [inst_1 : DecidablePred q] [inst_2 : Finite ↑{x | p x}]
  (e : { x // p x } ≃ { x // q x }) (x : α) (hx : ¬p x), e.extendSubtype x = ↑(e.toCompl ⟨x, hx⟩)
-- Mathlib.Algebra.Group.Submonoid.Operations
AddSubmonoid.iSup_map_single_le : ∀ {ι : Type u_4} {M : ι → Type u_5} [inst : (i : ι) → AddZeroClass (M i)] [inst_1 : DecidableEq ι] {I : Set ι}
  {S : (i : ι) → AddSubmonoid (M i)}, ⨆ i, AddSubmonoid.map (AddMonoidHom.single M i) (S i) ≤ AddSubmonoid.pi I S
-- Mathlib.Algebra.Category.Grp.FiniteGrp
FiniteGrp.mk.sizeOf_spec : ∀ (toGrp : GrpCat) [isFinite : Finite ↑toGrp],
  sizeOf { toGrp := toGrp, isFinite := isFinite } = 1 + sizeOf toGrp + sizeOf isFinite
-- Mathlib.Algebra.GroupWithZero.Basic
inv_eq_zero : ∀ {G₀ : Type u_2} [inst : GroupWithZero G₀] {a : G₀}, a⁻¹ = 0 ↔ a = 0
-- Mathlib.MeasureTheory.Function.LpSeminorm.Basic
MeasureTheory.lintegral_rpow_enorm_lt_top_of_eLpNorm_lt_top : ∀ {α : Type u_1} {ε : Type u_2} {m0 : MeasurableSpace α} {p : ENNReal} {μ : MeasureTheory.Measure α} [inst : ENorm ε]
  {f : α → ε}, p ≠ 0 → p ≠ ⊤ → MeasureTheory.eLpNorm f p μ < ⊤ → ∫⁻ (a : α), ‖f a‖ₑ ^ p.toReal ∂μ < ⊤
-- Mathlib.Data.Setoid.Partition
IndexedPartition.iUnion : ∀ {ι : Type u_1} {α : Type u_2} {s : ι → Set α} (hs : IndexedPartition s), ⋃ i, s i = Set.univ
-- Mathlib.Analysis.Normed.Operator.Compact.Basic
/-- Upgrade a compact `LinearMap` to a `ContinuousLinearMap`.  -/
ContinuousLinearMap.mkOfIsCompactOperator : {𝕜₁ : Type u_1} →
  {𝕜₂ : Type u_2} →
    [inst : NontriviallyNormedField 𝕜₁] →
      [inst_1 : NontriviallyNormedField 𝕜₂] →
        {σ₁₂ : 𝕜₁ →+* 𝕜₂} →
          [RingHomIsometric σ₁₂] →
            {M₁ : Type u_3} →
              {M₂ : Type u_4} →
                [inst_3 : TopologicalSpace M₁] →
                  [inst_4 : AddCommGroup M₁] →
                    [inst_5 : TopologicalSpace M₂] →
                      [inst_6 : AddCommGroup M₂] →
                        [inst_7 : Module 𝕜₁ M₁] →
                          [inst_8 : Module 𝕜₂ M₂] →
                            [IsTopologicalAddGroup M₁] →
                              [ContinuousConstSMul 𝕜₁ M₁] →
                                [IsTopologicalAddGroup M₂] →
                                  [ContinuousSMul 𝕜₂ M₂] → {f : M₁ →ₛₗ[σ₁₂] M₂} → IsCompactOperator ⇑f → M₁ →SL[σ₁₂] M₂
-- Init.Data.String.OrderInstances
String.Slice.Pos.instLawfulOrderBEq : ∀ {s : String.Slice}, Std.LawfulOrderBEq s.Pos
-- Mathlib.Algebra.Homology.LeftResolution.Basic
CategoryTheory.Abelian.LeftResolution.π_naturality : ∀ {A : Type u_1} {C : Type u_2} [inst : CategoryTheory.Category.{v_1, u_2} C]
  [inst_1 : CategoryTheory.Category.{v_2, u_1} A] {ι : CategoryTheory.Functor C A}
  (Λ : CategoryTheory.Abelian.LeftResolution ι) (X Y : A) (f : X ⟶ Y),
  CategoryTheory.CategoryStruct.comp (ι.map (Λ.F.map f)) (Λ.π.app Y) = CategoryTheory.CategoryStruct.comp (Λ.π.app X) f
-- Lean.Data.Lsp.LanguageFeatures
Lean.Lsp.ResolvableCompletionItemData.mk.injEq : ∀ (uri : Lean.Lsp.DocumentUri) (pos : Lean.Lsp.Position) (cPos? : Option ℕ) (id? : Option Lean.Lsp.CompletionIdentifier)
  (uri_1 : Lean.Lsp.DocumentUri) (pos_1 : Lean.Lsp.Position) (cPos?_1 : Option ℕ)
  (id?_1 : Option Lean.Lsp.CompletionIdentifier),
  ({ uri := uri, pos := pos, cPos? := cPos?, id? := id? } =
      { uri := uri_1, pos := pos_1, cPos? := cPos?_1, id? := id?_1 }) =
    (uri = uri_1 ∧ pos = pos_1 ∧ cPos? = cPos?_1 ∧ id? = id?_1)
-- Mathlib.Combinatorics.Derangements.Finite
instFintypeElemPermDerangements : {α : Type u_1} → [DecidableEq α] → [Fintype α] → Fintype ↑(derangements α)
-- Mathlib.Geometry.RingedSpace.PresheafedSpace.Gluing
/-- (Implementation). The map `Γ(𝒪_{U_i}, U) ⟶ Γ(𝒪_{U_j}, 𝖣.ι j ⁻¹' 𝖣.ι i '' U)`  -/
AlgebraicGeometry.PresheafedSpace.GlueData.opensImagePreimageMap : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    (D : AlgebraicGeometry.PresheafedSpace.GlueData C) →
      [inst_1 : CategoryTheory.Limits.HasLimits C] →
        (i j : D.J) →
          (U : TopologicalSpace.Opens ↑↑(D.U i)) →
            (D.U i).presheaf.obj (Opposite.op U) ⟶
              (D.U j).presheaf.obj (Opposite.op ((TopologicalSpace.Opens.map (D.ι j).base).obj (⋯.functor.obj U)))
-- Mathlib.Topology.VectorBundle.Riemannian
_private.Mathlib.Topology.VectorBundle.Riemannian.0.«term⟪_,_⟫» : Lean.ParserDescr
-- Mathlib.CategoryTheory.Bicategory.FunctorBicategory.Oplax
/-- Right unitor for the vertical composition of oplax natural transformations.  -/
CategoryTheory.Oplax.OplaxTrans.rightUnitor : {B : Type u₁} →
  [inst : CategoryTheory.Bicategory B] →
    {C : Type u₂} →
      [inst_1 : CategoryTheory.Bicategory C] →
        {F G : CategoryTheory.OplaxFunctor B C} →
          (η : F ⟶ G) → CategoryTheory.CategoryStruct.comp η (CategoryTheory.CategoryStruct.id G) ≅ η
-- Mathlib.CategoryTheory.Sums.Products
/-- `functorEquiv A A' B` transforms `Swap.equivalence` into `Prod.braiding`.  -/
CategoryTheory.Sum.Swap.equivalenceFunctorEquivFunctorIso : {A : Type u_1} →
  [inst : CategoryTheory.Category.{v_1, u_1} A] →
    {A' : Type u_2} →
      [inst_1 : CategoryTheory.Category.{v_2, u_2} A'] →
        {B : Type u} →
          [inst_2 : CategoryTheory.Category.{v, u} B] →
            ((CategoryTheory.Sum.Swap.equivalence A A').congrLeft.trans
                  (CategoryTheory.Sum.functorEquiv A' A B)).functor ≅
              ((CategoryTheory.Sum.functorEquiv A A' B).trans
                  (CategoryTheory.Prod.braiding (CategoryTheory.Functor A B) (CategoryTheory.Functor A' B))).functor
-- Mathlib.CategoryTheory.Monoidal.DayConvolution.Closed
CategoryTheory.MonoidalCategory.DayConvolutionInternalHom.mk.inj : ∀ {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}
  {inst_4 : CategoryTheory.MonoidalClosed V} {F G H : CategoryTheory.Functor C V}
  {π : (c j : C) → H.obj c ⟶ F.obj j ⟹ G.obj (CategoryTheory.MonoidalCategoryStruct.tensorObj j c)}
  {hπ :
    ∀ (c : C) ⦃i j : C⦄ (f : i ⟶ j),
      CategoryTheory.CategoryStruct.comp (π c i)
          ((CategoryTheory.ihom (F.obj i)).map (G.map (CategoryTheory.MonoidalCategoryStruct.whiskerRight f c))) =
        CategoryTheory.CategoryStruct.comp (π c j)
          ((CategoryTheory.MonoidalClosed.pre (F.map f)).app
            (G.obj (CategoryTheory.MonoidalCategoryStruct.tensorObj j c)))}
  {isLimitWedge : (c : C) → CategoryTheory.Limits.IsLimit (CategoryTheory.Limits.Wedge.mk (H.obj c) (π c) ⋯)}
  {map_comp_π :
    ∀ {c c' : C} (f : c ⟶ c') (j : C),
      CategoryTheory.CategoryStruct.comp (H.map f) (π c' j) =
        CategoryTheory.CategoryStruct.comp (π c j)
          ((CategoryTheory.ihom (F.obj j)).map (G.map (CategoryTheory.MonoidalCategoryStruct.whiskerLeft j f)))}
  {π_1 : (c j : C) → H.obj c ⟶ F.obj j ⟹ G.obj (CategoryTheory.MonoidalCategoryStruct.tensorObj j c)}
  {hπ_1 :
    ∀ (c : C) ⦃i j : C⦄ (f : i ⟶ j),
      CategoryTheory.CategoryStruct.comp (π_1 c i)
          ((CategoryTheory.ihom (F.obj i)).map (G.map (CategoryTheory.MonoidalCategoryStruct.whiskerRight f c))) =
        CategoryTheory.CategoryStruct.comp (π_1 c j)
          ((CategoryTheory.MonoidalClosed.pre (F.map f)).app
            (G.obj (CategoryTheory.MonoidalCategoryStruct.tensorObj j c)))}
  {isLimitWedge_1 : (c : C) → CategoryTheory.Limits.IsLimit (CategoryTheory.Limits.Wedge.mk (H.obj c) (π_1 c) ⋯)}
  {map_comp_π_1 :
    ∀ {c c' : C} (f : c ⟶ c') (j : C),
      CategoryTheory.CategoryStruct.comp (H.map f) (π_1 c' j) =
        CategoryTheory.CategoryStruct.comp (π_1 c j)
          ((CategoryTheory.ihom (F.obj j)).map (G.map (CategoryTheory.MonoidalCategoryStruct.whiskerLeft j f)))},
  { π := π, hπ := hπ, isLimitWedge := isLimitWedge, map_comp_π := map_comp_π } =
      { π := π_1, hπ := hπ_1, isLimitWedge := isLimitWedge_1, map_comp_π := map_comp_π_1 } →
    π = π_1 ∧ isLimitWedge ≍ isLimitWedge_1
-- Mathlib.Algebra.Category.Ring.Basic
SemiRingCat.hasForgetToMonCat : CategoryTheory.HasForget₂ SemiRingCat MonCat