mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Topology.Algebra.Valued.WithVal
WithVal.ofVal_nnratCast : ∀ {R : Type u_1} {Γ₀ : Type u_2} [inst : LinearOrderedCommGroupWithZero Γ₀] [inst_1 : DivisionRing R]
  (v : Valuation R Γ₀) (q : ℚ≥0), (↑q).ofVal = ↑q
-- Lean.Compiler.IR.Basic
Lean.IR.instAlphaEqvArg : Lean.IR.AlphaEqv Lean.IR.Arg
-- Mathlib.Data.Set.Card
Set.ncard_sdiff_add_ncard_of_subset : ∀ {α : Type u_1} {s t : Set α},
  s ⊆ t → autoParam t.Finite Set.ncard_sdiff_add_ncard_of_subset._auto_1 → (t \ s).ncard + s.ncard = t.ncard
-- Mathlib.Analysis.Complex.RealDeriv
HasStrictDerivAt.complexToReal_fderiv' : ∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℂ E] {f : ℂ → E} {x : ℂ} {f' : E},
  HasStrictDerivAt f f' x → HasStrictFDerivAt f (Complex.reCLM.smulRight f' + Complex.I • Complex.imCLM.smulRight f') x
-- Std.Data.HashMap.RawLemmas
Std.HashMap.Raw.getD_inter_of_not_mem_right : ∀ {α : Type u} [inst : BEq α] [inst_1 : Hashable α] {β : Type v} {m₁ m₂ : Std.HashMap.Raw α β} [EquivBEq α]
  [LawfulHashable α], m₁.WF → m₂.WF → ∀ {k : α} {fallback : β}, k ∉ m₂ → (m₁ ∩ m₂).getD k fallback = fallback
-- Mathlib.MeasureTheory.Group.FundamentalDomain
MeasureTheory.IsFundamentalDomain.integral_eq_tsum' : ∀ {G : Type u_1} {α : Type u_3} {E : Type u_5} [inst : Group G] [inst_1 : MulAction G α] [inst_2 : MeasurableSpace α]
  [inst_3 : NormedAddCommGroup E] {s : Set α} {μ : MeasureTheory.Measure α} [MeasurableConstSMul G α]
  [MeasureTheory.SMulInvariantMeasure G α μ] [Countable G] [inst_7 : NormedSpace ℝ E],
  MeasureTheory.IsFundamentalDomain G s μ →
    ∀ (f : α → E), MeasureTheory.Integrable f μ → ∫ (x : α), f x ∂μ = ∑' (g : G), ∫ (x : α) in s, f (g⁻¹ • x) ∂μ
-- Mathlib.Algebra.FreeMonoid.Basic
FreeMonoid.ofList_append : ∀ {α : Type u_1} (xs ys : List α), FreeMonoid.ofList (xs ++ ys) = FreeMonoid.ofList xs * FreeMonoid.ofList ys
-- Init.Data.List.Lemmas
List.getElem_append : ∀ {α : Type u_1} {l₁ l₂ : List α} {i : ℕ} (h : i < (l₁ ++ l₂).length),
  (l₁ ++ l₂)[i] = if h' : i < l₁.length then l₁[i] else l₂[i - l₁.length]
-- Mathlib.Order.Filter.Germ.Basic
Filter.Germ.liftRel_coe : ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} {l : Filter α} {r : β → γ → Prop} {f : α → β} {g : α → γ},
  Filter.Germ.LiftRel r ↑f ↑g ↔ ∀ᶠ (x : α) in l, r (f x) (g x)
-- Std.Data.DTreeMap.Internal.Zipper
_private.Std.Data.DTreeMap.Internal.Zipper.0.Std.DTreeMap.Internal.Zipper.prependMap.eq_def : ∀ {α : Type u} {β : α → Type v} (x : Std.DTreeMap.Internal.Impl α β) (x_1 : Std.DTreeMap.Internal.Zipper α β),
  Std.DTreeMap.Internal.Zipper.prependMap x x_1 =
    match x, x_1 with
    | Std.DTreeMap.Internal.Impl.leaf, it => it
    | Std.DTreeMap.Internal.Impl.inner size k v l r, it =>
      Std.DTreeMap.Internal.Zipper.prependMap l (Std.DTreeMap.Internal.Zipper.cons k v r it)
