mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Topology.Algebra.Nonarchimedean.AdicTopology
Ideal.hasBasis_nhds_adic : ∀ {R : Type u_1} [inst : CommRing R] (I : Ideal R) (x : R),
  (nhds x).HasBasis (fun _n => True) fun n => (fun y => x + y) '' ↑(I ^ n)
-- Mathlib.RingTheory.Ideal.Quotient.HasFiniteQuotients
/-- A domain that is finitely generated has finite quotients.  -/
Ring.HasFiniteQuotients.instOfIsDomainOfFiniteInt : ∀ {R : Type u_1} [inst : CommRing R] [IsDomain R] [Module.Finite ℤ R], Ring.HasFiniteQuotients R
-- Lean.Message
/-- Returns the top-level tag of the message.
If none, returns `Name.anonymous`.

This does not descend into message subtrees (e.g., `.compose`, `.ofLazy`).
The message kind is expected to describe the whole message.
 -/
Lean.Message.kind : Lean.Message → Lean.Name
-- Std.Data.DTreeMap.Internal.Model
Std.DTreeMap.Internal.Impl.explore.eq_def : ∀ {α : Type u} {β : α → Type v} {γ : Type w} [inst : Ord α] (k : α → Ordering) (init : γ)
  (inner : γ → Std.DTreeMap.Internal.Impl.ExplorationStep α β k → γ) (l : Std.DTreeMap.Internal.Impl α β),
  Std.DTreeMap.Internal.Impl.explore k init inner l =
    match l with
    | Std.DTreeMap.Internal.Impl.leaf =>
      inner init (Std.DTreeMap.Internal.Impl.ExplorationStep.eq [] Std.DTreeMap.Internal.Cell.empty [])
    | Std.DTreeMap.Internal.Impl.inner size ky y l r =>
      match h : k ky with
      | Ordering.lt =>
        Std.DTreeMap.Internal.Impl.explore k
          (inner init (Std.DTreeMap.Internal.Impl.ExplorationStep.lt ky h y r.toListModel)) inner l
      | Ordering.eq =>
        inner init
          (Std.DTreeMap.Internal.Impl.ExplorationStep.eq l.toListModel (Std.DTreeMap.Internal.Cell.ofEq ky y ⋯)
            r.toListModel)
      | Ordering.gt =>
        Std.DTreeMap.Internal.Impl.explore k
          (inner init (Std.DTreeMap.Internal.Impl.ExplorationStep.gt l.toListModel ky h y)) inner r
