mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.MeasureTheory.Measure.Count
MeasureTheory.Measure.count_singleton' : ∀ {α : Type u_1} [inst : MeasurableSpace α] {a : α}, MeasurableSet {a} → MeasureTheory.Measure.count {a} = 1
-- Mathlib.Algebra.Homology.Embedding.TruncGEHomology
HomologicalComplex.truncGE'.hasHomology_of_not_mem_boundary : ∀ {ι : Type u_1} {ι' : Type u_2} {c : ComplexShape ι} {c' : ComplexShape ι'} {C : Type u_3}
  [inst : CategoryTheory.Category.{v_1, u_3} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  (K : HomologicalComplex C c') (e : c.Embedding c') [inst_2 : e.IsTruncGE] [inst_3 : ∀ (i' : ι'), K.HasHomology i']
  (j : ι), ¬e.BoundaryGE j → (K.truncGE' e).HasHomology j
-- Mathlib.CategoryTheory.Limits.Shapes.IsTerminal
/-- Any two morphisms from an initial object are equal.  -/
CategoryTheory.Limits.IsInitial.hom_ext : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {X Y : C} (t : CategoryTheory.Limits.IsInitial X)
  (f g : X ⟶ Y), f = g
-- Std.Tactic.Do.Syntax
/-- `mhave` is like `have`, but operating on a stateful `Std.Do.SPred` goal.
```lean
example (P Q : SPred σs) : P ⊢ₛ (P → Q) → Q := by
  mintro HP HPQ
  mhave HQ : Q := by mspecialize HPQ HP; mexact HPQ
  mexact HQ
```
 -/
Lean.Parser.Tactic.mhaveError : Lean.ParserDescr
-- LeanSearchClient.Syntax
LeanSearchClient.SearchServer.getTermSuggestions : LeanSearchClient.SearchServer → String → ℕ → Lean.MetaM (Array Lean.Meta.Tactic.TryThis.Suggestion)
-- Mathlib.GroupTheory.Torsion
IsAddTorsion.addGroup.eq_1 : ∀ {G : Type u_1} [inst : AddMonoid G] (tG : IsAddTorsion G),
  tG.addGroup =
    { toAddMonoid := inst, neg := fun g => (addOrderOf g - 1) • g, sub := SubNegMonoid.sub', zsmul := zsmulRec,
      sub_eq_add_neg := ⋯, zsmul_zero' := ⋯, zsmul_succ' := ⋯, zsmul_neg' := ⋯, neg_add_cancel := ⋯ }
-- Mathlib.SetTheory.Cardinal.Aleph
Cardinal.beth_ofNat_lt_lift : ∀ {c : Cardinal.{u}} {n : ℕ} [inst : n.AtLeastTwo],
  Cardinal.beth (OfNat.ofNat n) < Cardinal.lift.{v, u} c ↔ Cardinal.beth (OfNat.ofNat n) < c
-- Mathlib.LinearAlgebra.Quotient.Basic
Submodule.factor_mk : ∀ {R : Type u_1} {M : Type u_2} [inst : Ring R] [inst_1 : AddCommGroup M] [inst_2 : Module R M] {p p' : Submodule R M}
  (H : p ≤ p') (x : M), (Submodule.factor H) (p.mkQ x) = p'.mkQ x
-- Mathlib.Topology.OpenPartialHomeomorph.Defs
OpenPartialHomeomorph.coe_toPartialEquiv : ∀ {X : Type u_1} {Y : Type u_3} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y]
  (e : OpenPartialHomeomorph X Y), ↑e.toPartialEquiv = ↑e
-- Mathlib.RingTheory.Ideal.Quotient.Operations
/-- The induced algebra morphism from the quotient by the kernel is injective.  -/
Ideal.kerLiftAlg_injective : ∀ {R₁ : Type u_1} {A : Type u_3} {B : Type u_4} [inst : CommSemiring R₁] [inst_1 : Ring A] [inst_2 : Algebra R₁ A]
  [inst_3 : Semiring B] [inst_4 : Algebra R₁ B] (f : A →ₐ[R₁] B), Function.Injective ⇑(Ideal.kerLiftAlg f)
-- Init.Data.Float.Float32
/-- Compares two floating point numbers for strict inequality.

This function does not reduce in the kernel. It is compiled to the C inequality operator.
 -/
Float32.decLt : (a b : Float32) → Decidable (a < b)
-- Mathlib.Data.TypeVec
TypeVec.lastFun_splitFun : ∀ {n : ℕ} {α : TypeVec.{u_1} (n + 1)} {α' : TypeVec.{u_2} (n + 1)} (f : α.drop.Arrow α'.drop) (g : α.last → α'.last),
  TypeVec.lastFun (TypeVec.splitFun f g) = g
-- Mathlib.Data.Vector.Basic
/-- The `List` of a vector after a `reverse`, retrieved by `toList` is equal
to the `List.reverse` after retrieving a vector's `toList`.  -/
List.Vector.toList_reverse : ∀ {α : Type u_1} {n : ℕ} {v : List.Vector α n}, v.reverse.toList = v.toList.reverse
-- Init.Data.UInt.Bitwise
UInt16.toUInt64_xor : ∀ (a b : UInt16), (a ^^^ b).toUInt64 = a.toUInt64 ^^^ b.toUInt64
-- Mathlib.RingTheory.DedekindDomain.AdicValuation
IsDedekindDomain.HeightOneSpectrum.intValuation_if_neg : ∀ {R : Type u_1} [inst : CommRing R] [inst_1 : IsDedekindDomain R] (v : IsDedekindDomain.HeightOneSpectrum R) {r : R},
  r ≠ 0 → v.intValuation r = WithZero.exp (-↑((Associates.mk v.asIdeal).count (Associates.mk (Ideal.span {r})).factors))
-- Mathlib.Algebra.Notation.Prod
Prod.mk_mul_mk : ∀ {M : Type u_8} {N : Type u_9} [inst : Mul M] [inst_1 : Mul N] (a₁ a₂ : M) (b₁ b₂ : N),
  (a₁, b₁) * (a₂, b₂) = (a₁ * a₂, b₁ * b₂)
-- Mathlib.Topology.Algebra.AsymptoticCone
AffineSpace.asymptoticNhds_bind_nhds : ∀ {k : Type u_1} {V : Type u_2} {P : Type u_3} [inst : Field k] [inst_1 : LinearOrder k] [inst_2 : AddCommGroup V]
  [inst_3 : Module k V] [inst_4 : AddTorsor V P] [inst_5 : TopologicalSpace V] [inst_6 : TopologicalSpace k]
  [OrderTopology k] [IsStrictOrderedRing k] [IsTopologicalAddGroup V] [ContinuousSMul k V]
  [inst_11 : TopologicalSpace P] [IsTopologicalAddTorsor P] (v : V),
  (AffineSpace.asymptoticNhds k P v).bind nhds = AffineSpace.asymptoticNhds k P v
-- Std.Sat.AIG.LawfulVecOperator
Std.Sat.AIG.LawfulVecOperator.le_size : ∀ {α : Type} {inst : Hashable α} {inst_1 : DecidableEq α} {β : Std.Sat.AIG α → ℕ → Type}
  {f : {len : ℕ} → (aig : Std.Sat.AIG α) → β aig len → Std.Sat.AIG.RefVecEntry α len}
  [self : Std.Sat.AIG.LawfulVecOperator α β f] {len : ℕ} (aig : Std.Sat.AIG α) (input : β aig len),
  aig.decls.size ≤ (f aig input).aig.decls.size
-- Mathlib.CategoryTheory.Functor.EpiMono
CategoryTheory.Functor.PreservesEpimorphisms.of_natTrans : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  {F G : CategoryTheory.Functor C D} [F.PreservesEpimorphisms] (f : F ⟶ G) [∀ (X : C), CategoryTheory.Epi (f.app X)],
  G.PreservesEpimorphisms
-- Mathlib.Data.List.Defs
/-- Notation for calculating the product of a `List`  -/
List.instSProd : {α : Type u_1} → {β : Type u_2} → SProd (List α) (List β) (List (α × β))
-- Mathlib.Algebra.Free
FreeMagma.length.eq_def : ∀ {α : Type u} (x : FreeMagma α),
  x.length =
    match x with
    | FreeMagma.of _x => 1
    | x.mul y => x.length + y.length
-- Mathlib.Algebra.Group.Equiv.Opposite
/-- The 'unopposite' of a monoid homomorphism `Mᵐᵒᵖ →* Nᵐᵒᵖ`. Inverse to `MonoidHom.op`.  -/
MonoidHom.unop : {M : Type u_3} → {N : Type u_4} → [inst : MulOneClass M] → [inst_1 : MulOneClass N] → (Mᵐᵒᵖ →* Nᵐᵒᵖ) ≃ (M →* N)
-- Mathlib.ModelTheory.LanguageMap
/-- Extends a language with a constant for each element of a parameter set in `M`.  -/
FirstOrder.«term_[[_]]» : Lean.TrailingParserDescr
-- Mathlib.RingTheory.AdjoinRoot
AdjoinRoot.powerBasisAux'_repr_symm_apply : ∀ {R : Type u_1} [inst : CommRing R] {g : Polynomial R} (hg : g.Monic) (c : Fin g.natDegree →₀ R),
  (AdjoinRoot.powerBasisAux' hg).repr.symm c = (AdjoinRoot.mk g) (∑ i, (Polynomial.monomial ↑i) (c i))
-- Init.Data.BitVec.Bitblast
BitVec.toInt_dvd_toInt_iff_of_msb_false_msb_true : ∀ {w : ℕ} {x y : BitVec w}, x.msb = false → y.msb = true → (y.toInt ∣ x.toInt ↔ x % -y = 0#w)
-- Mathlib.Algebra.GCDMonoid.Basic
/-- The proposition that `normUnit` maps units to their inverses.  -/
StrongNormalizationMonoid.normUnit_coe_units : ∀ {α : Type u_2} {inst : CommMonoidWithZero α} [self : StrongNormalizationMonoid α] (u : αˣ), normUnit ↑u = u⁻¹
-- Mathlib.Order.ConditionallyCompleteLattice.Indexed
WithBot.coe_iSup : ∀ {α : Type u_1} {ι : Sort u_4} [inst : Preorder α] [Nonempty ι] [inst_2 : SupSet α] {f : ι → α},
  BddAbove (Set.range f) → ↑(⨆ i, f i) = ⨆ i, ↑(f i)
-- Mathlib.Logic.Equiv.Basic
Equiv.piComm_apply : ∀ {α : Sort u_1} {β : Sort u_4} (φ : α → β → Sort u_9) (f : (x : α) → (y : β) → φ x y) (y : β) (x : α),
  (Equiv.piComm φ) f y x = Function.swap f y x
-- Mathlib.Data.Set.Image
Function.Involutive.preimage : ∀ {α : Type u_1} {f : α → α}, Function.Involutive f → Function.Involutive (Set.preimage f)
-- Mathlib.NumberTheory.LSeries.Basic
/-- If the `LSeries` of `f` is summable at `s`, then `f n` is bounded in absolute value
by a constant times `n^(re s)`.  -/
LSeriesSummable.le_const_mul_rpow : ∀ {f : ℕ → ℂ} {s : ℂ}, LSeriesSummable f s → ∃ C, ∀ (n : ℕ), n ≠ 0 → ‖f n‖ ≤ C * ↑n ^ s.re
-- Mathlib.Algebra.Lie.Extension
/-- The middle object in the sequence.  -/
LieAlgebra.Extension.L : {R : Type u_1} →
  {N : Type u_2} →
    {M : Type u_4} →
      [inst : CommRing R] →
        [inst_1 : LieRing N] →
          [inst_2 : LieAlgebra R N] →
            [inst_3 : LieRing M] → [inst_4 : LieAlgebra R M] → LieAlgebra.Extension R N M → Type u_5
-- Mathlib.Algebra.Module.Equiv.Defs
LinearEquiv.trans_apply : ∀ {R₁ : Type u_2} {R₂ : Type u_3} {R₃ : Type u_4} {M₁ : Type u_8} {M₂ : Type u_9} {M₃ : Type u_10} [inst : Semiring R₁]
  [inst_1 : Semiring R₂] [inst_2 : Semiring R₃] [inst_3 : AddCommMonoid M₁] [inst_4 : AddCommMonoid M₂]
  [inst_5 : AddCommMonoid M₃] {module_M₁ : Module R₁ M₁} {module_M₂ : Module R₂ M₂} {module_M₃ : Module R₃ M₃}
  {σ₁₂ : R₁ →+* R₂} {σ₂₁ : R₂ →+* R₁} {σ₁₃ : R₁ →+* R₃} {σ₃₁ : R₃ →+* R₁} [inst_6 : RingHomInvPair σ₁₃ σ₃₁]
  [inst_7 : RingHomInvPair σ₃₁ σ₁₃] {σ₂₃ : R₂ →+* R₃} {σ₃₂ : R₃ →+* R₂} {re₁₂ : RingHomInvPair σ₁₂ σ₂₁}
  {re₂₁ : RingHomInvPair σ₂₁ σ₁₂} {re₂₃ : RingHomInvPair σ₂₃ σ₃₂} {re₃₂ : RingHomInvPair σ₃₂ σ₂₃}
  [inst_8 : RingHomCompTriple σ₁₂ σ₂₃ σ₁₃] [inst_9 : RingHomCompTriple σ₃₂ σ₂₁ σ₃₁] {e₁₂ : M₁ ≃ₛₗ[σ₁₂] M₂}
  {e₂₃ : M₂ ≃ₛₗ[σ₂₃] M₃} (c : M₁), (e₁₂.trans e₂₃) c = e₂₃ (e₁₂ c)
-- Mathlib.Algebra.Order.AddGroupWithTop
IsAddRegular.of_ne_top : ∀ {α : Type u_2} [inst : LinearOrderedAddCommMonoidWithTop α] {a : α}, a ≠ ⊤ → IsAddRegular a
-- Mathlib.CategoryTheory.Localization.SmallHom
/-- The formal inverse in `SmallHom W X Y` of a morphism `f : Y ⟶ X` such that `W f`.  -/
CategoryTheory.Localization.SmallHom.mkInv : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    {W : CategoryTheory.MorphismProperty C} →
      {X Y : C} →
        (f : Y ⟶ X) →
          W f →
            [inst_1 : CategoryTheory.Localization.HasSmallLocalizedHom W X Y] →
              CategoryTheory.Localization.SmallHom W X Y
-- Mathlib.Algebra.MvPolynomial.Basic
MvPolynomial.X_mul_cancel_left_iff : ∀ {R : Type u} {σ : Type u_1} [inst : CommSemiring R] {p q : MvPolynomial σ R} {i : σ},
  MvPolynomial.X i * p = MvPolynomial.X i * q ↔ p = q
-- Lean.Meta.Tactic.Grind.Main
_private.Lean.Meta.Tactic.Grind.Main.0.Lean.Meta.Grind.initENodeCore : Lean.Expr → Bool → Bool → Lean.Meta.Grind.GoalM Unit
-- Mathlib.RingTheory.IntegralClosure.IntegralRestrict
galRestrict.congr_simp : ∀ (A : Type u_1) (K : Type u_2) (L : Type u_3) (B : Type u_6) [inst : CommRing A] [inst_1 : CommRing B]
  [inst_2 : Algebra A B] [inst_3 : Field K] [inst_4 : Field L] [inst_5 : Algebra A K] [inst_6 : IsFractionRing A K]
  [inst_7 : Algebra K L] [inst_8 : Algebra A L] [inst_9 : IsScalarTower A K L] [inst_10 : Algebra B L]
  [inst_11 : IsScalarTower A B L] [inst_12 : IsIntegralClosure B A L] [inst_13 : Algebra.IsAlgebraic K L],
  galRestrict A K L B = galRestrict A K L B
-- Mathlib.SetTheory.Cardinal.Arithmetic
Cardinal.mul_le_of_le : ∀ {a b c : Cardinal.{u_1}}, Cardinal.aleph0 ≤ c → a ≤ c → b ≤ c → a * b ≤ c
-- Mathlib.Order.Filter.AtTopBot.CompleteLattice
/-- If `f` is a monotone function taking values in a conditionally complete linear order
and `g` tends to `atBot` along a nontrivial filter,
then the indexed infimum of `f ∘ g` is equal to the indexed infimum of `f`.  -/
Monotone.ciInf_comp_tendsto_atBot_of_linearOrder : ∀ {α : Type u_3} {β : Type u_4} {γ : Type u_5} [inst : Preorder β] [inst_1 : ConditionallyCompleteLinearOrder γ]
  {l : Filter α} [l.NeBot] {f : β → γ},
  Monotone f → ∀ {g : α → β}, Filter.Tendsto g l Filter.atBot → ⨅ a, f (g a) = ⨅ b, f b
-- Mathlib.Data.Set.Basic
Set.subset_iff_notMem : ∀ {α : Type u} {s t : Set α}, s ⊆ t ↔ ∀ ⦃a : α⦄, a ∉ t → a ∉ s
-- Mathlib.Algebra.DualQuaternion
Quaternion.re_snd_dualNumberEquiv : ∀ {R : Type u_1} [inst : CommRing R] (q : Quaternion (DualNumber R)),
  (TrivSqZeroExt.snd (Quaternion.dualNumberEquiv q)).re = TrivSqZeroExt.snd q.re
-- Mathlib.CategoryTheory.Abelian.GrothendieckAxioms.Basic
/-- A category with finite biproducts and finite limits has countable AB4 if sequential colimits are
exact.
 -/
CategoryTheory.CountableAB4.of_countableAB5 : ∀ (C : Type u) [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  [CategoryTheory.Limits.HasFiniteBiproducts C] [CategoryTheory.Limits.HasFiniteLimits C]
  [inst_4 : CategoryTheory.Limits.HasColimitsOfShape ℕ C] [CategoryTheory.HasExactColimitsOfShape ℕ C]
  [inst_6 : CategoryTheory.Limits.HasCountableCoproducts C], CategoryTheory.CountableAB4 C
-- Mathlib.CategoryTheory.Adjunction.Basic
/-- Equality of the composition of the unit and counit with the identity `G ⟶ GFG ⟶ G = 𝟙`  -/
CategoryTheory.Adjunction.right_triangle_components : ∀ {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} (self : F ⊣ G) (Y : D),
  CategoryTheory.CategoryStruct.comp (self.unit.app (G.obj Y)) (G.map (self.counit.app Y)) =
    CategoryTheory.CategoryStruct.id (G.obj Y)
-- Mathlib.Algebra.Ring.Defs
/-- A domain is a nontrivial semiring such that multiplication by a nonzero element
is cancellative on both sides. In other words, a nontrivial semiring `R` satisfying
`∀ {a b c : R}, a ≠ 0 → a * b = a * c → b = c` and
`∀ {a b c : R}, b ≠ 0 → a * b = c * b → a = c`.

This is implemented as a mixin for `Semiring α`.
To obtain an integral domain use `[CommRing α] [IsDomain α]`.  -/
IsDomain : (α : Type u) → [Semiring α] → Prop
-- Std.Data.DTreeMap.Internal.WF.Lemmas
Std.DTreeMap.Internal.Impl.Const.alter_eq_alter! : ∀ {α : Type u} {β : Type v} [inst : Ord α] {t : Std.DTreeMap.Internal.Impl α fun x => β} {a : α}
  {f : Option β → Option β} (htb : t.Balanced),
  (Std.DTreeMap.Internal.Impl.Const.alter a f t htb).impl = Std.DTreeMap.Internal.Impl.Const.alter! a f t
-- Mathlib.MeasureTheory.SetSemiring
_private.Mathlib.MeasureTheory.SetSemiring.0.Set.Ioc_mem_ofPred_Ioc_le : ∀ {α : Type u_1} [inst : LinearOrder α] (u v : α), Set.Ioc u v ∈ {s | ∃ u v, u ≤ v ∧ s = Set.Ioc u v}
-- Std.Data.TreeMap.Lemmas
Std.TreeMap.foldr_eq_foldr_keysArray : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Std.TreeMap α β cmp} {δ : Type w} {f : α → δ → δ} {init : δ},
  Std.TreeMap.foldr (fun a x d => f a d) init t = Array.foldr f init t.keysArray
-- Mathlib.RingTheory.IntegralClosure.IsIntegralClosure.Basic
IsIntegral.sum : ∀ {R : Type u_1} {A : Type u_2} [inst : CommRing R] [inst_1 : CommRing A] [inst_2 : Algebra R A] {α : Type u_5}
  {s : Finset α} (f : α → A), (∀ x ∈ s, IsIntegral R (f x)) → IsIntegral R (∑ x ∈ s, f x)
-- Std.Data.TreeSet.Raw.Lemmas
Std.TreeSet.Raw.get?_eq_some_getD_of_contains : ∀ {α : Type u} {cmp : α → α → Ordering} {t : Std.TreeSet.Raw α cmp} [Std.TransCmp cmp],
  t.WF → ∀ {a fallback : α}, t.contains a = true → t.get? a = some (t.getD a fallback)
-- Mathlib.GroupTheory.Focal
AddSubgroup.addCommutator_le_focalAddSubgroup : ∀ {G : Type u_1} [inst : AddGroup G] (H : AddSubgroup G), ⁅H, H⁆ ≤ H.focalAddSubgroup
-- Mathlib.CategoryTheory.Limits.HasLimits
/-- All `F : J ⥤ C` have colimits for all small `J`  -/
CategoryTheory.Limits.HasColimitsOfSize.has_colimits_of_shape : ∀ {C : Type u} {inst : CategoryTheory.Category.{v, u} C}
  [self : CategoryTheory.Limits.HasColimitsOfSize.{v₁, u₁, v, u} C] (J : Type u₁)
  [inst_1 : CategoryTheory.Category.{v₁, u₁} J], CategoryTheory.Limits.HasColimitsOfShape J C
-- Mathlib.Topology.Algebra.Module.Alternating.Topology
/-- Given a continuous linear map taking values in the space of continuous multilinear maps
such that all of its values are alternating maps,
lift it to a continuous linear map taking values in the space of continuous alternating maps.  -/
ContinuousAlternatingMap.liftCLM : {𝕜 : Type u_1} →
  {E : Type u_2} →
    {F : Type u_3} →
      {ι : Type u_4} →
        [inst : NormedField 𝕜] →
          [inst_1 : AddCommGroup E] →
            [inst_2 : Module 𝕜 E] →
              [inst_3 : TopologicalSpace E] →
                [inst_4 : AddCommGroup F] →
                  [inst_5 : Module 𝕜 F] →
                    [inst_6 : TopologicalSpace F] →
                      [inst_7 : IsTopologicalAddGroup F] →
                        {G : Type u_5} →
                          [inst_8 : AddCommGroup G] →
                            [inst_9 : Module 𝕜 G] →
                              [inst_10 : TopologicalSpace G] →
                                [inst_11 : ContinuousConstSMul 𝕜 F] →
                                  (f : G →L[𝕜] ContinuousMultilinearMap 𝕜 (fun x => E) F) →
                                    (∀ (x : G) (v : ι → E) (i j : ι), v i = v j → i ≠ j → (f x) v = 0) →
                                      G →L[𝕜] E [⋀^ι]→L[𝕜] F
-- Mathlib.NumberTheory.NumberField.InfinitePlace.Basic
NumberField.InfinitePlace.norm_embedding_of_isReal : ∀ {K : Type u_1} [inst : Field K] {w : NumberField.InfinitePlace K} (hw : w.IsReal) (x : K),
  ‖(NumberField.InfinitePlace.embedding_of_isReal hw) x‖ = w x
-- Mathlib.CategoryTheory.Limits.Shapes.Pullback.IsPullback.Basic
CategoryTheory.IsPullback.mono_fst_of_mono : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {P X Y Z : C} {fst : P ⟶ X} {snd : P ⟶ Y} {f : X ⟶ Z}
  {g : Y ⟶ Z},
  CategoryTheory.IsPullback fst snd f g →
    autoParam (CategoryTheory.Mono g) CategoryTheory.IsPullback.mono_fst_of_mono._auto_1 → CategoryTheory.Mono fst
-- Lean.Elab.PreDefinition.TerminationHint
Lean.Elab.instInhabitedPartialFixpoint.default : Lean.Elab.PartialFixpoint
-- Mathlib.MeasureTheory.MeasurableSpace.Embedding
MeasurableEquiv.piFinSuccAbove_symm_apply : ∀ {n : ℕ} (α : Fin (n + 1) → Type u_8) [inst : (i : Fin (n + 1)) → MeasurableSpace (α i)] (i : Fin (n + 1)),
  ⇑(MeasurableEquiv.piFinSuccAbove α i).symm = ⇑(Fin.insertNthEquiv α i)
-- Mathlib.RingTheory.Ideal.Maps
Ideal.le_comap_sup : ∀ {R : Type u} {S : Type v} {F : Type u_1} [inst : Semiring R] [inst_1 : Semiring S] [inst_2 : FunLike F R S] (f : F)
  {K L : Ideal S} [inst_3 : RingHomClass F R S], Ideal.comap f K ⊔ Ideal.comap f L ≤ Ideal.comap f (K ⊔ L)
-- Lean.Meta.Tactic.Simp.Types
Lean.Meta.Simp.withParent : {α : Type} → Lean.Expr → Lean.Meta.SimpM α → Lean.Meta.SimpM α
-- Init.Data.List.Basic
List.modifyTailIdx_zero : ∀ {α : Type u} {f : List α → List α} {l : List α}, l.modifyTailIdx 0 f = f l
-- Mathlib.CategoryTheory.Bicategory.Functor.StrictPseudofunctor
CategoryTheory.StrictPseudofunctor.mapComp_eq_eqToIso : ∀ {B : Type u₁} [inst : CategoryTheory.Bicategory B] {C : Type u₂} [inst_1 : CategoryTheory.Bicategory C]
  (self : CategoryTheory.StrictPseudofunctor B C) {a b c : B} (f : a ⟶ b) (g : b ⟶ c),
  self.mapComp f g = CategoryTheory.eqToIso ⋯
-- Mathlib.MeasureTheory.Integral.Bochner.Basic
MeasureTheory.integral_eq_iff_of_ae_le : ∀ {α : Type u_1} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} {f g : α → ℝ},
  MeasureTheory.Integrable f μ →
    MeasureTheory.Integrable g μ → f ≤ᵐ[μ] g → (∫ (a : α), f a ∂μ = ∫ (a : α), g a ∂μ ↔ f =ᵐ[μ] g)
-- Mathlib.Geometry.RingedSpace.Basic
/-- The basic open of a section `f` is the set of all points `x`, such that the germ of `f` at
`x` is a unit.
 -/
AlgebraicGeometry.RingedSpace.basicOpen : (X : AlgebraicGeometry.RingedSpace) →
  {U : TopologicalSpace.Opens ↑↑X.toPresheafedSpace} →
    ↑(X.presheaf.obj (Opposite.op U)) → TopologicalSpace.Opens ↑↑X.toPresheafedSpace
-- Mathlib.Probability.Kernel.Composition.Prod
ProbabilityTheory.Kernel.prod.eq_1 : ∀ {α : Type u_1} {β : Type u_2} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} {γ : Type u_4}
  {mγ : MeasurableSpace γ} (κ : ProbabilityTheory.Kernel α β) (η : ProbabilityTheory.Kernel α γ),
  κ.prod η = (κ.parallelComp η).comp (ProbabilityTheory.Kernel.copy α)
-- Init.Grind.Config
Lean.Grind.Config.mk : Bool →
  Bool →
    Bool →
      Bool →
        Bool →
          ℕ →
            ℕ →
              ℕ →
                ℕ →
                  ℕ →
                    Bool →
                      Bool →
                        Bool →
                          Bool →
                            Bool →
                              ℕ →
                                Bool →
                                  Bool →
                                    Bool →
                                      Bool →
                                        Bool →
                                          Bool →
                                            Bool →
                                              Bool →
                                                Bool →
                                                  Bool →
                                                    Bool →
                                                      Bool →
                                                        ℕ →
                                                          ℕ →
                                                            Bool →
                                                              Bool →
                                                                ℕ →
                                                                  Bool →
                                                                    ℕ →
                                                                      ℕ →
                                                                        Bool →
                                                                          Bool →
                                                                            Bool →
                                                                              ℕ →
                                                                                ℕ →
                                                                                  Bool →
                                                                                    Bool →
                                                                                      Bool →
                                                                                        Bool →
                                                                                          Option ℕ → Lean.Grind.Config
-- Init.Data.Iterators.Lemmas.Combinators.Monadic.FilterMap
Std.IterM.anyM_filter : ∀ {α β : Type w} {m : Type w → Type w'} [inst : Std.Iterator α m β] [Std.Iterators.Finite α m] [inst_2 : Monad m]
  [inst_3 : Std.IteratorLoop α m m] [LawfulMonad m] [Std.LawfulIteratorLoop α m m] {it : Std.IterM m β} {f : β → Bool}
  {p : β → m (ULift.{w, 0} Bool)},
  Std.IterM.anyM p (Std.IterM.filter f it) =
    Std.IterM.anyM (fun x => if f x = true then p x else pure { down := false }) it
-- Std.Internal.UV.System
Std.Internal.UV.System.RUsage.systemTime : Std.Internal.UV.System.RUsage → UInt64
-- Mathlib.Topology.Algebra.Ring.Basic
NonUnitalSubsemiring.instIsSemitopologicalSemiring : ∀ {R : Type u_1} [inst : TopologicalSpace R] [inst_1 : NonUnitalSemiring R] [IsSemitopologicalSemiring R]
  (S : NonUnitalSubsemiring R), IsSemitopologicalSemiring ↥S
-- Lean.Elab.PreDefinition.WF.Fix
/-- The subgoals, created by `mkDecreasingProof`, are of the form `[data _recApp: rel arg param]`, where
`param` is the `PackMutual`'ed parameter of the current function, and thus we can peek at that to
know which function is making the call.
The close coupling with how arguments are packed and termination goals look like is not great,
but it works for now.
 -/
Lean.Elab.WF.groupGoalsByFunction : Lean.Meta.ArgsPacker → ℕ → Array Lean.MVarId → Lean.MetaM (Array (Array Lean.MVarId))
-- Mathlib.Algebra.Star.Basic
Nat.instStarRing : StarRing ℕ
-- Mathlib.Combinatorics.SimpleGraph.Basic
SimpleGraph.neighborSet_compl : ∀ {V : Type u} (G : SimpleGraph V) (v : V), Gᶜ.neighborSet v = (G.neighborSet v)ᶜ \ {v}
-- Mathlib.Algebra.CharP.Basic
/-- Characteristic `≠ 2` in a domain implies that `-a = a` iff `a = 0`.  -/
Ring.eq_self_iff_eq_zero_of_char_ne_two : ∀ {R : Type u_2} [inst : NonAssocRing R] [Nontrivial R] [NoZeroDivisors R], ringChar R ≠ 2 → ∀ {a : R}, -a = a ↔ a = 0
-- Mathlib.Order.Interval.Set.UnorderedInterval
Set.uIcc_of_le : ∀ {α : Type u_1} [inst : Lattice α] {a b : α}, a ≤ b → Set.uIcc a b = Set.Icc a b
-- Init.ByCases
/-- `by_cases (h :)? p` splits the main goal into two cases, assuming `h : p` in the first branch, and `h : ¬ p` in the second branch.
 -/
«tacticBy_cases_:_» : Lean.ParserDescr