-- Lean.DocString.Extension
Lean.VersoModuleDocs.mk.injEq : ∀ (snippets snippets_1 : Lean.PersistentArray Lean.VersoModuleDocs.Snippet),
  ({ snippets := snippets } = { snippets := snippets_1 }) = (snippets = snippets_1)
-- Init.Data.Bool
Bool.xor_right_comm : ∀ (x y z : Bool), (x ^^ y ^^ z) = (x ^^ z ^^ y)
-- Std.Data.DTreeMap.Internal.WF.Lemmas
_private.Std.Data.DTreeMap.Internal.WF.Lemmas.0.Std.Internal.List.alterKey_cons_perm.match_1.eq_1 : ∀ {α : Type u_3} {β : α → Type u_1} {k : α} (motive : Option (β k) → Sort u_2) (h_1 : Unit → motive none)
  (h_2 : (v : β k) → motive (some v)),
  (match none with
    | none => h_1 ()
    | some v => h_2 v) =
    h_1 ()
-- Mathlib.Algebra.Order.Hom.Basic
/-- `MulLEAddHomClass F α β` states that `F` is a type of subadditive morphisms.  -/
MulLEAddHomClass : (F : Type u_7) →
  (α : outParam (Type u_8)) → (β : outParam (Type u_9)) → [Mul α] → [Add β] → [LE β] → [FunLike F α β] → Prop
-- Mathlib.Algebra.Homology.ShortComplex.LeftHomology
CategoryTheory.ShortComplex.cyclesMapIso'_hom : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  {S₁ S₂ : CategoryTheory.ShortComplex C} (e : S₁ ≅ S₂) (h₁ : S₁.LeftHomologyData) (h₂ : S₂.LeftHomologyData),
  (CategoryTheory.ShortComplex.cyclesMapIso' e h₁ h₂).hom = CategoryTheory.ShortComplex.cyclesMap' e.hom h₁ h₂
-- Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Restrict
QuasispectrumRestricts.nonUnitalStarAlgHom_id : ∀ {R : Type u_1} {S : Type u_2} {A : Type u_3} [inst : Semifield R] [inst_1 : StarRing R] [inst_2 : MetricSpace R]
  [inst_3 : IsTopologicalSemiring R] [inst_4 : ContinuousStar R] [inst_5 : Field S] [inst_6 : StarRing S]
  [inst_7 : MetricSpace S] [inst_8 : IsTopologicalRing S] [inst_9 : ContinuousStar S] [inst_10 : NonUnitalRing A]
  [inst_11 : StarRing A] [inst_12 : Module S A] [inst_13 : IsScalarTower S A A] [inst_14 : SMulCommClass S A A]
  [inst_15 : Algebra R S] [inst_16 : Module R A] [inst_17 : IsScalarTower R S A] [inst_18 : StarModule R S]
  [inst_19 : ContinuousSMul R S] {a : A} {φ : ContinuousMapZero (↑(quasispectrum S a)) S →⋆ₙₐ[S] A} {f : C(S, R)}
  (h : QuasispectrumRestricts a ⇑f),
  φ (ContinuousMapZero.id (quasispectrum S a)) = a →
    (QuasispectrumRestricts.nonUnitalStarAlgHom φ h) (ContinuousMapZero.id (quasispectrum R a)) = a
-- Mathlib.Topology.Sheaves.Stalks
TopCat.Presheaf.stalkCongr_inv : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Limits.HasColimits C] {X : TopCat}
  (F : TopCat.Presheaf C X) {x y : ↑X} (e : Inseparable x y), (F.stalkCongr e).inv = F.stalkSpecializes ⋯
-- Mathlib.CategoryTheory.Monoidal.Mod
/-- **Alias** of `CategoryTheory.Mod.regular`.

---