-- Mathlib.GroupTheory.Coset.Basic
Subgroup.quotientEquivProdOfLE'.eq_1 : ∀ {α : Type u_1} [inst : Group α] {s t : Subgroup α} (h_le : s ≤ t) (f : α ⧸ t → α)
  (hf : Function.RightInverse f QuotientGroup.mk),
  Subgroup.quotientEquivProdOfLE' h_le f hf =
    { toFun := fun a => (Quotient.map' id ⋯ a, Quotient.map' (fun g => ⟨(f (Quotient.mk'' g))⁻¹ * g, ⋯⟩) ⋯ a),
      invFun := fun a => Quotient.map' (fun b => f a.1 * ↑b) ⋯ a.2, left_inv := ⋯, right_inv := ⋯ }
-- Init.Data.Int.Gcd
Int.pow_gcd_pow_of_gcd_eq_one : ∀ {n m : ℤ} {k l : ℕ}, n.gcd m = 1 → (n ^ k).gcd (m ^ l) = 1
-- Mathlib.Algebra.Homology.SpectralSequence.ComplexShape
ComplexShape.spectralSequenceNat_rel_iff : ∀ (u : ℤ × ℤ) (a b : ℕ × ℕ), (ComplexShape.spectralSequenceNat u).Rel a b ↔ ↑a.1 + u.1 = ↑b.1 ∧ ↑a.2 + u.2 = ↑b.2
-- Mathlib.Order.Interval.Set.Fin
Fin.preimage_succ_Icc_succ : ∀ {n : ℕ} (i j : Fin n), Fin.succ ⁻¹' Set.Icc i.succ j.succ = Set.Icc i j
-- Mathlib.GroupTheory.ArchimedeanDensely
LinearOrderedCommGroup.closure_equiv_closure.eq_1 : ∀ {G : Type u_1} {G' : Type u_2} [inst : CommGroup G] [inst_1 : LinearOrder G] [inst_2 : IsOrderedMonoid G]
  [inst_3 : CommGroup G'] [inst_4 : LinearOrder G'] [inst_5 : IsOrderedMonoid G'] (x : G) (y : G')
  (hxy : x = 1 ↔ y = 1),
  LinearOrderedCommGroup.closure_equiv_closure x y hxy =
    if hx : x = 1 then
      { toFun := fun x_1 => ⟨1, ⋯⟩, invFun := fun x_1 => ⟨1, ⋯⟩, left_inv := ⋯, right_inv := ⋯, map_mul' := ⋯,
        map_le_map_iff' := ⋯ }
    else
      let x' := max x x⁻¹;
      have hx' := ⋯;
      have xpos := ⋯;
      let y' := max y y⁻¹;
      have hy' := ⋯;
      have ypos := ⋯;
      have hxc := ⋯;
      have hyc := ⋯;
      have Hx := ⋯;
      have Hy := ⋯;
      { toMulEquiv := mulEquivOfOrderOfEq Hx Hy ⋯, map_le_map_iff' := ⋯ }
-- Mathlib.RingTheory.PolynomialLaw.Basic
/-- Lift an element of a tensor product  -/
PolynomialLaw.exists_lift : ∀ {R : Type u} [inst : CommSemiring R] {M : Type u_1} [inst_1 : AddCommMonoid M] [inst_2 : Module R M] {S : Type v}
  [inst_3 : CommSemiring S] [inst_4 : Algebra R S] (t : TensorProduct R S M),
  ∃ n ψ p, (LinearMap.rTensor M ψ.toLinearMap) p = t
-- Mathlib.Analysis.SpecialFunctions.Pow.Real
Complex.norm_cpow_of_ne_zero : ∀ {z : ℂ}, z ≠ 0 → ∀ (w : ℂ), ‖z ^ w‖ = ‖z‖ ^ w.re / Real.exp (z.arg * w.im)
-- Mathlib.Tactic.FieldSimp
_private.Mathlib.Tactic.FieldSimp.0.Mathlib.Tactic.FieldSimp.qNF.evalPrettyAux : {v : Lean.Level} →
  {M : Q(Type v)} →
    (iM : Q(CommGroupWithZero «$M»)) →
      (l : Mathlib.Tactic.FieldSimp.qNF M) →
        Lean.MetaM
          ((e : Q(«$M»)) ×
            have a := l.toNF;
            Q(«$a».eval = «$e»))
-- Mathlib.Analysis.SpecialFunctions.ExpDeriv
AnalyticWithinAt.cexp : ∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℂ E] {f : E → ℂ} {x : E} {s : Set E},
  AnalyticWithinAt ℂ f s x → AnalyticWithinAt ℂ (fun z => Complex.exp (f z)) s x
-- Mathlib.RingTheory.DedekindDomain.Ideal.Lemmas
IsDedekindDomain.idealFactorsEquivOfQuotEquiv_mem_normalizedFactors_of_mem_normalizedFactors : ∀ {R : Type u_1} {A : Type u_2} [inst : CommRing R] [inst_1 : CommRing A] [inst_2 : IsDedekindDomain A] {I : Ideal R}
  {J : Ideal A} [inst_3 : IsDedekindDomain R] (f : R ⧸ I ≃+* A ⧸ J),
  J ≠ ⊥ →
    ∀ {L : Ideal R} (hL : L ∈ UniqueFactorizationMonoid.normalizedFactors I),
      ↑((IsDedekindDomain.idealFactorsEquivOfQuotEquiv f) ⟨L, ⋯⟩) ∈ UniqueFactorizationMonoid.normalizedFactors J
-- Mathlib.RingTheory.Noetherian.OfPrime
/-- If all prime ideals in a commutative ring are finitely generated, so are all other ideals.  -/
IsNoetherianRing.of_prime : ∀ {R : Type u_1} [inst : CommRing R], (∀ (I : Ideal R), I.IsPrime → I.FG) → IsNoetherianRing R
-- Lean.Meta.InferType
_private.Lean.Meta.InferType.0.Lean.Meta.checkInferTypeCache : Lean.Expr → Lean.MetaM Lean.Expr → Lean.MetaM Lean.Expr
-- Batteries.Data.UnionFind.Basic
Batteries.UnionFind.parentD_findAux_or : ∀ (self : Batteries.UnionFind) (x : Fin self.size) (i : ℕ),
  Batteries.UnionFind.parentD (self.findAux x).s i = self.rootD i ∧ self.rootD i = self.rootD ↑x ∨
    Batteries.UnionFind.parentD (self.findAux x).s i = self.parent i
-- Mathlib.Analysis.Asymptotics.Lemmas
Asymptotics.IsBigO.of_pow : ∀ {α : Type u_1} {R : Type u_13} {𝕜 : Type u_15} [inst : SeminormedRing R] [inst_1 : NormedDivisionRing 𝕜]
  {l : Filter α} {f : α → 𝕜} {g : α → R} {n : ℕ}, n ≠ 0 → (f ^ n) =O[l] (g ^ n) → f =O[l] g
-- Mathlib.Analysis.Convex.DoublyStochasticMatrix
/-- The set of doubly stochastic matrices is convex.  -/
convex_doublyStochastic : ∀ {R : Type u_1} {n : Type u_2} [inst : Fintype n] [inst_1 : DecidableEq n] [inst_2 : Semiring R]
  [inst_3 : PartialOrder R] [inst_4 : IsOrderedRing R], Convex R ↑(doublyStochastic R n)
-- Init.Grind.ToInt
Lean.Grind.ToInt.LT.mk : ∀ {α : Type u} [inst : LT α] {I : outParam Lean.Grind.IntInterval} [inst_1 : Lean.Grind.ToInt α I],
  (∀ (x y : α), x < y ↔ ↑x < ↑y) → Lean.Grind.ToInt.LT α I
-- Mathlib.Geometry.Manifold.Notation
/-- Finds the first local instance of class `c` for which `p inst type` produces `some a`.
Instantiates mvars in and runs `whnfR` on `type` before passing it to `p`. (Does not validate that
`c` resolves to a class.)  -/
_private.Mathlib.Geometry.Manifold.Notation.0.Manifold.Elab.findSomeLocalInstanceOf? : Lean.Name → {α : Type} → (Lean.Expr → Lean.Expr → Lean.MetaM (Option α)) → Lean.MetaM (Option α)
-- Init.Data.UInt.Lemmas
UInt32.toUInt8_lt : ∀ {a b : UInt32}, a.toUInt8 < b.toUInt8 ↔ a % 256 < b % 256
-- Mathlib.Algebra.Module.TransferInstance
Equiv.linearEquiv_apply : ∀ {R : Type u_1} {α : Type u_2} {β : Type u_3} [inst : Semiring R] (e : α ≃ β) (a : α) [inst_1 : AddCommMonoid β]
  [inst_2 : Module R β], (Equiv.linearEquiv R e) a = e a
-- Init.Data.SInt.Float
/-- Truncates a floating-point number to the nearest 64-bit signed integer, rounding towards zero.

If the `Float` is larger than the maximum value for `Int64` (including `Inf`), returns the maximum
value of `Int64` (i.e. `Int64.maxValue`). If it is smaller than the minimum value for `Int64`
(including `-Inf`), returns the minimum value of `Int64` (i.e. `Int64.minValue`). If it is `NaN`,
returns `0`.

This function does not reduce in the kernel.
 -/
Float.toInt64 : Float → Int64
-- Plausible.Arbitrary
Plausible.Option.Arbitrary : {α : Type} → [Plausible.Arbitrary α] → Plausible.Arbitrary (Option α)
-- Mathlib.LinearAlgebra.Matrix.Echelon.Basic
Matrix.instDecidableIsLeadingEntryOfDecidableEqOfFintypeOfDecidableLT : {m : Type u_1} →
  {n : Type u_2} →
    {R : Type v} →
      [inst : Zero R] →
        [DecidableEq R] →
          [Fintype n] →
            [inst_3 : LT n] →
              [DecidableLT n] → (A : Matrix m n R) → (i : m) → (c : n) → Decidable (A.IsLeadingEntry i c)
-- Aesop.Search.ExpandSafePrefix
_private.Aesop.Search.ExpandSafePrefix.0.Aesop.expandSafePrefixGoal : {Q : Type} → [inst : Aesop.Queue Q] → Aesop.GoalRef → Aesop.SafeExpansionM Q Unit
-- Mathlib.LinearAlgebra.Matrix.InvariantBasisNumber
instInvariantBasisNumberMulOpposite : ∀ {R : Type u_1} [inst : Semiring R] [InvariantBasisNumber R], InvariantBasisNumber Rᵐᵒᵖ
-- Mathlib.Algebra.Polynomial.Module.Basic
PolynomialModule.instIsScalarTower : ∀ {R : Type u_2} [inst : CommRing R] {S : Type u_5} [inst_1 : CommSemiring S] [inst_2 : Algebra S R] (M : Type u)
  [inst_3 : AddCommGroup M] [inst_4 : Module R M] [inst_5 : Module S M] [IsScalarTower S R M],
  IsScalarTower S R (PolynomialModule R M)
-- Mathlib.Data.Set.Semiring
SetSemiring.instNonUnitalCommSemiringOfCommSemigroup : {α : Type u_1} → [CommSemigroup α] → NonUnitalCommSemiring (SetSemiring α)
-- Mathlib.MeasureTheory.Constructions.BorelSpace.Real
Measurable.coe_ereal_ennreal : ∀ {α : Type u_1} {mα : MeasurableSpace α} {f : α → ENNReal}, Measurable f → Measurable fun x => ↑(f x)
-- Mathlib.NumberTheory.LucasLehmer
LucasLehmer.ω_pow_eq_neg_one : ∀ (p' : ℕ), lucasLehmerResidue (p' + 2) = 0 → LucasLehmer.X.ω ^ 2 ^ (p' + 1) = -1
-- Std.Data.TreeSet.Raw.Lemmas
Std.TreeSet.Raw.size_inter_le_size_left : ∀ {α : Type u} {cmp : α → α → Ordering} {t₁ t₂ : Std.TreeSet.Raw α cmp} [Std.TransCmp cmp],
  t₁.WF → t₂.WF → (t₁ ∩ t₂).size ≤ t₁.size
-- Mathlib.Algebra.Group.Embedding
mulRightEmbedding.eq_1 : ∀ {G : Type u_1} [inst : Mul G] [inst_1 : IsRightCancelMul G] (g : G),
  mulRightEmbedding g = { toFun := fun h => h * g, inj' := ⋯ }
-- Mathlib.Algebra.GradedMonoid
SetLike.prod_mem_graded : ∀ {ι : Type u_2} {R : Type u_3} {S : Type u_4} [inst : SetLike S R] [inst_1 : CommMonoid R] [inst_2 : AddCommMonoid ι]
  (A : ι → S) [SetLike.GradedMonoid A] {κ : Type u_5} (i : κ → ι) (g : κ → R) {F : Finset κ},
  (∀ k ∈ F, g k ∈ A (i k)) → ∏ k ∈ F, g k ∈ A (∑ k ∈ F, i k)
-- Mathlib.Analysis.Asymptotics.Completion
Asymptotics.isTheta_completion_right : ∀ {α : Type u_1} {E : Type u_2} {F : Type u_3} [inst : Norm E] [inst_1 : SeminormedAddCommGroup F] {f : α → E}
  {g : α → F} {l : Filter α}, (f =Θ[l] fun x => ↑(g x)) ↔ f =Θ[l] g
-- Mathlib.Probability.Independence.Process.HasIndepIncrements.IsGaussianProcess
/-- `incrementsToRestrict I` is a continuous linear map `f` such that if `t₁ < ... < tₙ` are
then elements of `I`, then `f (xₜ₁, xₜ₂ - xₜ₁, ..., xₜₙ - xₜₙ₋₁) = (xₜ₁, ..., xₜₙ)`.  -/
_private.Mathlib.Probability.Independence.Process.HasIndepIncrements.IsGaussianProcess.0.ProbabilityTheory.incrementsToRestrict : {T : Type u_1} →
  {E : Type u_3} →
    [LinearOrder T] →
      (R : Type u_4) →
        [inst : Semiring R] →
          [inst_1 : AddCommMonoid E] →
            [inst_2 : Module R E] →
              [inst_3 : TopologicalSpace E] → [ContinuousAdd E] → (I : Finset T) → (Fin I.card → E) →L[R] ↥I → E
-- Init.Prelude
/-- The implementation of `a <|> b : α`. See `HOrElse`.  -/
OrElse.orElse : {α : Type u} → [self : OrElse α] → α → (Unit → α) → α
-- Mathlib.Topology.Semicontinuity.Basic
Continuous.comp_lowerSemicontinuousOn : ∀ {α : Type u_1} [inst : TopologicalSpace α] {s : Set α} {γ : Type u_4} [inst_1 : LinearOrder γ]
  [inst_2 : TopologicalSpace γ] [OrderTopology γ] {δ : Type u_5} [inst_4 : LinearOrder δ] [inst_5 : TopologicalSpace δ]
  [OrderTopology δ] {g : γ → δ} {f : α → γ},
  Continuous g → LowerSemicontinuousOn f s → Monotone g → LowerSemicontinuousOn (g ∘ f) s
-- Mathlib.Analysis.Calculus.ContDiff.WithLp
WithLp.contDiff_ofLp : ∀ {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [inst : NontriviallyNormedField 𝕜] [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedAddCommGroup F] [inst_3 : NormedSpace 𝕜 E] [inst_4 : NormedSpace 𝕜 F] {p : ENNReal}
  [inst_5 : Fact (1 ≤ p)] {n : WithTop ℕ∞}, ContDiff 𝕜 n WithLp.ofLp
-- Mathlib.CategoryTheory.Monoidal.Cartesian.ShrinkYoneda
GrpCat.shrinkFunctor.congr_simp : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] (F F_1 : CategoryTheory.Functor C GrpCat) (e_F : F = F_1)
  [inst_1 : ∀ (X : C), Small.{w, w'} ↑(F.obj X)],
  GrpCat.shrinkFunctor.{w, w', v, u} F = GrpCat.shrinkFunctor.{w, w', v, u} F_1
-- Mathlib.CategoryTheory.Functor.KanExtension.Basic
/-- The functor `RightExtension L' F ⥤ RightExtension L F`
induced by a natural transformation `L ⋙ G ⟶ L'`.  -/
CategoryTheory.Functor.RightExtension.postcomp₁ : {C : Type u_1} →
  {H : Type u_3} →
    {D : Type u_4} →
      {D' : Type u_5} →
        [inst : CategoryTheory.Category.{v_1, u_1} C] →
          [inst_1 : CategoryTheory.Category.{v_3, u_3} H] →
            [inst_2 : CategoryTheory.Category.{v_4, u_4} D] →
              [inst_3 : CategoryTheory.Category.{v_5, u_5} D'] →
                {L : CategoryTheory.Functor C D} →
                  {L' : CategoryTheory.Functor C D'} →
                    (G : CategoryTheory.Functor D D') →
                      (L.comp G ⟶ L') →
                        (F : CategoryTheory.Functor C H) →
                          CategoryTheory.Functor (L'.RightExtension F) (L.RightExtension F)
-- Mathlib.AlgebraicGeometry.ProjectiveSpectrum.Basic
AlgebraicGeometry.Proj.openCoverOfMapIrrelevantEqTop.eq_1 : ∀ {σ : Type u_1} {A : Type u} [inst : CommRing A] [inst_1 : SetLike σ A] [inst_2 : AddSubgroupClass σ A] (𝒜 : ℕ → σ)
  [inst_3 : GradedRing 𝒜] {X : AlgebraicGeometry.Scheme} (f : A →+* ↑(X.presheaf.obj (Opposite.op ⊤)))
  (hf : Ideal.map f (HomogeneousIdeal.irrelevant 𝒜).toIdeal = ⊤),
  AlgebraicGeometry.Proj.openCoverOfMapIrrelevantEqTop 𝒜 f hf =
    X.openCoverOfIsOpenCover (fun ir => X.basicOpen (f ir.snd.fst)) ⋯
-- Init.Data.String.Lemmas.Iterate
String.Model.revPositionsFrom_startPos : ∀ {s : String}, String.Model.revPositionsFrom s.startPos = []
-- Mathlib.Analysis.SpecialFunctions.Elliptic.Weierstrass
PeriodPair.ω₁_div_two_notMem_lattice : ∀ (L : PeriodPair), L.ω₁ / 2 ∉ L.lattice
-- Mathlib.MeasureTheory.Function.L1Space.HasFiniteIntegral
MeasureTheory.hasFiniteIntegral_const_enorm : ∀ {α : Type u_1} {ε : Type u_4} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} [inst : ENorm ε]
  [MeasureTheory.IsFiniteMeasure μ] {c : ε}, ‖c‖ₑ ≠ ⊤ → MeasureTheory.HasFiniteIntegral (fun x => c) μ
-- Mathlib.Algebra.Order.Hom.Monoid
OrderMonoidIso.trans_assoc : ∀ {α : Type u_2} {β : Type u_3} {γ : Type u_4} {δ : Type u_5} [inst : Preorder α] [inst_1 : Preorder β]
  [inst_2 : Preorder γ] [inst_3 : Preorder δ] [inst_4 : Mul α] [inst_5 : Mul β] [inst_6 : Mul γ] [inst_7 : Mul δ]
  (f : α ≃*o β) (g : β ≃*o γ) (h : γ ≃*o δ), (f.trans g).trans h = f.trans (g.trans h)
-- Mathlib.AlgebraicTopology.SimplicialSet.AnodyneExtensions.RelativeCellComplex
SSet.Subcomplex.Pairing.RankFunction.isPullback : ∀ {X : SSet} {A : X.Subcomplex} {P : A.Pairing} {ι : Type v} [inst : LinearOrder ι] (f : P.RankFunction ι)
  [inst_1 : P.IsProper] [inst_2 : SuccOrder ι] [inst_3 : NoMaxOrder ι] (j : ι),
  CategoryTheory.IsPullback (f.t j) (f.m j) (SSet.Subcomplex.homOfLE ⋯) (f.b j)
-- Mathlib.Topology.Sheaves.Stalks
/-- The morphism `(f⁻¹ℱ)(U) ⟶ ℱ_{f(x)}` for some `U ∋ x`.  -/
TopCat.Presheaf.germToPullbackStalk : (C : Type u) →
  [inst : CategoryTheory.Category.{v, u} C] →
    [inst_1 : CategoryTheory.Limits.HasColimits C] →
      {X Y : TopCat} →
        (f : X ⟶ Y) →
          (F : TopCat.Presheaf C Y) →
            (U : TopologicalSpace.Opens ↑X) →
              (x : ↑X) →
                x ∈ U →
                  (((TopCat.Presheaf.pullback C f).obj F).obj (Opposite.op U) ⟶
                    F.stalk ((CategoryTheory.ConcreteCategory.hom f) x))
-- Mathlib.Geometry.Manifold.IsManifold.ExtChartAt
ModelWithCorners.extendCoordChange_source_mem_nhdsWithin' : ∀ {𝕜 : Type u_1} {E : Type u_2} {M : Type u_3} {H : Type u_4} [inst : NontriviallyNormedField 𝕜]
  [inst_1 : NormedAddCommGroup E] [inst_2 : NormedSpace 𝕜 E] [inst_3 : TopologicalSpace H] [inst_4 : TopologicalSpace M]
  {I : ModelWithCorners 𝕜 E H} {e e' : OpenPartialHomeomorph M H} {x : M},
  x ∈ e.source →
    x ∈ e'.source → (ModelWithCorners.extendCoordChange e e').source ∈ nhdsWithin (↑(e.extend I) x) (Set.range ↑I)
-- Mathlib.CategoryTheory.Limits.Shapes.Opposites.Pullbacks
_private.Mathlib.CategoryTheory.Limits.Shapes.Opposites.Pullbacks.0.CategoryTheory.Limits.spanOp.match_1.eq_2 : ∀ (motive : CategoryTheory.Limits.WalkingSpan → Sort u_1) (h_1 : Unit → motive none)
  (h_2 : Unit → motive (some CategoryTheory.Limits.WalkingPair.left))
  (h_3 : Unit → motive (some CategoryTheory.Limits.WalkingPair.right)),
  (match some CategoryTheory.Limits.WalkingPair.left with
    | none => h_1 ()
    | some CategoryTheory.Limits.WalkingPair.left => h_2 ()
    | some CategoryTheory.Limits.WalkingPair.right => h_3 ()) =
    h_2 ()
-- Mathlib.CategoryTheory.Monoidal.Functor
CategoryTheory.Functor.CoreMonoidal.toMonoidal_toOplaxMonoidal : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.MonoidalCategory C] {D : Type u₂}
  [inst_2 : CategoryTheory.Category.{v₂, u₂} D] [inst_3 : CategoryTheory.MonoidalCategory D]
  {F : CategoryTheory.Functor C D} (h : F.CoreMonoidal), h.toMonoidal.toOplaxMonoidal = h.toOplaxMonoidal
-- Mathlib.RingTheory.HahnSeries.Addition
HahnSeries.addOppositeEquiv.eq_1 : ∀ {Γ : Type u_1} {R : Type u_3} [inst : PartialOrder Γ] [inst_1 : AddMonoid R],
  HahnSeries.addOppositeEquiv =
    { toFun := fun x => AddOpposite.op { coeff := fun a => AddOpposite.unop (x.coeff a), isPWO_support' := ⋯ },
      invFun := fun x => { coeff := fun a => AddOpposite.op ((AddOpposite.unop x).coeff a), isPWO_support' := ⋯ },
      left_inv := ⋯, right_inv := ⋯, map_add' := ⋯ }
-- Aesop.Stats.Extension
Aesop.StatsExtensionEntry : Type
-- Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic
Complex.sin_add_two_pi : ∀ (x : ℂ), Complex.sin (x + 2 * ↑Real.pi) = Complex.sin x
-- Mathlib.Data.Fin.SuccPred
Fin.predAbove_pred_of_lt : ∀ {n : ℕ} (p i : Fin (n + 1)) (h : i < p), (p.pred ⋯).predAbove i = i.castPred ⋯
-- Mathlib.Algebra.BigOperators.Sym
Finset.sum_count_of_mem_sym : ∀ {α : Type u_1} [inst : DecidableEq α] {m : ℕ} {k : Sym α m} {s : Finset α},
  k ∈ s.sym m → ∑ i ∈ s, Multiset.count i ↑k = m
-- Mathlib.MeasureTheory.Integral.Lebesgue.Countable
/-- **Alias** of `MeasureTheory.lintegral_le_of_forall_fin_meas_trim_le`.

---

If the Lebesgue integral of a function is bounded by some constant on all sets with finite
measure in a sub-σ-algebra and the measure is σ-finite on that sub-σ-algebra, then the integral
over the whole space is bounded by that same constant.  -/
MeasureTheory.lintegral_le_of_forall_fin_meas_le_of_measurable : ∀ {α : Type u_1} {m m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} (hm : m ≤ m0)
  [MeasureTheory.SigmaFinite (μ.trim hm)] (C : ENNReal) {f : α → ENNReal},
  (∀ (s : Set α), MeasurableSet s → μ s ≠ ⊤ → ∫⁻ (x : α) in s, f x ∂μ ≤ C) → ∫⁻ (x : α), f x ∂μ ≤ C
-- Mathlib.CategoryTheory.Limits.Shapes.WidePullbacks
CategoryTheory.Limits.WidePullback.lift_base : ∀ {J : Type w} {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {B : C} {objs : J → C}
  (arrows : (j : J) → objs j ⟶ B) [inst_1 : CategoryTheory.Limits.HasWidePullback B objs arrows] {X : C} (f : X ⟶ B)
  (fs : (j : J) → X ⟶ objs j) (w : ∀ (j : J), CategoryTheory.CategoryStruct.comp (fs j) (arrows j) = f),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.WidePullback.lift f fs w)
      (CategoryTheory.Limits.WidePullback.base arrows) =
    f
-- Mathlib.CategoryTheory.Bicategory.Adjunction.Adj
CategoryTheory.Bicategory.Adj.hom₂_ext : ∀ {B : Type u} [inst : CategoryTheory.Bicategory B] {a b : CategoryTheory.Bicategory.Adj B} {α β : a ⟶ b} {x y : α ⟶ β},
  x.τl = y.τl → x = y
-- Std.Data.ExtTreeMap.Lemmas
Std.ExtTreeMap.getD_union_of_not_mem_left : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t₁ t₂ : Std.ExtTreeMap α β cmp} [inst : Std.TransCmp cmp] {k : α}
  {fallback : β}, k ∉ t₁ → (t₁ ∪ t₂).getD k fallback = t₂.getD k fallback
-- Mathlib.CategoryTheory.Limits.Preserves.Basic
CategoryTheory.Limits.PreservesLimitsOfSize.mk : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  {F : CategoryTheory.Functor C D},
  autoParam
      (∀ {J : Type w} [inst_2 : CategoryTheory.Category.{w', w} J], CategoryTheory.Limits.PreservesLimitsOfShape J F)
      CategoryTheory.Limits.PreservesLimitsOfSize.preservesLimitsOfShape._autoParam →
    CategoryTheory.Limits.PreservesLimitsOfSize.{w', w, v₁, v₂, u₁, u₂} F
-- Mathlib.CategoryTheory.Generator.Basic
CategoryTheory.isCodetector_coseparator : ∀ (C : Type u₁) [inst : CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.Balanced C]
  [inst_2 : CategoryTheory.HasCoseparator C], CategoryTheory.IsCodetector (CategoryTheory.coseparator C)
-- Mathlib.Analysis.RCLike.Basic
RCLike.zero_re : ∀ {K : Type u_1} [inst : RCLike K], RCLike.re 0 = 0
-- Mathlib.Data.ZMod.Basic
ZMod.val_lt : ∀ {n : ℕ} [NeZero n] (a : ZMod n), a.val < n
-- Mathlib.Topology.Homeomorph.Defs
Homeomorph.refl_apply : ∀ (X : Type u_7) [inst : TopologicalSpace X], ⇑(Homeomorph.refl X) = id
-- Init.Data.Iterators.Lemmas.Consumers.Monadic.Loop
_private.Init.Data.Iterators.Lemmas.Consumers.Monadic.Loop.0.Std.IterM.findSomeM?_eq_match_step.match_1.eq_2 : ∀ {γ : Type u_1} (motive : Option γ → Sort u_2) (fx : γ) (h_1 : Unit → motive none) (h_2 : (fx : γ) → motive (some fx)),
  (match some fx with
    | none => h_1 ()
    | some fx => h_2 fx) =
    h_2 fx
-- Mathlib.RepresentationTheory.Homological.GroupHomology.Functoriality
groupHomology.cyclesMap_comp_isoCycles₂_hom : ∀ {k G H : Type u} [inst : CommRing k] [inst_1 : Group G] [inst_2 : Group H] {A : Rep.{u, u, u} k G}
  {B : Rep.{u, u, u} k H} (f : G →* H) (φ : A ⟶ Rep.res f B),
  CategoryTheory.CategoryStruct.comp (groupHomology.cyclesMap f φ 2) (groupHomology.isoCycles₂ B).hom =
    CategoryTheory.CategoryStruct.comp (groupHomology.isoCycles₂ A).hom (groupHomology.mapCycles₂ f φ)
-- Mathlib.Algebra.Group.Subgroup.Map
AddEquiv.addSubgroupMap.eq_1 : ∀ {G : Type u_1} {G' : Type u_2} [inst : AddGroup G] [inst_1 : AddGroup G'] (e : G ≃+ G') (H : AddSubgroup G),
  e.addSubgroupMap H = e.addSubmonoidMap H.toAddSubmonoid
-- Init.Notation
/-- All the elements of a type that satisfy a predicate.

`Subtype p`, usually written `{ x : α // p x }` or `{ x // p x }`, contains all elements `x : α` for
which `p x` is true. Its constructor is a pair of the value and the proof that it satisfies the
predicate. In run-time code, `{ x : α // p x }` is represented identically to `α`.

There is a coercion from `{ x : α // p x }` to `α`, so elements of a subtype may be used where the
underlying type is expected.

Examples:
 * `{ n : Nat // n % 2 = 0 }` is the type of even numbers.
 * `{ xs : Array String // xs.size = 5 }` is the type of arrays with five `String`s.
 * Given `xs : List α`, `List { x : α // x ∈ xs }` is the type of lists in which all elements are
   contained in `xs`.


Conventions for notations in identifiers:

 * The recommended spelling of `{ x // p x }` in identifiers is `subtype`. -/
«term{_:_//_}» : Lean.ParserDescr
-- Mathlib.Analysis.Calculus.AbsolutelyMonotone
/-- A globally `C^∞` function whose iterated derivatives are nonnegative on `s` is absolutely
monotone on `s`. The set `s` need *not* satisfy `UniqueDiffOn`.  -/
AbsolutelyMonotoneOn.of_contDiff : ∀ {f : ℝ → ℝ} {s : Set ℝ}, ContDiff ℝ (↑⊤) f → (∀ (n : ℕ), ∀ x ∈ s, 0 ≤ iteratedDeriv n f x) → AbsolutelyMonotoneOn f s
-- Aesop.Frontend.RuleExpr
Aesop.Frontend.RuleExpr.node.sizeOf_spec : ∀ (f : Aesop.Frontend.Feature) (children : Array Aesop.Frontend.RuleExpr),
  sizeOf (Aesop.Frontend.RuleExpr.node f children) = 1 + sizeOf f + sizeOf children