mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.CategoryTheory.EqToHom
CategoryTheory.Functor.congr_inv_of_congr_hom : ∀ {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) {X Y : C} (e : X ≅ Y) (hX : F.obj X = G.obj X) (hY : F.obj Y = G.obj Y),
  F.map e.hom =
      CategoryTheory.CategoryStruct.comp (CategoryTheory.eqToHom ⋯)
        (CategoryTheory.CategoryStruct.comp (G.map e.hom) (CategoryTheory.eqToHom ⋯)) →
    F.map e.inv =
      CategoryTheory.CategoryStruct.comp (CategoryTheory.eqToHom ⋯)
        (CategoryTheory.CategoryStruct.comp (G.map e.inv) (CategoryTheory.eqToHom ⋯))
-- Mathlib.Algebra.Order.Floor.Semiring
Nat.floor_ofNat : ∀ {R : Type u_1} [inst : Semiring R] [inst_1 : LinearOrder R] [inst_2 : FloorSemiring R] [IsStrictOrderedRing R] (n : ℕ)
  [inst_4 : n.AtLeastTwo], ⌊OfNat.ofNat n⌋₊ = OfNat.ofNat n
-- Mathlib.CategoryTheory.Preadditive.EilenbergMoore
CategoryTheory.Comonad.coalgebraPreadditive_homGroup_zsmul_f : ∀ (C : Type u₁) [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.Preadditive C]
  (U : CategoryTheory.Comonad C) [inst_2 : U.Additive] (F G : U.Coalgebra) (r : ℤ) (α : F ⟶ G), (r • α).f = r • α.f
-- Mathlib.Combinatorics.Additive.Convolution
Finset.card_div_eq : ∀ {G : Type u_1} [inst : Group G] [inst_1 : DecidableEq G] (A B : Finset G) (x : G),
  {ab ∈ A ×ˢ B | ab.1 / ab.2 = x}.card = A.convolution B⁻¹ x
-- Mathlib.GroupTheory.FreeGroup.IsFreeGroup
/-- Given an additive free group basis of `G` over `ι`, there is a canonical bijection between
maps from `ι` to an additive group `H` and morphisms from `G` to `H`.  -/
FreeAddGroupBasis.lift : {ι : Type u_1} →
  {G : Type u_3} →
    {H : Type u_4} → [inst : AddGroup G] → [inst_1 : AddGroup H] → FreeAddGroupBasis ι G → (ι → H) ≃ (G →+ H)
-- Mathlib.RingTheory.HopfAlgebra.Basic
/-- The antipode of the Hopf algebra.  -/
HopfAlgebraStruct.antipode : (R : Type u) →
  {A : Type v} → {inst : CommSemiring R} → {inst_1 : Semiring A} → [self : HopfAlgebraStruct R A] → A →ₗ[R] A
-- Mathlib.Order.WithBot
WithBot.unbot_eq_iff : ∀ {α : Type u_1} {a : WithBot α} {b : α} (h : a ≠ ⊥), a.unbot h = b ↔ a = ↑b
-- Mathlib.Data.Option.Basic
Option.pmap_bind_id_eq_pmap_join : ∀ {α : Type u_1} {β : Type u_2} {p : α → Prop} {f : (a : α) → p a → β} {x : Option (Option α)}
  (H : ∀ (a : Option α), x = some a → ∀ (a_2 : α), a = some a_2 → p a_2),
  ((Option.pmap (Option.pmap f) x H).bind fun a => a) = Option.pmap f x.join ⋯