A monoid object as a module over itself.  -/
CategoryTheory.Mod_.regular : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    [inst_1 : CategoryTheory.MonoidalCategory C] → (A : C) → [inst_2 : CategoryTheory.MonObj A] → CategoryTheory.Mod C A
-- Init.Data.Iterators.Lemmas.Consumers.Loop
_private.Init.Data.Iterators.Lemmas.Consumers.Loop.0.Std.IterM.DefaultConsumers.forIn'_eq_match_step.match_1.splitter : {β : Type u_3} →
  {γ : Type u_1} →
    {init : γ} →
      (PlausibleForInStep : β → γ → ForInStep γ → Prop) →
        (out : β) →
          (motive : Subtype (PlausibleForInStep out init) → Sort u_2) →
            (__do_lift : Subtype (PlausibleForInStep out init)) →
              ((c : γ) →
                  (property : PlausibleForInStep out init (ForInStep.yield c)) → motive ⟨ForInStep.yield c, property⟩) →
                ((c : γ) →
                    (property : PlausibleForInStep out init (ForInStep.done c)) → motive ⟨ForInStep.done c, property⟩) →
                  motive __do_lift
-- Init.Data.UInt.IntToBitVec
USize.toBitVec32_mul : ∀ {a b : USize} (h : System.Platform.numBits = 32), (a * b).toBitVec32 h = a.toBitVec32 h * b.toBitVec32 h
-- Mathlib.MeasureTheory.Integral.IntervalIntegral.Periodic
/-- If a function satisfies `MemLp` on the interval `(t, t + T]`, then its lift to the AddCircle
also satisfies `MemLp` with respect to the Haar measure.  -/
MeasureTheory.MemLp.memLp_liftIoc : ∀ {T : ℝ} [hT : Fact (0 < T)] {t : ℝ} {f : ℝ → ℂ} {p : ENNReal},
  MeasureTheory.MemLp f p (MeasureTheory.volume.restrict (Set.Ioc t (t + T))) →
    MeasureTheory.MemLp (AddCircle.liftIoc T t f) p MeasureTheory.volume
-- Mathlib.Analysis.Real.Sqrt
NNReal.isSquare : ∀ (x : NNReal), IsSquare x
-- Mathlib.Algebra.Group.Basic
/-- Composing two additions on the left by `y` then `x`
is equal to an addition on the left by `x + y`.  -/
comp_add_left : ∀ {α : Type u_1} [inst : AddSemigroup α] (x y : α), ((fun x_1 => x + x_1) ∘ fun x => y + x) = fun x_1 => x + y + x_1
-- Mathlib.Order.RelClasses
/-- Set notation form of `le_of_eq` -/
subset_of_eq : ∀ {α : Type u_1} [UsesSetNotationForOrder α] [inst : Preorder α] {a b : α}, a = b → a ⊆ b
-- Mathlib.AlgebraicTopology.SimplicialObject.DeltaZeroIter
CategoryTheory.SimplicialObject.δ₀Iter_zero : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] (X : CategoryTheory.SimplicialObject C) (n : ℕ),
  X.δ₀Iter 0 ⋯ = CategoryTheory.CategoryStruct.id (X.obj (Opposite.op { len := n }))
