mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.CategoryTheory.Sites.Over
CategoryTheory.GrothendieckTopology.coverPreserving_over_star : ∀ {C : Type u'} [inst : CategoryTheory.Category.{v_1, u'} C] [inst_1 : CategoryTheory.Limits.HasBinaryProducts C]
  {J : CategoryTheory.GrothendieckTopology C} (X : C),
  CategoryTheory.CoverPreserving J (J.over X) (CategoryTheory.Over.star X)
-- Mathlib.Order.MinMax
lt_min_iff : ∀ {α : Type u} [inst : LinearOrder α] {a b c : α}, a < min b c ↔ a < b ∧ a < c
-- Mathlib.RingTheory.HahnSeries.Summable
HahnSeries.SummableFamily.embDomain_image : ∀ {Γ : Type u_1} {R : Type u_3} {α : Type u_5} {β : Type u_6} [inst : PartialOrder Γ] [inst_1 : AddCommMonoid R]
  (s : HahnSeries.SummableFamily Γ R α) (f : α ↪ β) {a : α}, (s.embDomain f) (f a) = s a
-- Mathlib.MeasureTheory.Function.AEEqFun
MeasureTheory.AEEqFun.instModule : {α : Type u_1} →
  {γ : Type u_3} →
    [inst : MeasurableSpace α] →
      {μ : MeasureTheory.Measure α} →
        [inst_1 : TopologicalSpace γ] →
          {𝕜 : Type u_5} →
            [inst_2 : Semiring 𝕜] →
              [inst_3 : AddCommMonoid γ] →
                [inst_4 : ContinuousAdd γ] → [inst_5 : Module 𝕜 γ] → [ContinuousConstSMul 𝕜 γ] → Module 𝕜 (α →ₘ[μ] γ)
-- Mathlib.Data.ENNReal.Basic
ENNReal.coe_natCast : ∀ (n : ℕ), ↑↑n = ↑n
-- Mathlib.AlgebraicTopology.ModelCategory.BrownLemma
/-- The term in `CofibrantBrownFactorization f` that is deduced from
a factorization of `coprod.desc f (𝟙 Y) : X ⨿ Y ⟶ Y`
as a cofibration followed by a trivial fibration.  -/
HomotopicalAlgebra.CofibrantBrownFactorization.mk' : {C : Type u_1} →
  [inst : CategoryTheory.Category.{v_1, u_1} C] →
    [inst_1 : HomotopicalAlgebra.ModelCategory C] →
      {X Y : C} →
        (f : X ⟶ Y) →
          [HomotopicalAlgebra.IsCofibrant X] →
            [HomotopicalAlgebra.IsCofibrant Y] →
              (HomotopicalAlgebra.cofibrations C).MapFactorizationData (HomotopicalAlgebra.trivialFibrations C)
                  (CategoryTheory.Limits.coprod.desc f (CategoryTheory.CategoryStruct.id Y)) →
                HomotopicalAlgebra.CofibrantBrownFactorization f
-- Mathlib.RingTheory.FractionalIdeal.Operations
FractionalIdeal.ringEquivOfRingEquiv.eq_1 : ∀ {R : Type u_5} {S : Type u_6} (K : Type u_7) (L : Type u_8) [inst : CommRing R] [inst_1 : IsDomain R]
  [inst_2 : CommRing S] [inst_3 : IsDomain S] [inst_4 : CommRing K] [inst_5 : CommRing L] [inst_6 : Algebra R K]
  [inst_7 : Algebra S L] [inst_8 : IsFractionRing R K] [inst_9 : IsFractionRing S L] (f : R ≃+* S),
  FractionalIdeal.ringEquivOfRingEquiv K L f =
    { toFun := fun I => ⟨Submodule.map ↑(IsFractionRing.semilinearEquivOfRingEquiv K L f) ↑I, ⋯⟩,
      invFun := fun J => ⟨Submodule.map ↑(IsFractionRing.semilinearEquivOfRingEquiv L K f.symm) ↑J, ⋯⟩, left_inv := ⋯,
      right_inv := ⋯, map_mul' := ⋯, map_add' := ⋯ }
-- Init.Prelude
/-- An array of syntax elements interspersed with the given separators.