-- Mathlib.Analysis.SpecialFunctions.Log.Basic
Real.range_log : Set.range Real.log = Set.univ
-- Init.Omega.Coeffs
/-- Shim for `.enum.find?`.  -/
Lean.Omega.Coeffs.findIdx? : (ℤ → Bool) → Lean.Omega.Coeffs → Option ℕ
-- Init.Data.Option.Lemmas
Option.min_eq_some_iff : ∀ {α : Type u_1} [inst : Min α] {o o' : Option α} {a : α}, o ⊓ o' = some a ↔ ∃ b c, o = some b ∧ o' = some c ∧ b ⊓ c = a
-- Mathlib.CategoryTheory.Abelian.Basic
CategoryTheory.Abelian.hasFiniteLimits : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [CategoryTheory.Abelian C],
  CategoryTheory.Limits.HasFiniteLimits C
-- Lean.Data.Lsp.LanguageFeatures
Lean.Lsp.SymbolKind.variable.sizeOf_spec : sizeOf Lean.Lsp.SymbolKind.variable = 1
-- Init.Data.SInt.Lemmas
Int8.add_neg_eq_sub : ∀ {a b : Int8}, a + -b = a - b
-- Mathlib.GroupTheory.GroupAction.Hom
AddActionHom.fst_apply : ∀ (M : Type u_1) (α : Type u_2) (β : Type u_3) [inst : VAdd M α] [inst_1 : VAdd M β],
  ⇑(AddActionHom.fst M α β) = Prod.fst
-- Mathlib.Data.ENNReal.Inv
ENNReal.zpow_le_of_le : ∀ {x : ENNReal}, 1 ≤ x → ∀ {a b : ℤ}, a ≤ b → x ^ a ≤ x ^ b
-- Lean.Data.PersistentArray
Lean.PersistentArray.getAux : {α : Type u} → [Inhabited α] → Lean.PersistentArrayNode α → USize → USize → α
-- Mathlib.AlgebraicGeometry.Morphisms.Immersion
/-- The map `X ×[S] Y ⟶ X ×[T] Y` induced by any `S ⟶ T` is always an immersion.  -/
AlgebraicGeometry.IsImmersion.instMapDescScheme : ∀ {X Y S T : AlgebraicGeometry.Scheme} (f : X ⟶ S) (g : Y ⟶ S) (i : S ⟶ T),
  AlgebraicGeometry.IsImmersion (CategoryTheory.Limits.pullback.mapDesc f g i)
-- Mathlib.Order.Lattice
inf_le_inf_right : ∀ {α : Type u} [inst : SemilatticeInf α] {a b : α} (c : α), b ≤ a → b ⊓ c ≤ a ⊓ c
-- Mathlib.RingTheory.LocalProperties.Submodule
Submodule.mem_of_isLocalized_span : ∀ {R : Type u_1} {M : Type u_2} [inst : CommSemiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M] (s : Set R),
  Ideal.span s = ⊤ →
    ∀ (Mₚ : ↑s → Type u_5) [inst_3 : (r : ↑s) → AddCommMonoid (Mₚ r)] [inst_4 : (r : ↑s) → Module R (Mₚ r)]
      (f : (r : ↑s) → M →ₗ[R] Mₚ r) [inst_5 : ∀ (r : ↑s), IsLocalizedModule.Away (↑r) (f r)] {m : M}
      {N : Submodule R M}, (∀ (r : ↑s), (f r) m ∈ Submodule.localized₀ (Submonoid.powers ↑r) (f r) N) → m ∈ N
-- Mathlib.Algebra.Group.End
MulAut.congr_symm_apply : ∀ {G : Type u_3} [inst : Group G] {H : Type u_7} [inst_1 : Group H] (ϕ : G ≃* H) (f : MulAut H),
  (MulAut.congr ϕ).symm f = ϕ.trans (MulEquiv.trans f ϕ.symm)
-- Lean.Parser.Do
Lean.Parser.Term.doCatchMatch.parenthesizer : Lean.PrettyPrinter.Parenthesizer
-- Mathlib.MeasureTheory.Measure.Lebesgue.Basic
/-- A diagonal matrix rescales Lebesgue according to its determinant. This is a special case of
`Real.map_matrix_volume_pi_eq_smul_volume_pi`, that one should use instead (and whose proof
uses this particular case).  -/
Real.smul_map_diagonal_volume_pi : ∀ {ι : Type u_1} [inst : Fintype ι] [inst_1 : DecidableEq ι] {D : ι → ℝ},
  (Matrix.diagonal D).det ≠ 0 →
    ENNReal.ofReal |(Matrix.diagonal D).det| •
        MeasureTheory.Measure.map (⇑(Matrix.toLin' (Matrix.diagonal D))) MeasureTheory.volume =
      MeasureTheory.volume
-- Mathlib.Algebra.Algebra.Basic
FaithfulSMul.algebraMap_eq_one_iff : ∀ (R : Type u_1) (A : Type u_2) [inst : CommSemiring R] [inst_1 : Semiring A] [inst_2 : Algebra R A] [FaithfulSMul R A]
  {r : R}, (algebraMap R A) r = 1 ↔ r = 1
-- Mathlib.MeasureTheory.Group.Action
MeasureTheory.measure_inv_smul_sdiff : ∀ {G : Type u} {α : Type w} {m : MeasurableSpace α} [inst : Group G] [inst_1 : MulAction G α]
  (μ : MeasureTheory.Measure α) [MeasureTheory.SMulInvariantMeasure G α μ] (c : G) (s t : Set α),
  μ (c⁻¹ • s \ t) = μ (s \ c • t)
-- Aesop.Search.SearchM
Aesop.SearchM.State.maxRuleApplicationDepthReached : {Q : Type} → [inst : Aesop.Queue Q] → Aesop.SearchM.State Q → Bool
-- Mathlib.CategoryTheory.Bicategory.Span.Basic
CategoryTheory.Span.hom_ext_iff : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] {Wₗ Wᵣ : CategoryTheory.MorphismProperty C} {c c' : C}
  {S S' : CategoryTheory.Span Wₗ Wᵣ c c'} {f g : S ⟶ S'}, f = g ↔ f.hom = g.hom
-- Std.Time.DateTime.PlainDateTime
Std.Time.PlainDateTime.ext : ∀ {x y : Std.Time.PlainDateTime}, x.date = y.date → x.time = y.time → x = y
-- Mathlib.Data.List.Lattice
List.mem_union_left : ∀ {α : Type u_1} {l₁ : List α} {a : α} [inst : DecidableEq α], a ∈ l₁ → ∀ (l₂ : List α), a ∈ l₁ ∪ l₂
-- Mathlib.GroupTheory.Focal
/-- Lemma: The focal subgroup is indeed a subgroup of H.  -/
Subgroup.focalSubgroup_le : ∀ {G : Type u_1} [inst : Group G] (H : Subgroup G), H.focalSubgroup ≤ H
-- Init.Meta.Defs
_private.Init.Meta.Defs.0.Lean.Syntax.decodeScientificLitVal?.decodeAfterExp : String → String.Pos.Raw → ℕ → ℕ → Bool → ℕ → Option (ℕ × Bool × ℕ)
-- Mathlib.RingTheory.Localization.AtPrime.Basic
Localization.le_comap_primeCompl_iff : ∀ {R : Type u_1} [inst : CommSemiring R] {P : Type u_3} [inst_1 : CommSemiring P] {I : Ideal R} [hI : I.IsPrime]
  {J : Ideal P} [inst_2 : J.IsPrime] {f : R →+* P}, I.primeCompl ≤ Submonoid.comap f J.primeCompl ↔ Ideal.comap f J ≤ I
-- Mathlib.Analysis.Complex.UnitDisc.Basic
Complex.UnitDisc.instSMulCommClass_circle_right : SMulCommClass Complex.UnitDisc Circle Complex.UnitDisc
-- Lean.Meta.Match.MatcherInfo
Lean.Meta.Match.MatcherInfo.getAltRange : Lean.Meta.MatcherInfo → Std.Rco ℕ
-- Mathlib.MeasureTheory.Integral.CurveIntegral.Basic
curveIntegralFun_cast : ∀ {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [inst : RCLike 𝕜] [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F] {a b c d : E}
  (ω : E → E →L[𝕜] F) (γ : Path a b) (hc : c = a) (hd : d = b), curveIntegralFun ω (γ.cast hc hd) = curveIntegralFun ω γ
-- Std.Data.ExtTreeMap.Basic
/-- Returns the `n`-th smallest key, or `fallback` if `n` is at least `t.size`.  -/
Std.ExtTreeMap.keyAtIdxD : {α : Type u} → {β : Type v} → {cmp : α → α → Ordering} → [Std.TransCmp cmp] → Std.ExtTreeMap α β cmp → ℕ → α → α
-- Init.Data.Format.Basic
/-- Emits the string `s`.
 -/
Std.Format.MonadPrettyFormat.pushOutput : {m : Type → Type} → [self : Std.Format.MonadPrettyFormat m] → String → m Unit
-- Mathlib.Data.Multiset.ZeroCons
Multiset.singleton_eq_cons_iff : ∀ {α : Type u_1} {a b : α} (m : Multiset α), {a} = b ::ₘ m ↔ a = b ∧ m = 0
-- Batteries.Data.List.Basic
/-- Tail-recursive version of `tails`.  -/
List.tailsTR : {α : Type u_1} → List α → List (List α)
-- Mathlib.Algebra.Category.FGModuleCat.Basic
/-- Universe lifting as a functor on `FGModuleCat`.  -/
FGModuleCat.ulift : (R : Type u) → [inst : Ring R] → CategoryTheory.Functor (FGModuleCat R) (FGModuleCat R)
-- Mathlib.SetTheory.Cardinal.ToNat
Cardinal.cast_toNat_eq_iff_lt_aleph0 : ∀ {c : Cardinal.{u_1}}, ↑(Cardinal.toNat c) = c ↔ c < Cardinal.aleph0
-- Mathlib.FieldTheory.Galois.NormalBasis
AdjoinRoot.powerBasis.eq_1 : ∀ {K : Type u_5} [inst : Field K] {f : Polynomial K} (hf : f ≠ 0),
  AdjoinRoot.powerBasis hf =
    { gen := AdjoinRoot.root f, dim := f.natDegree, basis := AdjoinRoot.powerBasisAux hf, basis_eq_pow := ⋯ }
-- Mathlib.Data.Sign.Basic
/-- Casting `SignType → ℤ → α` is the same as casting directly `SignType → α`.  -/
SignType.intCast_cast : ∀ {α : Type u_1} [inst : AddGroupWithOne α] (s : SignType), ↑↑s = ↑s
-- Mathlib.CategoryTheory.Monoidal.Mon
CategoryTheory.AddMon.EquivLaxMonoidalFunctorPUnit.addMonToLaxMonoidalObj_ε : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.MonoidalCategory C]
  (A : CategoryTheory.AddMon C),
  CategoryTheory.Functor.LaxMonoidal.ε (CategoryTheory.AddMon.EquivLaxMonoidalFunctorPUnit.addMonToLaxMonoidalObj A) =
    CategoryTheory.AddMonObj.zero
-- Mathlib.Algebra.MonoidAlgebra.Degree
AddMonoidAlgebra.le_inf_support_coeff_add : ∀ {R : Type u_1} {A : Type u_3} {T : Type u_4} [inst : SemilatticeInf T] [inst_1 : OrderTop T] [inst_2 : Semiring R]
  (degt : A → T) (f g : AddMonoidAlgebra R A),
  f.coeff.support.inf degt ⊓ g.coeff.support.inf degt ≤ (f + g).coeff.support.inf degt
-- Lean.Meta.TryThis
/-- Optional info to be printed immediately before replacement text in a widget.  -/
Lean.Meta.Tactic.TryThis.Suggestion.preInfo? : Lean.Meta.Tactic.TryThis.Suggestion → Option String
-- Mathlib.Combinatorics.Matroid.Closure
Matroid.closure_inter_ground : ∀ {α : Type u_2} (M : Matroid α) (X : Set α), M.closure (X ∩ M.E) = M.closure X
-- Mathlib.Analysis.Complex.CanonicalDecomposition
/-- **Extended canonical decomposition:** A meromorphic function on a closed disk is equal, up to
modification over a discrete set, to a product of a non-vanishing analytic function, canonical
factors and meromorphic functions of the form `(x - const) ^ n` where `const` is on the
circumference of the disk.
 -/
MeromorphicOn.exists_ecanonicalDecomp : ∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℂ E] {R : ℝ} {f : ℂ → E},
  MeromorphicOn f (Metric.closedBall 0 R) →
    (∀ (u : ↑(Metric.closedBall 0 R)), meromorphicOrderAt f ↑u ≠ ⊤) → ∃ h, Complex.ECanonicalDecomp f h R
-- Mathlib.Topology.Bornology.Constructions
Bornology.IsBounded.image_eval : ∀ {ι : Type u_3} {X : ι → Type u_4} [inst : (i : ι) → Bornology (X i)] {s : Set ((i : ι) → X i)},
  Bornology.IsBounded s → ∀ (i : ι), Bornology.IsBounded (Function.eval i '' s)
-- Mathlib.Geometry.Manifold.BumpFunction
SmoothBumpFunction.instNonempty : ∀ {E : Type uE} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] {H : Type uH} [inst_2 : TopologicalSpace H]
  {I : ModelWithCorners ℝ E H} {M : Type uM} [inst_3 : TopologicalSpace M] [inst_4 : ChartedSpace H M] {c : M},
  Nonempty (SmoothBumpFunction I c)
-- Mathlib.Control.Traversable.Instances
List.traverse_cons : ∀ {F : Type u → Type u} [inst : Applicative F] {α' β' : Type u} (f : α' → F β') (a : α') (l : List α'),
  traverse f (a :: l) = (fun x1 x2 => x1 :: x2) <$> f a <*> traverse f l
-- Mathlib.RingTheory.Congruence.Hom
/-- Surjective ring homomorphisms constant on the equivalence classes
of a ring congruence relation induce a surjective homomorphism on the quotient.  -/
RingCon.lift_surjective_of_surjective : ∀ {M : Type u_1} {P : Type u_3} [inst : NonAssocSemiring M] [inst_1 : NonAssocSemiring P] {c : RingCon M} {f : M →+* P}
  (h : c ≤ RingCon.ker f), Function.Surjective ⇑f → Function.Surjective ⇑(c.lift f h)
-- Mathlib.RingTheory.Valuation.Discrete.Basic
/-- The generator of a surjective discrete valuation in `ℤᵐ⁰` is equal to `exp (-1)`.  -/
Valuation.IsRankOneDiscrete.generator_eq_exp_neg_one_of_surjective : ∀ {A : Type u_2} [inst : Ring A] {v : Valuation A (WithZero (Multiplicative ℤ))} [hv : v.IsRankOneDiscrete],
  Function.Surjective ⇑v →
    Valuation.IsRankOneDiscrete.generator v =
      Units.mk0 (WithZero.exp (-1)) Valuation.IsRankOneDiscrete.generator_eq_exp_neg_one_of_mem_range._proof_1
-- Mathlib.Data.List.Chain
List.IsChain.iff_of_mem_tail_imp : ∀ {α : Type u_1} {R S : α → α → Prop} {l : List α},
  (∀ (a b : α), a ∈ l → b ∈ l.tail → (R a b ↔ S a b)) → (List.IsChain R l ↔ List.IsChain S l)
-- Mathlib.Tactic.ClickSuggestions.Util
/-- The main goal.  -/
Mathlib.Tactic.ClickSuggestions.Context.goal : Mathlib.Tactic.ClickSuggestions.Context → Lean.MVarId
-- Mathlib.Analysis.Normed.Operator.LinearIsometry
/-- An antilinear isometric equivalence between two normed vector spaces.  -/
«term_≃ₗᵢ⋆[_]_» : Lean.TrailingParserDescr
-- Mathlib.Topology.MetricSpace.HausdorffDistance
/-- The Hausdorff distances from `s` to `t` and from `t` to `s` coincide.  -/
Metric.hausdorffDist_comm : ∀ {α : Type u} [inst : PseudoMetricSpace α] {s t : Set α}, Metric.hausdorffDist s t = Metric.hausdorffDist t s
-- Mathlib.Algebra.Module.Submodule.Pointwise
Submodule.mem_neg : ∀ {R : Type u_2} {M : Type u_3} [inst : Semiring R] [inst_1 : AddCommGroup M] [inst_2 : Module R M] {g : M}
  {S : Submodule R M}, g ∈ -S ↔ -g ∈ S
-- Mathlib.AlgebraicGeometry.Stalk
AlgebraicGeometry.IsAffineOpen.fromSpecStalk.eq_1 : ∀ {X : AlgebraicGeometry.Scheme} {U : X.Opens} (hU : AlgebraicGeometry.IsAffineOpen U) {x : ↥X} (hxU : x ∈ U),
  hU.fromSpecStalk hxU =
    CategoryTheory.CategoryStruct.comp (AlgebraicGeometry.Spec.map (X.presheaf.germ U x hxU)) hU.fromSpec
-- Lean.Meta.Tactic.Apply
/-- Try to convert an `Eq` into an `Iff` by applying `propext`.
If successful, then returns then new goal, otherwise returns the original `MVarId`.
 -/
Lean.MVarId.propext : Lean.MVarId → Lean.MetaM Lean.MVarId
-- Mathlib.AlgebraicGeometry.Birational.RationalMap
AlgebraicGeometry.Scheme.PartialMap.restrict_domain : ∀ {X Y : AlgebraicGeometry.Scheme} (f : X.PartialMap Y) (U : X.Opens) (hU : Dense ↑U) (hU' : U ≤ f.domain),
  (f.restrict U hU hU').domain = U
-- Mathlib.LinearAlgebra.Dual.Basis
Module.Basis.toDual_linearCombination_right : ∀ {R : Type uR} {M : Type uM} {ι : Type uι} [inst : CommSemiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M]
  [inst_3 : DecidableEq ι] (b : Module.Basis ι R M) (f : ι →₀ R) (i : ι),
  (b.toDual (b i)) ((Finsupp.linearCombination R ⇑b) f) = f i
-- Mathlib.Analysis.Convex.Strict
StrictConvex.neg : ∀ {𝕜 : Type u_1} {E : Type u_3} [inst : Ring 𝕜] [inst_1 : PartialOrder 𝕜] [inst_2 : TopologicalSpace E]
  [inst_3 : AddCommGroup E] [inst_4 : Module 𝕜 E] {s : Set E} [IsTopologicalAddGroup E],
  StrictConvex 𝕜 s → StrictConvex 𝕜 (-s)
-- Mathlib.CategoryTheory.Sites.Sieves
CategoryTheory.Sieve.mem_functorPushforward_inverse : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  {Y : C} {X : D} {S : CategoryTheory.Sieve X} {e : C ≌ D} {f : Y ⟶ e.inverse.obj X},
  (CategoryTheory.Sieve.functorPushforward e.inverse S).arrows f ↔
    S.arrows (CategoryTheory.CategoryStruct.comp (e.functor.map f) (e.counit.app X))
-- Mathlib.Topology.Covering.Quotient
isQuotientCoveringMap_quotientMk_of_properlyDiscontinuousSMul : ∀ {E : Type u_1} [inst : TopologicalSpace E] {G : Type u_3} [inst_1 : Group G] [inst_2 : MulAction G E]
  [ContinuousConstSMul G E] [ProperlyDiscontinuousSMul G E] [LocallyCompactSpace E] [T2Space E] [IsCancelSMul G E],
  IsQuotientCoveringMap (Quotient.mk (MulAction.orbitRel G E)) G
-- Mathlib.Data.Nat.ModEq
/-- Cancel right multiplication on both sides of the `≡` and in the modulus.

For cancelling right multiplication in the modulus, see `Nat.ModEq.of_mul_right`.  -/
Nat.ModEq.mul_right_cancel' : ∀ {a b c m : ℕ}, c ≠ 0 → a * c ≡ b * c [MOD m * c] → a ≡ b [MOD m]
-- Mathlib.Order.RelClasses
/-- **Alias** of `LT.lt.trans_eq`. -/
HasSSubset.SSubset.trans_eq : ∀ {α : Type u_1} {a b c : α} [inst : LT α], a < b → b = c → a < c
-- Mathlib.Order.Filter.IsBounded
/-- A bounded function `u` is in particular eventually bounded.  -/
Filter.isBoundedUnder_of : ∀ {α : Type u_1} {β : Type u_2} {r : α → α → Prop} {f : Filter β} {u : β → α},
  (∃ b, ∀ (x : β), r (u x) b) → Filter.IsBoundedUnder r f u
-- Mathlib.AlgebraicGeometry.PullbackCarrier
AlgebraicGeometry.Scheme.Pullback.Triplet.tensorCongr_trans_hom_assoc : ∀ {X Y S : AlgebraicGeometry.Scheme} {f : X ⟶ S} {g : Y ⟶ S} {x y z : AlgebraicGeometry.Scheme.Pullback.Triplet f g}
  (e : x = y) (e' : y = z) {Z : CommRingCat} (h : z.tensor ⟶ Z),
  CategoryTheory.CategoryStruct.comp (AlgebraicGeometry.Scheme.Pullback.Triplet.tensorCongr e).hom
      (CategoryTheory.CategoryStruct.comp (AlgebraicGeometry.Scheme.Pullback.Triplet.tensorCongr e').hom h) =
    CategoryTheory.CategoryStruct.comp (AlgebraicGeometry.Scheme.Pullback.Triplet.tensorCongr ⋯).hom h
-- Mathlib.Order.Category.BddDistLat
BddDistLat.mk.inj : ∀ {toDistLat : DistLat} {isBoundedOrder : BoundedOrder ↑toDistLat} {toDistLat_1 : DistLat}
  {isBoundedOrder_1 : BoundedOrder ↑toDistLat_1},
  { toDistLat := toDistLat, isBoundedOrder := isBoundedOrder } =
      { toDistLat := toDistLat_1, isBoundedOrder := isBoundedOrder_1 } →
    toDistLat = toDistLat_1 ∧ isBoundedOrder ≍ isBoundedOrder_1
-- Mathlib.CategoryTheory.Limits.Final
CategoryTheory.Functor.Initial.limitIso_inv : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  (F : CategoryTheory.Functor C D) [inst_2 : F.Initial] {E : Type u₃} [inst_3 : CategoryTheory.Category.{v₃, u₃} E]
  (G : CategoryTheory.Functor D E) [inst_4 : CategoryTheory.Limits.HasLimit G],
  (CategoryTheory.Functor.Initial.limitIso F G).inv = CategoryTheory.Limits.limit.pre G F
-- Std.Data.ExtTreeMap.Lemmas
Std.ExtTreeMap.contains_insertMany_list : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Std.ExtTreeMap α β cmp} [inst : Std.TransCmp cmp]
  [inst_1 : BEq α] [Std.LawfulBEqCmp cmp] {l : List (α × β)} {k : α},
  (t.insertMany l).contains k = (t.contains k || (List.map Prod.fst l).contains k)
-- Lean.Meta.CongrTheorems
/-- Create a congruence theorem that is useful for the simplifier.
In this kind of theorem, if the i-th argument is a `cast` argument, then the theorem
contains an input `a_i` representing the i-th argument in the left-hand-side, and
it appears with a cast (e.g., `Eq.rec ... a_i ...`) in the right-hand-side.
The idea is that the right-hand-side of this theorem "tells" the simplifier
how the resulting term looks like.  -/
_private.Lean.Meta.CongrTheorems.0.Lean.Meta.mkCongrSimpCore?.mk? : Bool → Lean.Expr → Lean.Meta.FunInfo → Array Lean.Meta.CongrArgKind → Lean.MetaM (Option Lean.Meta.CongrTheorem)
-- Mathlib.Probability.Kernel.IonescuTulcea.Maps
IocProdIoc.eq_1 : ∀ {ι : Type u_1} [inst : LinearOrder ι] [inst_1 : LocallyFiniteOrder ι] [inst_2 : DecidableLE ι] {X : ι → Type u_2}
  (a b c : ι) (x : ((i : ↥(Finset.Ioc a b)) → X ↑i) × ((i : ↥(Finset.Ioc b c)) → X ↑i)) (i : ↥(Finset.Ioc a c)),
  IocProdIoc a b c x i = if h : ↑i ≤ b then x.1 ⟨↑i, ⋯⟩ else x.2 ⟨↑i, ⋯⟩
-- Aesop.Util.UnorderedArraySet
Aesop.UnorderedArraySet : (α : Type u_1) → [BEq α] → Type u_1
-- Mathlib.Analysis.Convex.Function
StrictConvexOn.convex_lt : ∀ {𝕜 : Type u_1} {E : Type u_2} {β : Type u_5} [inst : Semiring 𝕜] [inst_1 : PartialOrder 𝕜] [inst_2 : AddCommMonoid E]
  [inst_3 : AddCommMonoid β] [inst_4 : PartialOrder β] [inst_5 : Module 𝕜 E] [inst_6 : Module 𝕜 β]
  [IsOrderedAddMonoid β] [PosSMulMono 𝕜 β] {s : Set E} {f : E → β},
  StrictConvexOn 𝕜 s f → ∀ (r : β), Convex 𝕜 {x | x ∈ s ∧ f x < r}
-- Std.Time.DateTime.PlainDateTime
/-- Returns the local (civil) date of the `PlainDateTime` as a `Day.Offset` relative to 1970-01-01.
 -/
Std.Time.PlainDateTime.toEpochDay : Std.Time.PlainDateTime → Std.Time.Day.Offset
-- Mathlib.Algebra.Homology.HomotopyCofiber
HomologicalComplex.homotopyCofiber.sndX.eq_1 : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Preadditive C] {ι : Type u_2}
  {c : ComplexShape ι} {F G : HomologicalComplex C c} (φ : F ⟶ G) [inst_2 : HomologicalComplex.HasHomotopyCofiber φ]
  [inst_3 : DecidableRel c.Rel] (i : ι),
  HomologicalComplex.homotopyCofiber.sndX φ i =
    if hi : c.Rel i (c.next i) then
      CategoryTheory.CategoryStruct.comp (HomologicalComplex.homotopyCofiber.XIsoBiprod φ i (c.next i) hi).hom
        CategoryTheory.Limits.biprod.snd
    else (HomologicalComplex.homotopyCofiber.XIso φ i hi).hom
-- Mathlib.Algebra.Algebra.Tower
AlgHom.extendScalarsHomOfSurjective_symm_apply : ∀ {R : Type u} {S : Type v} {A : Type w} [inst : CommSemiring R] [inst_1 : CommSemiring S] [inst_2 : Semiring A]
  [inst_3 : Algebra R S] [inst_4 : Algebra S A] [inst_5 : Algebra R A] [inst_6 : IsScalarTower R S A]
  (h : Function.Surjective ⇑(algebraMap R S)) (f : A →ₐ[S] A),
  (AlgHom.extendScalarsHomOfSurjective h).symm f = AlgHom.restrictScalars R f
-- Lean.Meta.Tactic.Grind.Theorems
/-- A unique identifier corresponding to the origin.  -/
Lean.Meta.Grind.Origin.key : Lean.Meta.Grind.Origin → Lean.Name
-- Mathlib.AlgebraicGeometry.Birational.Composition
AlgebraicGeometry.Scheme.PartialMap.comp_id : ∀ {X Y : AlgebraicGeometry.Scheme} [inst : PreirreducibleSpace ↥X] [inst_1 : Nonempty ↥Y] (f : X.PartialMap Y)
  [inst_2 : AlgebraicGeometry.IsDominant f.hom], f.comp (AlgebraicGeometry.Scheme.PartialMap.id Y) = f
-- Init.Data.Array.Attach
Array.attach_map_val : ∀ {α : Type u_1} {β : Type u_2} (xs : Array α) (f : α → β), Array.map (fun i => f ↑i) xs.attach = Array.map f xs
-- Init.Data.Vector.Count
Vector.count_push_self : ∀ {α : Type u_1} [inst : BEq α] [LawfulBEq α] {n : ℕ} {a : α} {xs : Vector α n},
  Vector.count a (xs.push a) = Vector.count a xs + 1
-- Lean.Meta.LazyDiscrTree
Lean.Meta.LazyDiscrTree.Key.proj.sizeOf_spec : ∀ (a : Lean.Name) (a_1 a_2 : ℕ),
  sizeOf (Lean.Meta.LazyDiscrTree.Key.proj a a_1 a_2) = 1 + sizeOf a + sizeOf a_1 + sizeOf a_2
-- Mathlib.Data.ENat.Basic
/-- A version of `WithTop.map` for `AddHom`s.  -/
AddHom.ENatMap : {N : Type u_2} → [inst : Add N] → (ℕ →ₙ+ N) → ℕ∞ →ₙ+ WithTop N
-- Mathlib.CategoryTheory.Limits.Shapes.Kernels
/-- The kernel of a morphism, expressed as the equalizer with the 0 morphism.  -/
CategoryTheory.Limits.kernel : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C] →
      {X Y : C} → (f : X ⟶ Y) → [CategoryTheory.Limits.HasKernel f] → C
-- Mathlib.Algebra.Ring.ULift
ULift.up_ofNat : ∀ {R : Type u} [inst : NatCast R] (n : ℕ) [inst_1 : n.AtLeastTwo], { down := OfNat.ofNat n } = OfNat.ofNat n
-- Lean.Parser.Do
Lean.Parser.Term.doLetElse.parenthesizer : Lean.PrettyPrinter.Parenthesizer
-- Mathlib.MeasureTheory.Measure.FiniteMeasure
MeasureTheory.FiniteMeasure.map_apply_of_aemeasurable : ∀ {Ω : Type u_1} {Ω' : Type u_2} [inst : MeasurableSpace Ω] [inst_1 : MeasurableSpace Ω']
  (ν : MeasureTheory.FiniteMeasure Ω) {f : Ω → Ω'},
  AEMeasurable f ↑ν → ∀ {A : Set Ω'}, MeasurableSet A → (ν.map f) A = ν (f ⁻¹' A)
-- Std.Data.DTreeMap.Internal.Model
/-- Implementation detail of the tree map  -/
Std.DTreeMap.Internal.Impl.getEntryGT?ₘ' : {α : Type u} → {β : α → Type v} → [Ord α] → α → Std.DTreeMap.Internal.Impl α β → Option ((a : α) × β a)
-- Mathlib.ModelTheory.Basic
FirstOrder.Language.isRelational_sum : ∀ {L : FirstOrder.Language} {L' : FirstOrder.Language} [L.IsRelational] [L'.IsRelational], (L.sum L').IsRelational