-- Lean.Meta.Tactic.Grind.Action
Lean.Meta.Grind.Action.mkGrindSeq : List Lean.Meta.Grind.TGrind → Lean.TSyntax `Lean.Parser.Tactic.Grind.grindSeq
-- Mathlib.Order.CompletePartialOrder
/-- For each directed set `d`, `sSup d` is the least upper bound of `d`.  -/
CompletePartialOrder.lubOfDirected : ∀ {α : Type u_4} [self : CompletePartialOrder α] (d : Set α), DirectedOn (fun x1 x2 => x1 ≤ x2) d → IsLUB d (sSup d)
-- Mathlib.CategoryTheory.Adjunction.Basic
/-- Construct a right adjoint functor to `F`, given the functor's value on objects `G_obj` and
a bijection `e` between `F.obj X ⟶ Y` and `X ⟶ G_obj Y` satisfying a naturality law
`he : ∀ X' X Y f g, e X' Y (F.map f ≫ g) = f ≫ e X Y g`.
Dual to `leftAdjointOfEquiv`.  -/
CategoryTheory.Adjunction.rightAdjointOfEquiv : {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_obj : D → C} →
            (e : (X : C) → (Y : D) → (F.obj X ⟶ Y) ≃ (X ⟶ G_obj Y)) →
              (∀ (X' X : C) (Y : D) (f : X' ⟶ X) (g : F.obj X ⟶ Y),
                  (e X' Y) (CategoryTheory.CategoryStruct.comp (F.map f) g) =
                    CategoryTheory.CategoryStruct.comp f ((e X Y) g)) →
                CategoryTheory.Functor D C
-- Mathlib.Algebra.Ring.Subsemiring.Basic
Subsemiring.prod_bot_sup_bot_prod : ∀ {R : Type u} {S : Type v} [inst : NonAssocSemiring R] [inst_1 : NonAssocSemiring S] (s : Subsemiring R)
  (t : Subsemiring S), s.prod ⊥ ⊔ ⊥.prod t = s.prod t
-- Mathlib.Algebra.Category.ModuleCat.Monoidal.Basic
SemimoduleCat.monoidalCategory : {R : Type u} → [inst : CommSemiring R] → CategoryTheory.MonoidalCategory (SemimoduleCat R)
-- Mathlib.Topology.Order.LowerUpperTopology
/-- If `α` is equipped with the upper topology, then it is homeomorphic to `WithUpper α`.
 -/
Topology.IsUpper.withUpperHomeomorph : {α : Type u_1} → [inst : Preorder α] → [inst_1 : TopologicalSpace α] → [Topology.IsUpper α] → Topology.WithUpper α ≃ₜ α
-- Mathlib.RingTheory.Valuation.ValuationSubring
ValuationSubring.coe_unitGroupToResidueFieldUnits_apply : ∀ {K : Type u} [inst : Field K] (A : ValuationSubring K) (x : ↥A.unitGroup),
  ↑(A.unitGroupToResidueFieldUnits x) = (Ideal.Quotient.mk (IsLocalRing.maximalIdeal ↥A)) ↑(A.unitGroupMulEquiv x)
-- Init.Core
/-- Monadic iteration in `do`-blocks with a membership proof, using the `for h : x in xs` notation.

The parameter `m` is the monad of the `do`-block in which iteration is performed, `ρ` is the type of
the collection being iterated over, `α` is the type of elements, and `d` is the specific membership
predicate to provide.
 -/
ForIn' : (Type u₁ → Type u₂) →
  (ρ : Type u) → (α : outParam (Type v)) → outParam (Membership α ρ) → Type (max (max (max u (u₁ + 1)) u₂) v)
-- Mathlib.CategoryTheory.Abelian.Projective.Resolution
CategoryTheory.ProjectiveResolution.ofComplex_exactAt_succ : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Abelian C]
  [inst_2 : CategoryTheory.EnoughProjectives C] (Z : C) (n : ℕ),
  HomologicalComplex.ExactAt (CategoryTheory.ProjectiveResolution.ofComplex Z) (n + 1)
-- Mathlib.NumberTheory.LSeries.Dirichlet
/-- The L-series of a Dirichlet character mod `N > 0` converges absolutely at `s` if and only if
`re s > 1`.  -/
DirichletCharacter.LSeriesSummable_iff : ∀ {N : ℕ}, N ≠ 0 → ∀ (χ : DirichletCharacter ℂ N) {s : ℂ}, LSeriesSummable (fun n => χ ↑n) s ↔ 1 < s.re
-- Mathlib.RepresentationTheory.Homological.GroupHomology.LowDegree
groupHomology.d₂₁_comp_d₁₀_assoc : ∀ {k G : Type u} [inst : CommRing k] [inst_1 : Group G] (A : Rep.{u, u, u} k G) {Z : ModuleCat k}
  (h : ModuleCat.of k ↑A ⟶ Z),
  CategoryTheory.CategoryStruct.comp (groupHomology.d₂₁ A)
      (CategoryTheory.CategoryStruct.comp (groupHomology.d₁₀ A) h) =
    CategoryTheory.CategoryStruct.comp 0 h
-- Init.Data.Nat.Basic
Nat.ne_iff_lt_or_gt : ∀ {a b : ℕ}, a ≠ b ↔ a < b ∨ b < a
-- Mathlib.Tactic.Translate.ToAdditive
/-- `to_additive_name_hint src tgt` lets `to_additive` translate the name segment `src` to `tgt`
for the rest of the file current. `src` and `tgt` should both be capitalized.  -/
Mathlib.Tactic.ToAdditive.commandTo_additive_name_hint__ : Lean.ParserDescr
-- Mathlib.Algebra.Algebra.Epi
Algebra.instIsEpiOfIsDomainOfIsFractionRing : ∀ (R : Type u_1) (A : Type u_2) [inst : CommRing R] [IsDomain R] [inst_2 : Field A] [inst_3 : Algebra R A]
  [IsFractionRing R A], Algebra.IsEpi R A
-- Mathlib.NumberTheory.ModularForms.BoundedAtCusp
UpperHalfPlane.IsZeroAtImInfty.slash : ∀ {g : GL (Fin 2) ℝ} {f : UpperHalfPlane → ℂ} (k : ℤ),
  ↑g 1 0 = 0 → UpperHalfPlane.IsZeroAtImInfty f → UpperHalfPlane.IsZeroAtImInfty (SlashAction.map k g f)
-- Mathlib.Algebra.Homology.Augment
/-- There is a canonical chain map from the truncation of a chain map `C` to
the "single object" chain complex consisting of the truncated object `C.X 0` in degree 0.
The components of this chain map are `C.d 1 0` in degree 0, and zero otherwise.
 -/
ChainComplex.truncateTo : {V : Type u} →
  [inst : CategoryTheory.Category.{v, u} V] →
    [inst_1 : CategoryTheory.Limits.HasZeroObject V] →
      [inst_2 : CategoryTheory.Limits.HasZeroMorphisms V] →
        (C : ChainComplex V ℕ) → ChainComplex.truncate.obj C ⟶ (ChainComplex.single₀ V).obj (C.X 0)
-- Mathlib.Analysis.Convex.StdSimplex
/-- `stdSimplex 𝕜 ι` is compact.  -/
isCompact_stdSimplex : ∀ (𝕜 : Type u_1) (ι : Type u_2) [inst : Fintype ι] [inst_1 : TopologicalSpace 𝕜] [inst_2 : Semiring 𝕜]
  [inst_3 : PartialOrder 𝕜] [OrderClosedTopology 𝕜] [ContinuousAdd 𝕜] [CompactIccSpace 𝕜] [IsOrderedAddMonoid 𝕜],
  IsCompact (stdSimplex 𝕜 ι)
-- Std.Http.Data.URI.Encoding
/-- Attempts to create an encoded query parameter from raw bytes.
 -/
Std.Http.URI.EncodedQueryParam.ofByteArray? : ByteArray → Option Std.Http.URI.EncodedQueryParam
-- Mathlib.RingTheory.WittVector.Frobenius
WittVector.frobenius_bijective : ∀ (p : ℕ) (R : Type u_1) [hp : Fact (Nat.Prime p)] [inst : CommRing R] [CharP R p] [PerfectRing R p],
  Function.Bijective ⇑WittVector.frobenius
-- Mathlib.Combinatorics.SimpleGraph.Copy
SimpleGraph.IsIndContained.trans : ∀ {V : Type u_1} {W : Type u_2} {X : Type u_3} {G : SimpleGraph V} {H : SimpleGraph W} {I : SimpleGraph X},
  G.IsIndContained H → H.IsIndContained I → G.IsIndContained I
-- Mathlib.AlgebraicTopology.CechNerve
/-- The diagram `Option ι ⥤ C` sending `none` to the terminal object and `some j` to `X`.  -/
CategoryTheory.CechNerveTerminalFrom.wideCospan : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    [CategoryTheory.Limits.HasTerminal C] →
      (ι : Type w) → C → CategoryTheory.Functor (CategoryTheory.Limits.WidePullbackShape ι) C
-- Mathlib.RepresentationTheory.Subrepresentation
Subrepresentation.instPartialOrder : {A : Type u_1} →
  {G : Type u_2} →
    {W : Type u_3} →
      [inst : Semiring A] →
        [inst_1 : Monoid G] →
          [inst_2 : AddCommMonoid W] →
            [inst_3 : Module A W] → {ρ : Representation A G W} → PartialOrder (Subrepresentation ρ)
-- Mathlib.RingTheory.PowerSeries.WellKnown
/-- Power series for the sine function at zero.  -/
PowerSeries.sin : (A : Type u_1) → [inst : Ring A] → [Algebra ℚ A] → PowerSeries A
-- Init.Ext
Char.ext_iff : ∀ {c d : Char}, c = d ↔ c.val = d.val
-- Mathlib.Topology.LocallyFinsupp
Function.locallyFinsuppWithin.posPart_apply : ∀ {X : Type u_1} [inst : TopologicalSpace X] {U : Set X} {Y : Type u_2} [inst_1 : Lattice Y] [inst_2 : AddCommGroup Y]
  (a : Function.locallyFinsuppWithin U Y) (x : X), a⁺ x = (a x)⁺
-- Mathlib.Order.Monotone.Defs
monotone_id : ∀ {α : Type u} [inst : Preorder α], Monotone id
-- Aesop.Tree.TreeM
Aesop.getAllIntroducedMVars : Aesop.TreeM (Std.HashSet Lean.MVarId)
-- Init.Data.Vector.Int
Vector.prod_reverse_int : ∀ {n : ℕ} (xs : Vector ℤ n), xs.reverse.prod = xs.prod
-- Mathlib.Algebra.Group.Equiv.Basic
AddEquivClass.isDedekindFiniteAddMonoid_iff : ∀ {F : Type u_1} {α : Type u_2} {β : Type u_3} [inst : EquivLike F α β] [inst_1 : AddZero α] [inst_2 : AddZero β]
  [AddEquivClass F α β] [ZeroHomClass F α β] (f : F), IsDedekindFiniteAddMonoid α ↔ IsDedekindFiniteAddMonoid β
-- Mathlib.RingTheory.TensorProduct.IsBaseChangePi
IsBaseChange.finitePow : ∀ {R : Type u_1} {S : Type u_2} [inst : CommSemiring R] [inst_1 : CommSemiring S] [inst_2 : Algebra R S] (ι : Type u_3)
  [Finite ι] {M : Type u_4} {M' : Type u_5} [inst_4 : AddCommMonoid M] [inst_5 : AddCommMonoid M'] [inst_6 : Module R M]
  [inst_7 : Module R M'] [inst_8 : Module S M'] [inst_9 : IsScalarTower R S M'] {f : M →ₗ[R] M'},
  IsBaseChange S f → IsBaseChange S (f.compLeft ι)
-- Mathlib.GroupTheory.FreeAbelianGroup
FreeAbelianGroup.map_id : ∀ {α : Type u}, FreeAbelianGroup.map id = AddMonoidHom.id (FreeAbelianGroup α)
-- Mathlib.Probability.Kernel.Disintegration.Density
ProbabilityTheory.Kernel.setLIntegral_density : ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} {mα : MeasurableSpace α} {mβ : MeasurableSpace β}
  {mγ : MeasurableSpace γ} [inst : MeasurableSpace.CountablyGenerated γ] {κ : ProbabilityTheory.Kernel α (γ × β)}
  {ν : ProbabilityTheory.Kernel α γ},
  κ.fst ≤ ν →
    ∀ [ProbabilityTheory.IsFiniteKernel ν] (a : α) {s : Set β},
      MeasurableSet s →
        ∀ {A : Set γ}, MeasurableSet A → ∫⁻ (x : γ) in A, ENNReal.ofReal (κ.density ν a x s) ∂ν a = (κ a) (A ×ˢ s)
-- Mathlib.Tactic.ClickSuggestions.SectionState
Mathlib.Tactic.ClickSuggestions.instInhabitedResult.default : {α : Type} → [Inhabited α] → Mathlib.Tactic.ClickSuggestions.Result α
-- Mathlib.Order.Filter.Basic
Filter.disjoint_iff : ∀ {α : Type u} {f g : Filter α}, Disjoint f g ↔ ∃ s ∈ f, ∃ t ∈ g, Disjoint s t
-- Mathlib.MeasureTheory.Function.LocallyIntegrable
MeasureTheory.LocallyIntegrableOn.eq_1 : ∀ {X : Type u_1} {ε : Type u_3} [inst : MeasurableSpace X] [inst_1 : TopologicalSpace X] [inst_2 : TopologicalSpace ε]
  [inst_3 : ContinuousENorm ε] (f : X → ε) (s : Set X) (μ : MeasureTheory.Measure X),
  MeasureTheory.LocallyIntegrableOn f s μ = ∀ x ∈ s, MeasureTheory.IntegrableAtFilter f (nhdsWithin x s) μ
-- Mathlib.MeasureTheory.Function.LpSeminorm.Basic
MeasureTheory.eLpNorm_le_add_measure_left : ∀ {α : Type u_1} {m0 : MeasurableSpace α} {ε : Type u_7} [inst : TopologicalSpace ε] [inst_1 : ContinuousENorm ε]
  (f : α → ε) (μ ν : MeasureTheory.Measure α) {p : ENNReal},
  MeasureTheory.eLpNorm f p ν ≤ MeasureTheory.eLpNorm f p (μ + ν)
-- Lean.Parser.Extra
/-- No-op parser that advises the pretty printer to emit a space/soft line break.  -/
Lean.Parser.ppSpace : Lean.Parser.Parser
-- Mathlib.Topology.PartialHomeomorph.Defs
PartialHomeomorph.invOn : ∀ {X : Type u_1} {Y : Type u_3} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y] (e : PartialHomeomorph X Y),
  Set.InvOn (↑e.symm) (↑e) e.source e.target
-- Mathlib.Order.Interval.Set.Monotone
MonotoneOn.Ico : ∀ {α : Type u_1} {β : Type u_2} [inst : Preorder α] [inst_1 : Preorder β] {f g : α → β} {s : Set α},
  MonotoneOn f s → AntitoneOn g s → AntitoneOn (fun x => Set.Ico (f x) (g x)) s
-- Mathlib.Algebra.Group.Pointwise.Finset.Basic
Finset.neg_insert : ∀ {α : Type u_2} [inst : DecidableEq α] [inst_1 : Neg α] (a : α) (s : Finset α), -insert a s = insert (-a) (-s)
-- Mathlib.Order.Irreducible
/-- **Alias** of the reverse direction of `infPrime_iff_infIrred`. -/
InfIrred.infPrime : ∀ {α : Type u_2} [inst : DistribLattice α] {a : α}, InfIrred a → InfPrime a
-- Mathlib.Algebra.Order.Monovary
antivary_neg : ∀ {ι : Type u_1} {α : Type u_2} {β : Type u_3} [inst : AddCommGroup α] [inst_1 : PartialOrder α] [IsOrderedAddMonoid α]
  [inst_3 : AddCommGroup β] [inst_4 : PartialOrder β] [IsOrderedAddMonoid β] {f : ι → α} {g : ι → β},
  Antivary (-f) (-g) ↔ Antivary f g
-- Mathlib.Order.Interval.Set.Image
StrictMono.image_Ico_subset : ∀ {α : Type u_1} {β : Type u_2} {f : α → β} [inst : PartialOrder α] [inst_1 : Preorder β] {a b : α},
  StrictMono f → f '' Set.Ico a b ⊆ Set.Ico (f a) (f b)
-- Mathlib.Combinatorics.SimpleGraph.Matching
SimpleGraph.Subgraph.IsMatching.not_adj_right_of_ne : ∀ {V : Type u_1} {G : SimpleGraph V} {M : G.Subgraph} {u v w : V}, M.IsMatching → u ≠ v → M.Adj u w → ¬M.Adj v w
-- Mathlib.Topology.ContinuousMap.ContinuousMapZero
ContinuousMapZero.instAddCommMonoid : {X : Type u_1} →
  {R : Type u_2} →
    [inst : Zero X] →
      [inst_1 : TopologicalSpace X] →
        [inst_2 : TopologicalSpace R] →
          [inst_3 : AddCommMonoid R] → [ContinuousAdd R] → AddCommMonoid (ContinuousMapZero X R)
-- Mathlib.GroupTheory.Commutator.Finite
card_commutator_closureCommutatorRepresentatives : ∀ {G : Type u_1} [inst : Group G],
  Nat.card ↥(commutator ↥(closureCommutatorRepresentatives G)) = Nat.card ↥(commutator G)
-- Mathlib.CategoryTheory.Join.Pseudofunctor
CategoryTheory.Join.pseudofunctorRight_toPrelaxFunctor_toPrelaxFunctorStruct_map₂_toNatTrans_app : ∀ (C : Type u₁) [inst : CategoryTheory.Category.{v₁, u₁} C] {a b : CategoryTheory.Cat} {f g : a ⟶ b} (f_1 : f ⟶ g)
  (x : CategoryTheory.Join C ↑a),
  ((CategoryTheory.Join.pseudofunctorRight C).map₂ f_1).toNatTrans.app x =
    match x with
    | CategoryTheory.Join.left x => CategoryTheory.CategoryStruct.id (CategoryTheory.Join.left x)
    | CategoryTheory.Join.right x => (CategoryTheory.Join.inclRight C ↑b).map (f_1.toNatTrans.app x)
-- Init.System.IOError
IO.Error.invalidArgument.inj : ∀ {filename : Option String} {osCode : UInt32} {details : String} {filename_1 : Option String} {osCode_1 : UInt32}
  {details_1 : String},
  IO.Error.invalidArgument filename osCode details = IO.Error.invalidArgument filename_1 osCode_1 details_1 →
    filename = filename_1 ∧ osCode = osCode_1 ∧ details = details_1
-- Std.Data.Iterators.Lemmas.Equivalence.Basic
Std.BundledIterM.α : {m : Type w → Type w'} → {β : Type w} → Std.BundledIterM m β → Type w
-- Mathlib.Algebra.Quaternion
QuaternionAlgebra.ext_iff : ∀ {R : Type u_1} {a b c : R} {x y : QuaternionAlgebra R a b c},
  x = y ↔ x.re = y.re ∧ x.imI = y.imI ∧ x.imJ = y.imJ ∧ x.imK = y.imK
-- Mathlib.Order.SuccPred.LinearLocallyFinite
/-- `toZ` numbers elements of `ι` according to their order, starting from `i0`. We prove in
`orderIsoRangeToZOfLinearSuccPredArch` that this defines an `OrderIso` between `ι` and
the range of `toZ`.  -/
toZ : {ι : Type u_1} → [inst : LinearOrder ι] → [inst_1 : SuccOrder ι] → [IsSuccArchimedean ι] → [PredOrder ι] → ι → ι → ℤ
-- Mathlib.CategoryTheory.Filtered.Final
CategoryTheory.isFiltered_structuredArrow_of_isFiltered_of_exists : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  (F : CategoryTheory.Functor C D) [CategoryTheory.IsFilteredOrEmpty C] (d : D),
  (∃ c, Nonempty (d ⟶ F.obj c)) →
    (∀ {c : C} (s s' : d ⟶ F.obj c),
        ∃ c' t, CategoryTheory.CategoryStruct.comp s (F.map t) = CategoryTheory.CategoryStruct.comp s' (F.map t)) →
      CategoryTheory.IsFiltered (CategoryTheory.StructuredArrow d F)
-- Mathlib.Algebra.Module.Submodule.Map
Submodule.map_comap_le : ∀ {R : Type u_1} {R₂ : Type u_3} {M : Type u_5} {M₂ : Type u_7} [inst : Semiring R] [inst_1 : Semiring R₂]
  [inst_2 : AddCommMonoid M] [inst_3 : AddCommMonoid M₂] [inst_4 : Module R M] [inst_5 : Module R₂ M₂] {σ₁₂ : R →+* R₂}
  [inst_6 : RingHomSurjective σ₁₂] (f : M →ₛₗ[σ₁₂] M₂) (q : Submodule R₂ M₂), Submodule.map f (Submodule.comap f q) ≤ q
-- Mathlib.Combinatorics.Enumerative.IncidenceAlgebra
/-- `mu'` as a bare function defined recursively.  -/
_private.Mathlib.Combinatorics.Enumerative.IncidenceAlgebra.0.IncidenceAlgebra.muFun' : (𝕜 : Type u_2) →
  {α : Type u_5} →
    [AddCommGroup 𝕜] → [One 𝕜] → [inst : Preorder α] → [LocallyFiniteOrder α] → [DecidableEq α] → α → α → 𝕜
-- Mathlib.Topology.Instances.TrivSqZeroExt
/-- `TrivSqZeroExt.snd` as a continuous linear map.  -/
TrivSqZeroExt.sndCLM : (R : Type u_3) →
  (M : Type u_4) →
    [inst : TopologicalSpace R] →
      [inst_1 : TopologicalSpace M] →
        [inst_2 : CommSemiring R] → [inst_3 : AddCommMonoid M] → [inst_4 : Module R M] → TrivSqZeroExt R M →L[R] M
-- Lean.Elab.Tactic.ElabTerm
Lean.Elab.Tactic.evalRename : Lean.Elab.Tactic.Tactic