Separator arrays result from repetition operators such as `,*`.
[Coercions](https://lean-lang.org/doc/reference/4.33.0/find/?domain=Verso.Genre.Manual.section&name=coercions) to and from `Array Syntax` insert or remove separators
as required.

The typed equivalent is `Lean.Syntax.TSepArray`.
 -/
Lean.Syntax.SepArray : String → Type
-- Mathlib.Analysis.Normed.Ring.WithAbs
/-- Type synonym for a semiring which depends on an absolute value. This is a function that takes
an absolute value on a semiring and returns the semiring. We use this to assign and infer instances
on a semiring that depend on absolute values.

This is also helpful when dealing with several absolute values on the same semiring.  -/
WithAbs : {R : Type u_1} →
  {S : Type u_2} →
    [inst : Semiring S] → [inst_1 : PartialOrder S] → [inst_2 : Semiring R] → AbsoluteValue R S → Type u_1
-- Mathlib.LinearAlgebra.Multilinear.Basic
MultilinearMap.mkPiRing_apply_one_eq_self : ∀ {R : Type uR} {ι : Type uι} {M₂ : Type v₂} [inst : CommSemiring R] [inst_1 : AddCommMonoid M₂] [inst_2 : Module R M₂]
  [inst_3 : Fintype ι] (f : MultilinearMap R (fun x => R) M₂), MultilinearMap.mkPiRing R ι (f fun x => 1) = f
-- Mathlib.CategoryTheory.Monoidal.Comon_
CategoryTheory.IsCommComonObj.mk : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.MonoidalCategory C]
  [inst_2 : CategoryTheory.BraidedCategory C] {X : C} [inst_3 : CategoryTheory.ComonObj X],
  autoParam
      (CategoryTheory.CategoryStruct.comp CategoryTheory.ComonObj.comul (β_ X X).hom = CategoryTheory.ComonObj.comul)
      CategoryTheory.IsCommComonObj.comul_comm._autoParam →
    CategoryTheory.IsCommComonObj X
-- Mathlib.RingTheory.Localization.Basic
IsLocalization.instSubmonoid : ∀ {R : Type u_1} [inst : CommSemiring R], IsLocalization (IsUnit.submonoid R) R
-- Mathlib.Analysis.CStarAlgebra.ApproximateUnit
/-- The canonical approximate unit in a C⋆-algebra has a basis of sets
`{x | a ≤ x} ∩ closedBall 0 1` for `0 ≤ a`.  -/
CStarAlgebra.hasBasis_approximateUnit : ∀ (A : Type u_1) [inst : NonUnitalCStarAlgebra A] [inst_1 : PartialOrder A] [inst_2 : StarOrderedRing A],
  (CStarAlgebra.approximateUnit A).HasBasis (fun x => 0 ≤ x ∧ ‖x‖ < 1) fun x => {x_1 | x ≤ x_1} ∩ Metric.closedBall 0 1
-- Batteries.Data.Array.Match
_private.Batteries.Data.Array.Match.0.Std.IterStep.successor.match_1.eq_2 : ∀ {α : Type u_1} {β : Type u_2} (motive : Std.IterStep α β → Sort u_3) (it : α)
  (h_1 : (it : α) → (out : β) → motive (Std.IterStep.yield it out)) (h_2 : (it : α) → motive (Std.IterStep.skip it))
  (h_3 : Unit → motive Std.IterStep.done),
  (match Std.IterStep.skip it with
    | Std.IterStep.yield it out => h_1 it out
    | Std.IterStep.skip it => h_2 it
    | Std.IterStep.done => h_3 ()) =
    h_2 it
-- Mathlib.Analysis.Asymptotics.Defs
Asymptotics.IsBigO.sum_congr' : ∀ {α : Type u_1} {E' : Type u_6} [inst : SeminormedAddCommGroup E'] {l : Filter α} {ι : Type u_18} {A : ι → α → E'}
  {B : ι → α → ℝ} {i : α → Finset ι},
  Function.uncurry A =O[⊤ ×ˢ l] Function.uncurry B → (fun H => ∑ j ∈ i H, A j H) =O[l] fun H => ∑ j ∈ i H, ‖B j H‖
-- Std.Sat.AIG.RelabelNat
Std.Sat.AIG.RelabelNat.State.Inv2.upper_lt_size : ∀ {α : Type} [inst : DecidableEq α] [inst_1 : Hashable α] {upper : ℕ} {map : Std.HashMap α ℕ}
  {decls : Array (Std.Sat.AIG.Decl α)}, Std.Sat.AIG.RelabelNat.State.Inv2 decls upper map → upper ≤ decls.size
-- Lean.Meta.Match.MatcherInfo
Lean.Meta.Match.Extension.Entry : Type
-- Mathlib.CategoryTheory.Limits.Shapes.Pullback.Assoc
_private.Mathlib.CategoryTheory.Limits.Shapes.Pullback.Assoc.0.CategoryTheory.Limits.termW'_1 : Lean.ParserDescr
-- Std.Data.DTreeMap.Internal.WF.Defs
Std.DTreeMap.Internal.Impl.WF.below.modify : ∀ {α : Type u} [inst : Ord α] {motive : {β : α → Type v} → (a : Std.DTreeMap.Internal.Impl α β) → a.WF → Prop}
  {x : α → Type v} [inst_1 : Std.LawfulEqOrd α] {t : Std.DTreeMap.Internal.Impl α x} {k : α} {f : x k → x k} (a : t.WF),
  Std.DTreeMap.Internal.Impl.WF.below a → motive t a → Std.DTreeMap.Internal.Impl.WF.below ⋯
-- Mathlib.Dynamics.Ergodic.Function
/-- Let `f : α → α` be a quasi-ergodic map.
Let `g : α → X` be a null-measurable function from `α` to a nonempty measurable space
with a countable family of measurable sets separating the points of `X`.
If `g` is a.e.-invariant under `f`, then `g` is a.e. constant.  -/
QuasiErgodic.ae_eq_const_of_ae_eq_comp₀ : ∀ {α : Type u_1} {X : Type u_2} [inst : MeasurableSpace α] {μ : MeasureTheory.Measure α} [Nonempty X]
  [inst_2 : MeasurableSpace X] [MeasurableSpace.CountablySeparated X] {f : α → α} {g : α → X},
  QuasiErgodic f μ → MeasureTheory.NullMeasurable g μ → g ∘ f =ᵐ[μ] g → ∃ c, g =ᵐ[μ] Function.const α c
-- Mathlib.Logic.Function.Iterate
Function.iterate_add_apply : ∀ {α : Type u} (f : α → α) (m n : ℕ) (x : α), f^[m + n] x = f^[m] (f^[n] x)
-- Mathlib.Combinatorics.Matroid.IndepAxioms
IndepMatroid.ofFinitaryCardAugment.congr_simp : ∀ {α : Type u_1} (E E_1 : Set α) (e_E : E = E_1) (Indep Indep_1 : Set α → Prop) (e_Indep : Indep = Indep_1)
  (indep_empty : Indep ∅) (indep_subset : ∀ ⦃I J : Set α⦄, Indep J → I ⊆ J → Indep I)
  (indep_aug :
    ∀ ⦃I J : Set α⦄, Indep I → I.Finite → Indep J → J.Finite → I.ncard < J.ncard → ∃ e ∈ J, e ∉ I ∧ Indep (insert e I))
  (indep_compact : ∀ (I : Set α), (∀ J ⊆ I, J.Finite → Indep J) → Indep I)
  (subset_ground : ∀ (I : Set α), Indep I → I ⊆ E),
  IndepMatroid.ofFinitaryCardAugment E Indep indep_empty indep_subset indep_aug indep_compact subset_ground =
    IndepMatroid.ofFinitaryCardAugment E_1 Indep_1 ⋯ ⋯ ⋯ ⋯ ⋯
-- Mathlib.Tactic.NormNum.GCD
/-- Given natural number literals `ex` and `ey`, return their GCD as a natural number literal
and an equality proof. Panics if `ex` or `ey` aren't natural number literals.  -/
Mathlib.Meta.NormNum.proveNatGCD : (ex ey : Q(ℕ)) → (ed : Q(ℕ)) × Q(«$ex».gcd «$ey» = «$ed»)
-- Mathlib.Data.Num.Lemmas
PosNum.dvd_to_nat : ∀ {m n : PosNum}, ↑m ∣ ↑n ↔ m ∣ n
-- Mathlib.Order.Interval.Finset.Basic
Finset.Ioc_self : ∀ {α : Type u_2} (a : α) [inst : Preorder α] [inst_1 : LocallyFiniteOrder α], Finset.Ioc a a = ∅
-- Mathlib.CategoryTheory.Endomorphism
CategoryTheory.InducedCategory.endEquiv_symm_apply_hom : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {D : Type u_1} {F : D → C}
  {X : CategoryTheory.InducedCategory C F} (f : F X ⟶ F X), (CategoryTheory.InducedCategory.endEquiv.symm f).hom = f
-- Mathlib.Algebra.Ring.InjSurj
/-- Pushforward a `CommRing` instance along a surjective function.  -/
Function.Surjective.commRing : {R : Type u_1} →
  {S : Type u_2} →
    (f : R → S) →
      Function.Surjective f →
        [inst : Add S] →
          [inst_1 : Mul S] →
            [inst_2 : Zero S] →
              [inst_3 : One S] →
                [inst_4 : Neg S] →
                  [inst_5 : Sub S] →
                    [inst_6 : SMul ℕ S] →
                      [inst_7 : SMul ℤ S] →
                        [inst_8 : Pow S ℕ] →
                          [inst_9 : NatCast S] →
                            [inst_10 : IntCast S] →
                              [inst_11 : CommRing R] →
                                f 0 = 0 →
                                  f 1 = 1 →
                                    (∀ (x y : R), f (x + y) = f x + f y) →
                                      (∀ (x y : R), f (x * y) = f x * f y) →
                                        (∀ (x : R), f (-x) = -f x) →
                                          (∀ (x y : R), f (x - y) = f x - f y) →
                                            (∀ (n : ℕ) (x : R), f (n • x) = n • f x) →
                                              (∀ (n : ℤ) (x : R), f (n • x) = n • f x) →
                                                (∀ (x : R) (n : ℕ), f (x ^ n) = f x ^ n) →
                                                  (∀ (n : ℕ), f ↑n = ↑n) → (∀ (n : ℤ), f ↑n = ↑n) → CommRing S
-- Mathlib.AlgebraicTopology.SimplicialObject.Basic
CategoryTheory.SimplicialObject.Augmented.point_map : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C]
  {Y X :
    CategoryTheory.Comma (CategoryTheory.Functor.id (CategoryTheory.SimplicialObject C))
      (CategoryTheory.SimplicialObject.const C)}
  (f : Y ⟶ X), CategoryTheory.SimplicialObject.Augmented.point.map f = f.right
-- Mathlib.Algebra.Order.Group.Unbundled.Basic
StrictAntiOn.inv : ∀ {α : Type u} {β : Type u_1} [inst : Group α] [inst_1 : Preorder α] [MulLeftStrictMono α] [MulRightStrictMono α]
  [inst_4 : Preorder β] {f : β → α} {s : Set β}, StrictAntiOn f s → StrictMonoOn (fun x => (f x)⁻¹) s
-- Init.Data.List.SplitOn.Basic
_private.Init.Data.List.SplitOn.Basic.0.List.splitOnPTR.go.match_1.splitter : {α : Type u_1} →
  (motive : List α → Array α → Array (List α) → Sort u_2) →
    (x : List α) →
      (x_1 : Array α) →
        (x_2 : Array (List α)) →
          ((acc : Array α) → (r : Array (List α)) → motive [] acc r) →
            ((a : α) → (t : List α) → (acc : Array α) → (r : Array (List α)) → motive (a :: t) acc r) → motive x x_1 x_2
-- Lean.Meta.Tactic.Simp.BuiltinSimprocs.BitVec
/-- Simplification procedure for `setWidth` on `BitVec`s.  -/
BitVec.reduceSetWidth : Lean.Meta.Simp.DSimproc
-- Mathlib.Algebra.NonAssoc.PreLie.Basic
LeftPreLieAlgebra.ext_iff : ∀ {R : Type u_1} {inst : CommRing R} {L : Type u_2} {inst_1 : LeftPreLieRing L} {x y : LeftPreLieAlgebra R L},
  x = y ↔ SMul.smul = SMul.smul
-- Init.Data.AC
Lean.Data.AC.mergeIdem.loop : ℕ → List ℕ → List ℕ
-- Mathlib.Analysis.SpecialFunctions.Sigmoid
DifferentiableAt.sigmoid : ∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] {f : E → ℝ} {x : E},
  DifferentiableAt ℝ f x → DifferentiableAt ℝ (Real.sigmoid ∘ f) x
-- Mathlib.Topology.Sheaves.Module
TopologicalSpace.Opens.overEquivalence.eq_1 : ∀ {X : Type u} [inst : TopologicalSpace X] (U : TopologicalSpace.Opens X),
  U.overEquivalence =
    {
      functor :=
        { obj := fun V => { carrier := Subtype.val ⁻¹' ↑V.left, is_open' := ⋯ },
          map := fun {X_1 Y} f => CategoryTheory.homOfLE ⋯, map_id := ⋯, map_comp := ⋯ },
      inverse :=
        { obj := fun W => CategoryTheory.Over.mk (CategoryTheory.homOfLE ⋯),
          map := fun {X_1 Y} f => CategoryTheory.Over.homMk (CategoryTheory.homOfLE ⋯) ⋯, map_id := ⋯, map_comp := ⋯ },
      unitIso := CategoryTheory.NatIso.ofComponents (fun V => CategoryTheory.Over.isoMk (CategoryTheory.eqToIso ⋯) ⋯) ⋯,
      counitIso := CategoryTheory.NatIso.ofComponents (fun V => CategoryTheory.eqToIso ⋯) ⋯, functor_unitIso_comp := ⋯ }
-- Mathlib.MeasureTheory.Function.ConvergenceInMeasure
MeasureTheory.ExistsSeqTendstoAe.seqTendstoAeSeq.eq_def : ∀ {α : Type u_1} {E : Type u_4} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} [inst : PseudoEMetricSpace E]
  {f : ℕ → α → E} {g : α → E} (hfg : MeasureTheory.TendstoInMeasure μ f Filter.atTop g) (x : ℕ),
  MeasureTheory.ExistsSeqTendstoAe.seqTendstoAeSeq hfg x =
    match x with
    | 0 => MeasureTheory.ExistsSeqTendstoAe.seqTendstoAeSeqAux hfg 0
    | n.succ =>
      max (MeasureTheory.ExistsSeqTendstoAe.seqTendstoAeSeqAux hfg (n + 1))
        (MeasureTheory.ExistsSeqTendstoAe.seqTendstoAeSeq hfg n + 1)
-- Std.Data.DTreeMap.Raw.Lemmas
Std.DTreeMap.Raw.getKeyD_diff_of_not_mem_right : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t₁ t₂ : Std.DTreeMap.Raw α β cmp} [Std.TransCmp cmp],
  t₁.WF → t₂.WF → ∀ {k fallback : α}, k ∉ t₂ → (t₁ \ t₂).getKeyD k fallback = t₁.getKeyD k fallback
-- Mathlib.Analysis.SpecialFunctions.ImproperIntegrals
setIntegral_Ioi_zero_rpow : ∀ (s : ℝ), ∫ (x : ℝ) in Set.Ioi 0, x ^ s = 0
-- Mathlib.MeasureTheory.Group.ModularCharacter
MeasureTheory.Measure.addModularCharacterFun_pos : ∀ {G : Type u_1} [inst : TopologicalSpace G] [inst_1 : AddGroup G] [inst_2 : IsTopologicalAddGroup G]
  [inst_3 : LocallyCompactSpace G] (g : G), 0 < MeasureTheory.Measure.addModularCharacterFun g
-- Mathlib.Data.NNReal.Basic
NNReal.toReal_eq : ∀ (a b : NNReal), a = b ↔ ↑a = ↑b
-- Mathlib.CategoryTheory.Equivalence
CategoryTheory.Equivalence.cancel_unit_right : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  (e : C ≌ D) {X Y : C} (f f' : X ⟶ Y),
  CategoryTheory.CategoryStruct.comp f (e.unit.app Y) = CategoryTheory.CategoryStruct.comp f' (e.unit.app Y) ↔ f = f'
-- Init.Data.SInt.Lemmas
Int32.toNat_toInt : ∀ (x : Int32), x.toInt.toNat = x.toNatClampNeg
-- Mathlib.GroupTheory.CosetCover
AddSubgroup.leftCoset_cover_filter_FiniteIndex : ∀ {G : Type u_1} [inst : AddGroup G] {ι : Type u_2} {H : ι → AddSubgroup G} {g : ι → G} {s : Finset ι},
  ⋃ i ∈ s, g i +ᵥ ↑(H i) = Set.univ →
    ∀ [inst_1 : DecidablePred AddSubgroup.FiniteIndex], ⋃ k ∈ {i ∈ s | (H i).FiniteIndex}, g k +ᵥ ↑(H k) = Set.univ
-- Mathlib.AlgebraicGeometry.EllipticCurve.Affine.Point
WeierstrassCurve.Affine.Point.map_map : ∀ {R : Type r} {S : Type s} {F : Type u} {K : Type v} {L : Type w} [inst : CommRing R] [inst_1 : CommRing S]
  [inst_2 : Field F] [inst_3 : Field K] [inst_4 : Field L] {W' : WeierstrassCurve.Affine R} [inst_5 : DecidableEq F]
  [inst_6 : DecidableEq K] [inst_7 : DecidableEq L] [inst_8 : Algebra R S] [inst_9 : Algebra R F]
  [inst_10 : Algebra S F] [inst_11 : IsScalarTower R S F] [inst_12 : Algebra R K] [inst_13 : Algebra S K]
  [inst_14 : IsScalarTower R S K] [inst_15 : Algebra R L] [inst_16 : Algebra S L] [inst_17 : IsScalarTower R S L]
  (f : F →ₐ[S] K) (g : K →ₐ[S] L) (P : (W'.baseChange F).Point),
  (WeierstrassCurve.Affine.Point.map g) ((WeierstrassCurve.Affine.Point.map f) P) =
    (WeierstrassCurve.Affine.Point.map (g.comp f)) P
-- Mathlib.RingTheory.Valuation.Basic
/-- A ring homomorphism `S → R` induces a map `Valuation R Γ₀ → Valuation S Γ₀`.  -/
Valuation.comap : {R : Type u_3} →
  {Γ₀ : Type u_4} →
    [inst : Ring R] →
      [inst_1 : LinearOrderedCommMonoidWithZero Γ₀] →
        {S : Type u_7} → [inst_2 : Ring S] → (S →+* R) → Valuation R Γ₀ → Valuation S Γ₀
-- Mathlib.CategoryTheory.Limits.Shapes.ZeroMorphisms
/-- A category with a zero object has zero morphisms.

It is rarely a good idea to use this. Many categories that have a zero object have zero
morphisms for some other reason, for example from additivity. Library code that uses
`zeroMorphismsOfZeroObject` will then be incompatible with these categories because
the `HasZeroMorphisms` instances will not be definitionally equal. For this reason library
code should generally ask for an instance of `HasZeroMorphisms` separately, even if it already
asks for an instance of `HasZeroObject`.  -/
CategoryTheory.Limits.IsZero.hasZeroMorphisms : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    {O : C} → CategoryTheory.Limits.IsZero O → CategoryTheory.Limits.HasZeroMorphisms C
-- Init.Data.Rat.Basic
instDecidableEqRat.decEq : (x x_1 : ℚ) → Decidable (x = x_1)
-- Mathlib.CategoryTheory.MorphismProperty.Limits
CategoryTheory.MorphismProperty.instIsStableUnderBaseChangeAlongCompOfHasPullbacksAlong : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] (P : CategoryTheory.MorphismProperty C) {X Y Z : C} (f : X ⟶ Y)
  (g : Y ⟶ Z) [P.IsStableUnderBaseChangeAlong f] [P.IsStableUnderBaseChangeAlong g] [P.HasPullbacksAlong g],
  P.IsStableUnderBaseChangeAlong (CategoryTheory.CategoryStruct.comp f g)
-- Mathlib.Combinatorics.Matroid.Loop
Matroid.isColoop_iff_notMem_closure_compl : ∀ {α : Type u_1} {M : Matroid α} {e : α},
  autoParam (e ∈ M.E) Matroid.isColoop_iff_notMem_closure_compl._auto_1 → (M.IsColoop e ↔ e ∉ M.closure (M.E \ {e}))
-- Mathlib.Order.Interval.Basic
NonemptyInterval.map₂_snd : ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} [inst : Preorder α] [inst_1 : Preorder β] [inst_2 : Preorder γ]
  (f : α → β → γ) (h₀ : ∀ (b : β), Monotone fun a => f a b) (h₁ : ∀ (a : α), Monotone (f a)) (a : NonemptyInterval α)
  (a_1 : NonemptyInterval β), (NonemptyInterval.map₂ f h₀ h₁ a a_1).toProd.2 = f a.toProd.2 a_1.toProd.2
-- Mathlib.MeasureTheory.Group.Measure
/-- An alternative way to prove that `μ` is right invariant under multiplication.  -/
MeasureTheory.forall_measure_preimage_mul_right_iff : ∀ {G : Type u_1} [inst : MeasurableSpace G] [inst_1 : Mul G] [MeasurableMul G] (μ : MeasureTheory.Measure G),
  (∀ (g : G) (A : Set G), MeasurableSet A → μ ((fun h => h * g) ⁻¹' A) = μ A) ↔ μ.IsMulRightInvariant
-- Mathlib.Algebra.Module.PUnit
PUnit.smul.eq_1 : ∀ {R : Type u_1}, PUnit.smul = { smul := fun x x_1 => PUnit.unit }
-- Init.Data.List.Pairwise
List.pairwise_singleton : ∀ {α : Type u_1} (R : α → α → Prop) (a : α), List.Pairwise R [a]
-- Mathlib.Order.ConditionallyCompleteLattice.Defs
ConditionallyCompleteLinearOrder.mk : {α : Type u_5} →
  [toConditionallyCompleteLattice : ConditionallyCompleteLattice α] →
    [toOrd : Ord α] →
      (∀ (a b : α), a ≤ b ∨ b ≤ a) →
        DecidableLE α →
          (toDecidableEq : DecidableEq α) →
            (toDecidableLT : DecidableLT α) →
              (∀ (s : Set α), ¬BddAbove s → sSup s = sSup ∅) →
                (∀ (s : Set α), ¬BddBelow s → sInf s = sInf ∅) →
                  autoParam (∀ (a b : α), compare a b = compareOfLessAndEq a b)
                      ConditionallyCompleteLinearOrder.compare_eq_compareOfLessAndEq._autoParam →
                    ConditionallyCompleteLinearOrder α
-- Std.Sat.AIG.RefVecOperator.Map
Std.Sat.AIG.RefVec.MapTarget.mk : {α : Type} →
  [inst : Hashable α] →
    [inst_1 : DecidableEq α] →
      {aig : Std.Sat.AIG α} →
        {len : ℕ} →
          aig.RefVec len →
            (func : (aig : Std.Sat.AIG α) → aig.Ref → Std.Sat.AIG.Entrypoint α) →
              [lawful : Std.Sat.AIG.LawfulOperator α Std.Sat.AIG.Ref func] →
                [chainable : Std.Sat.AIG.RefVec.LawfulMapOperator α func] → Std.Sat.AIG.RefVec.MapTarget aig len
-- Mathlib.Tactic.TacticAnalysis
/-- Type returned by the `.test` function.  -/
Mathlib.TacticAnalysis.ComplexConfig.out : Mathlib.TacticAnalysis.ComplexConfig → Type
-- Mathlib.Analysis.Distribution.TemperedDistribution
/-- The 1-dimensional derivative on tempered distribution as a continuous `ℂ`-linear map.  -/
TemperedDistribution.derivCLM : (F : Type u_4) →
  [inst : AddCommGroup F] →
    [inst_1 : Module ℂ F] →
      [inst_2 : TopologicalSpace F] →
        [inst_3 : IsTopologicalAddGroup F] →
          [inst_4 : ContinuousConstSMul ℂ F] → TemperedDistribution ℝ F →L[ℂ] TemperedDistribution ℝ F
-- Mathlib.GroupTheory.QuotientGroup.Defs
Con.subgroup.eq_1 : ∀ {G : Type u_1} [inst : Group G] (c : Con G),
  c.subgroup = { carrier := {x | c x 1}, mul_mem' := ⋯, one_mem' := ⋯, inv_mem' := ⋯ }
-- Mathlib.GroupTheory.OreLocalization.Basic
OreLocalization.instInhabited : {R : Type u_1} →
  [inst : Monoid R] → {S : Submonoid R} → [inst_1 : OreLocalization.OreSet S] → Inhabited (OreLocalization S R)
-- Mathlib.Lean.Meta.RefinedDiscrTree.Lookup
_private.Mathlib.Lean.Meta.RefinedDiscrTree.Lookup.0.Lean.Meta.RefinedDiscrTree.setTrie : {α : Type} →
  Lean.Meta.RefinedDiscrTree.TrieIndex → Lean.Meta.RefinedDiscrTree.Trie α → Lean.Meta.RefinedDiscrTree.TreeM✝ α Unit
-- Mathlib.Algebra.Ring.CentroidHom
CentroidHom.neg_apply : ∀ {α : Type u_5} [inst : NonUnitalNonAssocRing α] (f : CentroidHom α) (a : α), (-f) a = -f a
-- Mathlib.AlgebraicTopology.SimplicialSet.Skeleton
/-- Given a monomorphism `i : X ⟶ Y` of simplicial sets and a nondegenerate `d`-simplex
of `Y` not in the range of `i`, this is the inclusion of the corresponding summand
of the coproduct `sigmaStdSimplex i d`.  -/
SSet.relativeCellComplexOfMono.Cell.ιSigmaStdSimplex : {X Y : SSet} →
  {i : X ⟶ Y} →
    {d : ℕ} →
      SSet.relativeCellComplexOfMono.Cell i d →
        (SSet.stdSimplex.obj { len := d } ⟶ SSet.relativeCellComplexOfMono.sigmaStdSimplex i d)
-- Mathlib.Algebra.Group.Defs
inv_mul_cancel_comm : ∀ {G : Type u_1} [inst : CommGroup G] (a b : G), a⁻¹ * b * a = b
-- Mathlib.Algebra.MonoidAlgebra.Basic
/-- Version of `algHom_ext` where both assumptions are written as equalities of bundled homs.  -/
MonoidAlgebra.algHom_ext' : ∀ {R : Type u_1} {A : Type u_4} {B : Type u_5} {M : Type u_7} [inst : CommSemiring R] [inst_1 : Semiring A]
  [inst_2 : Semiring B] [inst_3 : Algebra R A] [inst_4 : Algebra R B] [inst_5 : Monoid M]
  ⦃φ₁ φ₂ : MonoidAlgebra A M →ₐ[R] B⦄,
  (↑φ₁).comp (MonoidAlgebra.of A M) = (↑φ₂).comp (MonoidAlgebra.of A M) →
    φ₁.comp MonoidAlgebra.singleOneAlgHom = φ₂.comp MonoidAlgebra.singleOneAlgHom → φ₁ = φ₂
-- Mathlib.Order.Interval.Finset.Fin
Fin.Ico_add_one_eq_Ioo : ∀ {n : ℕ} {a b : Fin n}, ↑a + 1 < n → Finset.Ico (a + 1) b = Finset.Ioo a b
-- Mathlib.Topology.VectorBundle.Basic
Bundle.Trivialization.continuousLinearMapAt.congr_simp : ∀ (R : Type u_1) {B : Type u_2} {F : Type u_3} {E : B → Type u_4} [inst : NontriviallyNormedField R]
  [inst_1 : (x : B) → AddCommMonoid (E x)] [inst_2 : (x : B) → Module R (E x)] [inst_3 : NormedAddCommGroup F]
  [inst_4 : NormedSpace R F] [inst_5 : TopologicalSpace B] [inst_6 : TopologicalSpace (Bundle.TotalSpace F E)]
  [inst_7 : (x : B) → TopologicalSpace (E x)] [inst_8 : FiberBundle F E]
  (e e_1 : Bundle.Trivialization F Bundle.TotalSpace.proj) (e_e : e = e_1) [inst_9 : Bundle.Trivialization.IsLinear R e]
  (b : B), Bundle.Trivialization.continuousLinearMapAt R e b = Bundle.Trivialization.continuousLinearMapAt R e_1 b