mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic
Real.sin_pi_over_two_pow_succ : ∀ (n : ℕ), Real.sin (Real.pi / 2 ^ (n + 2)) = √(2 - Real.sqrtTwoAddSeries 0 n) / 2
-- Mathlib.Analysis.Normed.Algebra.UnitizationL1
WithLp.unitization_mul : ∀ {𝕜 : Type u_1} {A : Type u_2} [inst : NormedField 𝕜] [inst_1 : NonUnitalNormedRing A] [inst_2 : NormedSpace 𝕜 A]
  [inst_3 : IsScalarTower 𝕜 A A] [inst_4 : SMulCommClass 𝕜 A A] (x y : WithLp 1 (Unitization 𝕜 A)),
  (x * y).ofLp = x.ofLp * y.ofLp
-- Mathlib.MeasureTheory.Integral.Prod
/-- Change the order of Bochner integration.  -/
MeasureTheory.integral_integral_swap : ∀ {α : Type u_1} {β : Type u_2} {E : Type u_3} [inst : MeasurableSpace α] [inst_1 : MeasurableSpace β]
  {μ : MeasureTheory.Measure α} {ν : MeasureTheory.Measure β} [inst_2 : NormedAddCommGroup E] [MeasureTheory.SFinite ν]
  [inst_4 : NormedSpace ℝ E] [MeasureTheory.SFinite μ] ⦃f : α → β → E⦄,
  MeasureTheory.Integrable (Function.uncurry f) (μ.prod ν) →
    ∫ (x : α), ∫ (y : β), f x y ∂ν ∂μ = ∫ (y : β), ∫ (x : α), f x y ∂μ ∂ν
-- Init.Data.Vector.Perm
Vector.Perm.append : ∀ {α : Type u_1} {m n : ℕ} {xs ys : Vector α m} {as bs : Vector α n},
  xs.Perm ys → as.Perm bs → (xs ++ as).Perm (ys ++ bs)
-- Mathlib.Analysis.SpecialFunctions.Complex.Arg
Complex.arg_eq_pi_iff : ∀ {z : ℂ}, z.arg = Real.pi ↔ z.re < 0 ∧ z.im = 0
-- Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Rpow.Basic
IsStrictlyPositive.rpow : ∀ {A : Type u_1} [inst : PartialOrder A] [inst_1 : Ring A] [inst_2 : StarRing A] [inst_3 : TopologicalSpace A]
  [inst_4 : StarOrderedRing A] [inst_5 : Algebra ℝ A] [inst_6 : ContinuousFunctionalCalculus ℝ A IsSelfAdjoint]
  [inst_7 : NonnegSpectrumClass ℝ A] (a : A) (y : ℝ),
  autoParam (IsStrictlyPositive a) IsStrictlyPositive.rpow._auto_1 → IsStrictlyPositive (a ^ y)
-- Lean.Compiler.LCNF.Basic
/-- Parameters.
 -/
Lean.Compiler.LCNF.Signature.params : {pu : Lean.Compiler.LCNF.Purity} → Lean.Compiler.LCNF.Signature pu → Array (Lean.Compiler.LCNF.Param pu)
-- Mathlib.MeasureTheory.OuterMeasure.AE
/-- The “almost everywhere” filter of co-null sets.  -/
MeasureTheory.ae : {α : Type u_1} →
  {F : Type u_3} → [inst : FunLike F (Set α) ENNReal] → [MeasureTheory.OuterMeasureClass F α] → F → Filter α
-- Mathlib.Geometry.Convex.Cone.Basic
ConvexCone.coe_inf : ∀ {R : Type u_2} {M : Type u_4} [inst : Semiring R] [inst_1 : PartialOrder R] [inst_2 : AddCommMonoid M]
  [inst_3 : SMul R M] (C₁ C₂ : ConvexCone R M), ↑(C₁ ⊓ C₂) = ↑C₁ ∩ ↑C₂
-- Mathlib.Analysis.Distribution.SchwartzSpace.Basic
_private.Mathlib.Analysis.Distribution.SchwartzSpace.Basic.0.SchwartzMap.seminormAux_smul_le : ∀ {𝕜 : Type u_2} {E : Type u_5} {F : Type u_6} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E]
  [inst_2 : NormedAddCommGroup F] [inst_3 : NormedSpace ℝ F] [inst_4 : NormedField 𝕜] [inst_5 : NormedSpace 𝕜 F]
  [inst_6 : SMulCommClass ℝ 𝕜 F] (k n : ℕ) (c : 𝕜) (f : SchwartzMap E F),
  SchwartzMap.seminormAux✝ k n (c • f) ≤ ‖c‖ * SchwartzMap.seminormAux✝ k n f
-- Mathlib.Algebra.Group.Prod
/-- Addition as an additive monoid homomorphism.  -/
addAddMonoidHom : {α : Type u_6} → [inst : AddCommMonoid α] → α × α →+ α
-- Mathlib.Analysis.Convex.Gauge
gauge_ball : ∀ {E : Type u_2} [inst : SeminormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] {r : ℝ},
  0 ≤ r → ∀ (x : E), gauge (Metric.ball 0 r) x = ‖x‖ / r
-- Std.Data.DTreeMap.Raw.Lemmas
Std.DTreeMap.Raw.maxKey?_insertIfNew : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t : Std.DTreeMap.Raw α β cmp} [Std.TransCmp cmp],
  t.WF →
    ∀ {k : α} {v : β k},
      (t.insertIfNew k v).maxKey? = some (t.maxKey?.elim k fun k' => if cmp k' k = Ordering.lt then k else k')
-- Mathlib.Tactic.CongrExclamation
/-- Patterns to use when doing intro.  -/
CongrState.patterns : CongrState → List (Lean.TSyntax `rintroPat)
-- Mathlib.Order.UpperLower.Prod
UpperSet.prod_mono_right : ∀ {α : Type u_1} {β : Type u_2} [inst : Preorder α] [inst_1 : Preorder β] {s : UpperSet α} {t₁ t₂ : UpperSet β},
  t₁ ≤ t₂ → s ×ˢ t₁ ≤ s ×ˢ t₂
-- Init.Data.Array.Lemmas
_private.Init.Data.Array.Lemmas.0.Array.getElem_shrink_loop : ∀ {α : Type u_1} {xs : Array α} {n i : ℕ} (h : i < (Array.shrink.loop✝ n xs).size), (Array.shrink.loop✝ n xs)[i] = xs[i]
-- Mathlib.Algebra.EuclideanDomain.Basic
/-- The well-founded relation in a Euclidean Domain satisfying `a % b ≺ b` for `b ≠ 0`  -/
_private.Mathlib.Algebra.EuclideanDomain.Basic.0.EuclideanDomain.«term_≺_» : Lean.TrailingParserDescr
-- Mathlib.RingTheory.Valuation.Basic
Valuation.IsNontrivial.exists_one_lt : ∀ {K : Type u_7} [inst : DivisionRing K] {Γ₀ : Type u_8} [inst_1 : LinearOrderedCommGroupWithZero Γ₀]
  {v : Valuation K Γ₀} [hv : v.IsNontrivial], ∃ x, 1 < v x
-- Mathlib.Geometry.Euclidean.Sphere.Basic
EuclideanGeometry.Sphere.isDiameter_iff_left_mem_and_pointReflection_center_left : ∀ {V : Type u_1} {P : Type u_2} [inst : NormedAddCommGroup V] [inst_1 : NormedSpace ℝ V] [inst_2 : MetricSpace P]
  [inst_3 : NormedAddTorsor V P] {s : EuclideanGeometry.Sphere P} {p₁ p₂ : P},
  s.IsDiameter p₁ p₂ ↔ p₁ ∈ s ∧ (Equiv.pointReflection s.center) p₁ = p₂
-- Mathlib.AlgebraicGeometry.ZariskisMainTheorem
AlgebraicGeometry.IsFinite.eq_proper_inf_locallyQuasiFinite : @AlgebraicGeometry.IsFinite = @AlgebraicGeometry.IsProper ⊓ @AlgebraicGeometry.LocallyQuasiFinite
-- Init.Data.SInt.Lemmas
Int16.toInt_minValue : Int16.minValue.toInt = -2 ^ 15
-- Std.Tactic.BVDecide.Bitblast.BVExpr.Basic
Std.Tactic.BVDecide.BVExpr.var.injEq : ∀ {w : ℕ} (idx idx_1 : ℕ), (Std.Tactic.BVDecide.BVExpr.var idx = Std.Tactic.BVDecide.BVExpr.var idx_1) = (idx = idx_1)
-- Mathlib.MeasureTheory.Integral.SetToL1
MeasureTheory.setToFun_smul : ∀ {α : Type u_1} {E : Type u_2} {F : Type u_3} {𝕜 : Type u_6} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E]
  [inst_2 : NormedAddCommGroup F] [inst_3 : NormedSpace ℝ F] {m : MeasurableSpace α} {μ : MeasureTheory.Measure α}
  {T : Set α → E →L[ℝ] F} {C : ℝ} [inst_4 : NormedDivisionRing 𝕜] [inst_5 : Module 𝕜 E] [NormSMulClass 𝕜 E]
  [inst_7 : Module 𝕜 F] [NormSMulClass 𝕜 F] (hT : MeasureTheory.DominatedFinMeasAdditive μ T C),
  (∀ (c : 𝕜) (s : Set α) (x : E), (T s) (c • x) = c • (T s) x) →
    ∀ (c : 𝕜) (f : α → E), MeasureTheory.setToFun μ T hT (c • f) = c • MeasureTheory.setToFun μ T hT f
-- Mathlib.CategoryTheory.Adhesive.Basic
CategoryTheory.IsPushout.IsVanKampen.isPullback_of_mono_right : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {W X Y Z : C} {f : W ⟶ X} {g : W ⟶ Y} {h : X ⟶ Z} {i : Y ⟶ Z}
  [CategoryTheory.Mono g] {H : CategoryTheory.IsPushout f g h i}, H.IsVanKampen → CategoryTheory.IsPullback f g h i
-- Mathlib.LinearAlgebra.QuadraticForm.Dual
/-- `QuadraticForm.dualProd` commutes (isometrically) with `QuadraticForm.prod`.  -/
QuadraticForm.dualProdProdIsometry : {R : Type u_1} →
  {M : Type u_2} →
    {N : Type u_3} →
      [inst : CommSemiring R] →
        [inst_1 : AddCommMonoid M] →
          [inst_2 : AddCommMonoid N] →
            [inst_3 : Module R M] →
              [inst_4 : Module R N] →
                QuadraticMap.IsometryEquiv (QuadraticForm.dualProd R (M × N))
                  (QuadraticMap.prod (QuadraticForm.dualProd R M) (QuadraticForm.dualProd R N))
-- Init.Data.Iterators.Combinators.Monadic.FlatMap
Std.Iterators.Types.Flatten.instIteratorLoop : {α α₂ β : Type w} →
  {m : Type w → Type w'} →
    {n : Type u_1 → Type u_2} →
      [inst : Monad m] →
        [Monad n] →
          [inst_2 : Std.Iterator α m (Std.IterM m β)] →
            [inst_3 : Std.Iterator α₂ m β] → Std.IteratorLoop (Std.Iterators.Types.Flatten α α₂ β m) m n
-- Std.Data.HashSet.Raw
Std.HashSet.Raw.instMembershipOfBEqOfHashable : {α : Type u} → [BEq α] → [Hashable α] → Membership α (Std.HashSet.Raw α)
-- Mathlib.Data.Matrix.Basic
/-- `Matrix.diagonal` as an `AddMonoidHom`.  -/
Matrix.diagonalAddMonoidHom : (n : Type u_3) → (α : Type u_11) → [DecidableEq n] → [inst : AddZeroClass α] → (n → α) →+ Matrix n n α
-- Mathlib.LinearAlgebra.LinearDisjoint
/-- Linear disjointness is preserved by taking multiplicative opposite.  -/
Submodule.linearDisjoint_op : ∀ {R : Type u} {S : Type v} [inst : CommSemiring R] [inst_1 : Semiring S] [inst_2 : Algebra R S] {M N : Submodule R S},
  M.LinearDisjoint N ↔
    (Submodule.equivOpposite.symm (MulOpposite.op N)).LinearDisjoint (Submodule.equivOpposite.symm (MulOpposite.op M))
-- Mathlib.CategoryTheory.Action.Monoidal
CategoryTheory.Functor.mapAction_μ_hom : ∀ {V : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} V] {G : Type u_2} [inst_1 : Monoid G] {W : Type u_3}
  [inst_2 : CategoryTheory.Category.{v_2, u_3} W] [inst_3 : CategoryTheory.MonoidalCategory V]
  [inst_4 : CategoryTheory.MonoidalCategory W] (F : CategoryTheory.Functor V W) [inst_5 : F.LaxMonoidal]
  (X Y : Action V G),
  (CategoryTheory.Functor.LaxMonoidal.μ (F.mapAction G) X Y).hom = CategoryTheory.Functor.LaxMonoidal.μ F X.V Y.V
-- Mathlib.RingTheory.DedekindDomain.Ideal.Lemmas
/-- **Alias** of `Ideal.prod_normalizedFactors_eq_self`. -/
prod_normalizedFactors_eq_self : ∀ {T : Type u_4} [inst : CommRing T] [inst_1 : IsDedekindDomain T] {I : Ideal T},
  I ≠ ⊥ → (UniqueFactorizationMonoid.normalizedFactors I).prod = I
-- Mathlib.GroupTheory.OrderOfElement
addOrderOf_fst_dvd_addOrderOf : ∀ {α : Type u_4} {β : Type u_5} [inst : AddMonoid α] [inst_1 : AddMonoid β] {x : α × β}, addOrderOf x.1 ∣ addOrderOf x
-- Mathlib.Algebra.Group.Action.Pointwise.Finset
Finset.mul_singleton : ∀ {α : Type u_2} [inst : Mul α] [inst_1 : DecidableEq α] {s : Finset α} (a : α), s * {a} = MulOpposite.op a • s
-- Mathlib.Algebra.Category.Grp.EpiMono
GrpCat.SurjectiveOfEpiAuxs.comp_eq : ∀ {A B : GrpCat} (f : A ⟶ B),
  CategoryTheory.CategoryStruct.comp f (GrpCat.ofHom (GrpCat.SurjectiveOfEpiAuxs.g f)) =
    CategoryTheory.CategoryStruct.comp f (GrpCat.ofHom (GrpCat.SurjectiveOfEpiAuxs.h f))
-- Mathlib.Topology.Algebra.Valued.WithVal
WithVal.congr_symm_apply : ∀ {R : Type u_1} {Γ₀ : Type u_2} [inst : LinearOrderedCommGroupWithZero Γ₀] [inst_1 : Ring R] (v : Valuation R Γ₀)
  {S : Type u_3} [inst_2 : Ring S] {Λ₀ : Type u_4} [inst_3 : LinearOrderedCommGroupWithZero Λ₀] (w : Valuation S Λ₀)
  (f : R ≃+* S) (x : WithVal w), (WithVal.congr v w f).symm x = WithVal.toVal v (f.symm x.ofVal)
-- Mathlib.Algebra.BigOperators.Group.Finset.Piecewise
Finset.prod_dite_of_true : ∀ {ι : Type u_1} {M : Type u_3} {s : Finset ι} [inst : CommMonoid M] {p : ι → Prop} [inst_1 : DecidablePred p]
  (h : ∀ i ∈ s, p i) (f : (i : ι) → p i → M) (g : (i : ι) → ¬p i → M),
  (∏ i ∈ s, if hi : p i then f i hi else g i hi) = ∏ i, f ↑i ⋯
-- Aesop.Rule.Forward
Aesop.ForwardRule.toForwardRuleInfo : Aesop.ForwardRule → Aesop.ForwardRuleInfo
-- Mathlib.Topology.Category.TopCat.GrothendieckTopology
TopCat.instIsStableUnderCompositionPrecoverage : TopCat.precoverage.IsStableUnderComposition
-- Mathlib.MeasureTheory.Group.Arithmetic
measurableSMul_of_mul : ∀ (M : Type u_2) [inst : Mul M] [inst_1 : MeasurableSpace M] [MeasurableMul M], MeasurableSMul M M
-- Mathlib.RingTheory.Invariant.Basic
Ideal.Quotient.stabilizerQuotientInertiaEquiv_mk : ∀ {A : Type u_1} {B : Type u_2} [inst : CommRing A] [inst_1 : CommRing B] [inst_2 : Algebra A B] (G : Type u_3)
  [inst_3 : Group G] [inst_4 : Finite G] [inst_5 : MulSemiringAction G B] [inst_6 : SMulCommClass G A B] (P : Ideal A)
  (Q : Ideal B) [inst_7 : Q.IsPrime] [inst_8 : Q.LiesOver P] [inst_9 : Algebra.IsInvariant A B G]
  (g : ↥(MulAction.stabilizer G Q)),
  (Ideal.Quotient.stabilizerQuotientInertiaEquiv G P Q) ↑g = (Ideal.Quotient.stabilizerHom Q P G) g
-- Aesop.Search.Expansion.Simp
Aesop.SimpResult.simplified.inj : ∀ {newGoal : Lean.MVarId} {usedTheorems : Lean.Meta.Simp.UsedSimps} {newGoal_1 : Lean.MVarId}
  {usedTheorems_1 : Lean.Meta.Simp.UsedSimps},
  Aesop.SimpResult.simplified newGoal usedTheorems = Aesop.SimpResult.simplified newGoal_1 usedTheorems_1 →
    newGoal = newGoal_1 ∧ usedTheorems = usedTheorems_1
-- Mathlib.Data.Finite.Defs
/-- A set is finite if the corresponding `Subtype` is finite,
i.e., if there exists a natural `n : ℕ` and an equivalence `s ≃ Fin n`.  -/
Set.Finite : {α : Type u} → Set α → Prop
-- Init.Data.List.Basic
List.beq_cons₂ : ∀ {α : Type u} [inst : BEq α] {a b : α} {as bs : List α}, (a :: as).beq (b :: bs) = (a == b && as.beq bs)
-- Mathlib.CategoryTheory.Equivalence
CategoryTheory.Iso.compInverseIso_inv_app : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  {E : Type u₃} [inst_2 : CategoryTheory.Category.{v₃, u₃} E] {F : CategoryTheory.Functor C E}
  {G : CategoryTheory.Functor C D} {H : D ≌ E} (i : F ≅ G.comp H.functor) (X : C),
  i.compInverseIso.inv.app X =
    CategoryTheory.CategoryStruct.comp (H.unitIso.hom.app (G.obj X)) (H.inverse.map (i.inv.app X))
-- Std.Data.DTreeMap.Lemmas
Std.DTreeMap.getKey?_map : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t : Std.DTreeMap α β cmp} {γ : α → Type w} [Std.TransCmp cmp]
  {f : (a : α) → β a → γ a} {k : α}, (Std.DTreeMap.map f t).getKey? k = t.getKey? k
-- Init.Data.List.Nat.Modify
List.modifyHead_dropLast : ∀ {α : Type u_1} {l : List α} {f : α → α}, List.modifyHead f l.dropLast = (List.modifyHead f l).dropLast
-- Std.Http.Protocol.H1.Error
Std.Http.Protocol.H1.Error.invalidChunk.sizeOf_spec : sizeOf Std.Http.Protocol.H1.Error.invalidChunk = 1
-- Mathlib.Analysis.SpecificLimits.Basic
geom_le : ∀ {u : ℕ → ℝ} {c : ℝ}, 0 ≤ c → ∀ (n : ℕ), (∀ k < n, c * u k ≤ u (k + 1)) → c ^ n * u 0 ≤ u n
-- Mathlib.Data.Finset.Image
Finset.filter_image : ∀ {α : Type u_1} {β : Type u_2} [inst : DecidableEq β] {f : α → β} {s : Finset α} {p : β → Prop}
  [inst_1 : DecidablePred p], Finset.filter p (Finset.image f s) = Finset.image f ({a ∈ s | p (f a)})
-- Mathlib.Data.Bool.Basic
Bool.and_le_right : ∀ (x y : Bool), (x && y) ≤ y
-- Mathlib.NumberTheory.Padics.PadicVal.Basic
padicValNat_self : ∀ {p : ℕ} [Fact (Nat.Prime p)], padicValNat p p = 1
-- Lean.Data.Json.Basic
Lean.JsonNumber.shiftr : Lean.JsonNumber → ℕ → Lean.JsonNumber
-- Mathlib.Algebra.Ring.Subsemiring.Basic
/-- Restriction of a ring homomorphism to a subsemiring of the codomain.  -/
RingHom.codRestrict : {R : Type u} →
  {S : Type v} →
    [inst : NonAssocSemiring R] →
      [inst_1 : NonAssocSemiring S] →
        {σS : Type u_2} →
          [inst_2 : SetLike σS S] →
            [inst_3 : SubsemiringClass σS S] → (f : R →+* S) → (s : σS) → (∀ (x : R), f x ∈ s) → R →+* ↥s
-- Mathlib.Algebra.Category.MonCat.Colimits
MonCat.Colimits.descFunLift.eq_def : ∀ {J : Type v} [inst : CategoryTheory.Category.{u, v} J] (F : CategoryTheory.Functor J MonCat)
  (s : CategoryTheory.Limits.Cocone F) (x : MonCat.Colimits.Prequotient F),
  MonCat.Colimits.descFunLift F s x =
    match x with
    | MonCat.Colimits.Prequotient.of j x => (CategoryTheory.ConcreteCategory.hom (s.ι.app j)) x
    | MonCat.Colimits.Prequotient.one => 1
    | x.mul y => MonCat.Colimits.descFunLift F s x * MonCat.Colimits.descFunLift F s y
-- Init.Data.Range.Polymorphic.UpwardEnumerable
Std.PRange.LawfulUpwardEnumerable.succMany?_succ_eq_succ?_bind_succMany? : ∀ {α : Type u_1} [inst : Std.PRange.UpwardEnumerable α] [Std.PRange.LawfulUpwardEnumerable α] (n : ℕ) (a : α),
  Std.PRange.succMany? (n + 1) a = (Std.PRange.succ? a).bind fun x => Std.PRange.succMany? n x
-- Mathlib.SetTheory.Ordinal.Exponential
Ordinal.right_le_opow : ∀ {a : Ordinal.{u_1}} (b : Ordinal.{u_1}), 1 < a → b ≤ a ^ b
-- Mathlib.Geometry.Manifold.Sheaf.Smooth
smoothSheafCommRing.forgetStalk_hom_comp_evalHom_assoc : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {EM : Type u_2} [inst_1 : NormedAddCommGroup EM]
  [inst_2 : NormedSpace 𝕜 EM] {HM : Type u_3} [inst_3 : TopologicalSpace HM] (IM : ModelWithCorners 𝕜 EM HM)
  {E : Type u_4} [inst_4 : NormedAddCommGroup E] [inst_5 : NormedSpace 𝕜 E] {H : Type u_5} [inst_6 : TopologicalSpace H]
  (I : ModelWithCorners 𝕜 E H) (M : Type u) [inst_7 : TopologicalSpace M] [inst_8 : ChartedSpace HM M] (R : Type u)
  [inst_9 : TopologicalSpace R] [inst_10 : ChartedSpace H R] [inst_11 : CommRing R] [inst_12 : ContMDiffRing I (↑⊤) R]
  (x : ↑(TopCat.of M)) {Z : Type u} (h : R ⟶ Z),
  CategoryTheory.CategoryStruct.comp (smoothSheafCommRing.forgetStalk IM I M R x).hom
      (CategoryTheory.CategoryStruct.comp (smoothSheaf.evalHom IM I R x) h) =
    CategoryTheory.CategoryStruct.comp
      (TypeCat.ofHom ⇑(CategoryTheory.ConcreteCategory.hom (smoothSheafCommRing.evalHom IM I M R x))) h
-- Mathlib.Order.SupClosed
InfClosed.inter : ∀ {α : Type u_3} [inst : SemilatticeInf α] {s t : Set α}, InfClosed s → InfClosed t → InfClosed (s ∩ t)
-- Init.Grind.Interactive
/-- `lia` linear integer arithmetic.  -/
Lean.Parser.Tactic.Grind.lia : Lean.ParserDescr
-- Lean.Meta.Tactic.Simp.SimpAll
Lean.Meta.SimpAll.State.mk : Bool →
  Lean.MVarId →
    Array Lean.Meta.SimpAll.Entry →
      Lean.Meta.Simp.Context →
        Lean.Meta.Simp.SimprocsArray → Lean.Meta.Simp.UsedSimps → Lean.Meta.Simp.Diagnostics → Lean.Meta.SimpAll.State
-- Mathlib.Combinatorics.SimpleGraph.Basic
SimpleGraph.edgeSet_eq_iff : ∀ {V : Type u} (G : SimpleGraph V) (s : Set (Sym2 V)),
  G.edgeSet = s ↔ G = SimpleGraph.fromEdgeSet s ∧ Disjoint s Sym2.diagSet
-- Mathlib.CategoryTheory.Limits.Types.ColimitType
/-- Structure which expresses that `c : F.CoconeTypes`
satisfies the universal property of the colimit of types:
compatible families of maps `F.obj j → T` (where `T`
is any type in a specified universe) descend in a unique
way as maps `c.pt → T`.  -/
CategoryTheory.Functor.CoconeTypes.IsColimitCore : {J : Type u} →
  [inst : CategoryTheory.Category.{v, u} J] →
    {F : CategoryTheory.Functor J (Type w₀)} → F.CoconeTypes → Type (max (max (max u w₀) w₁) (w₂ + 1))
-- Mathlib.Analysis.SpecialFunctions.Log.Base
Real.tendsto_logb_nhdsNE_zero : ∀ {b : ℝ}, 1 < b → Filter.Tendsto (Real.logb b) (nhdsWithin 0 {0}ᶜ) Filter.atBot
-- Std.Data.Iterators.Combinators.Monadic.Zip
Std.Iterators.Types.Zip.rel₁_of_left : ∀ {m : Type w → Type w'} {α₁ β₁ : Type w} [inst : Std.Iterator α₁ m β₁] {α₂ β₂ : Type w} [inst_1 : Std.Iterator α₂ m β₂]
  [inst_2 : Std.Iterators.Finite α₁ m] [inst_3 : Std.Iterators.Productive α₂ m] {it' it : Std.IterM m (β₁ × β₂)},
  it'.internalState.left.finitelyManySteps.Rel it.internalState.left.finitelyManySteps →
    Std.Iterators.Types.Zip.Rel₁ m it' it
-- Mathlib.Order.Hom.WithTopBot
LatticeHom.withTopWithBot_comp : ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} [inst : Lattice α] [inst_1 : Lattice β] [inst_2 : Lattice γ]
  (f : LatticeHom β γ) (g : LatticeHom α β), (f.comp g).withTopWithBot = f.withTopWithBot.comp g.withTopWithBot
-- Mathlib.CategoryTheory.Monoidal.Internal.FunctorCategory
CategoryTheory.Monoidal.MonFunctorCategoryEquivalence.unitIso_inv_app_hom_app : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  [inst_2 : CategoryTheory.MonoidalCategory D] (X : CategoryTheory.Mon (CategoryTheory.Functor C D)) (x : C),
  (CategoryTheory.Monoidal.MonFunctorCategoryEquivalence.unitIso.inv.app X).hom.app x =
    CategoryTheory.CategoryStruct.id (X.X.obj x)
-- Std.Data.DTreeMap.Basic
/-- Tries to retrieve the largest key in the tree map, returning `fallback` if the tree map is empty.
 -/
Std.DTreeMap.maxKeyD : {α : Type u} → {β : α → Type v} → {cmp : α → α → Ordering} → Std.DTreeMap α β cmp → α → α
-- Mathlib.RingTheory.UniqueFactorizationDomain.Defs
UniqueFactorizationMonoid.factors_zero : ∀ {α : Type u_1} [inst : CommMonoidWithZero α] [inst_1 : UniqueFactorizationMonoid α],
  UniqueFactorizationMonoid.factors 0 = 0
-- Batteries.Data.List.Matcher
/-- The pattern for the matcher  -/
List.Matcher.pattern : {α : Type u_1} → List.Matcher α → List α
-- Mathlib.Analysis.InnerProductSpace.TensorProduct
LinearIsometry.toLinearMap_lTensor : ∀ {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} {G : Type u_4} [inst : RCLike 𝕜] [inst_1 : NormedAddCommGroup E]
  [inst_2 : InnerProductSpace 𝕜 E] [inst_3 : NormedAddCommGroup F] [inst_4 : InnerProductSpace 𝕜 F]
  [inst_5 : NormedAddCommGroup G] [inst_6 : InnerProductSpace 𝕜 G] (f : F →ₗᵢ[𝕜] G),
  (LinearIsometry.lTensor E f).toLinearMap = LinearMap.lTensor E f.toLinearMap
-- Mathlib.Algebra.Order.IsBotOne
/-- **Alias** of the reverse direction of `one_lt_iff_ne_one`. -/
one_lt_of_ne_one : ∀ {α : Type u_1} {a : α} [inst : PartialOrder α] [inst_1 : One α] [IsBotOneClass α], a ≠ 1 → 1 < a
-- Mathlib.Order.Rel.GaloisConnection
/-- `leftDual` maps every element `J` to `rightFixedPoints`.  -/
SetRel.leftDual_mem_rightFixedPoint : ∀ {α : Type u_1} {β : Type u_2} (R : SetRel α β) (J : Set α), R.leftDual J ∈ R.rightFixedPoints
-- Mathlib.Algebra.Group.Hom.Basic
MonoidHom.mul_apply : ∀ {M : Type u_2} {N : Type u_3} [inst : MulOneClass M] [inst_1 : CommMonoid N] (f g : M →* N) (x : M),
  (f * g) x = f x * g x
-- Mathlib.Analysis.Normed.Module.Multilinear.Curry
continuousMultilinearCurryRightEquiv_symm_apply : ∀ {𝕜 : Type u} {n : ℕ} {Ei : Fin n.succ → Type wEi} {G : Type wG} [inst : NontriviallyNormedField 𝕜]
  [inst_1 : (i : Fin n.succ) → NormedAddCommGroup (Ei i)] [inst_2 : (i : Fin n.succ) → NormedSpace 𝕜 (Ei i)]
  [inst_3 : NormedAddCommGroup G] [inst_4 : NormedSpace 𝕜 G] (f : Ei i.castSucc [×n]→L[𝕜] Ei (Fin.last n) →L[𝕜] G)
  (v : (i : Fin n.succ) → Ei i),
  ((continuousMultilinearCurryRightEquiv 𝕜 Ei G).symm f) v = (f (Fin.init v)) (v (Fin.last n))
-- Mathlib.Algebra.Module.Congruence.Defs
/-- A congruence relation that preserves additive action.  -/
VAddCon : (S : Type u_2) → (M : Type u_3) → [VAdd S M] → Type u_3
-- Mathlib.CategoryTheory.Triangulated.Functor
CategoryTheory.Functor.mapTriangleCommShiftIso.congr_simp : ∀ {C : Type u_1} {D : Type u_2} [inst : CategoryTheory.Category.{v_1, u_1} C]
  [inst_1 : CategoryTheory.Category.{v_2, u_2} D] [inst_2 : CategoryTheory.HasShift C ℤ]
  [inst_3 : CategoryTheory.HasShift D ℤ] (F : CategoryTheory.Functor C D) [inst_4 : F.CommShift ℤ]
  [inst_5 : CategoryTheory.Preadditive C] [inst_6 : CategoryTheory.Preadditive D] [inst_7 : F.Additive] (n : ℤ),
  F.mapTriangleCommShiftIso n = F.mapTriangleCommShiftIso n
-- Mathlib.Data.Ordmap.Invariants
_private.Mathlib.Data.Ordmap.Invariants.0.Ordnode.rotateR.match_1.splitter : {α : Type u_1} →
  (motive : Ordnode α → α → Ordnode α → Sort u_2) →
    (x : Ordnode α) →
      (x_1 : α) →
        (x_2 : Ordnode α) →
          ((size : ℕ) →
              (l : Ordnode α) →
                (x : α) → (m : Ordnode α) → (y : α) → (r : Ordnode α) → motive (Ordnode.node size l x m) y r) →
            ((y : α) → (r : Ordnode α) → motive Ordnode.nil y r) → motive x x_1 x_2
-- Std.Data.DHashMap.Lemmas
_private.Std.Data.DHashMap.Lemmas.0.Std.DHashMap.Option.map_cast_apply : ∀ {γ γ' : Type u} (h : γ = γ') (x : Option γ), Option.map (cast h) x = cast ⋯ x
-- Mathlib.GroupTheory.OreLocalization.Basic
/-- Scalar multiplication in a monoid localization.  -/
OreLocalization.hsmul : {R : Type u_1} →
  {M : Type u_3} →
    {X : Type u_4} →
      [inst : Monoid M] →
        {S : Submonoid M} →
          [inst_1 : OreLocalization.OreSet S] →
            [inst_2 : MulAction M X] → [SMul R M] → R → OreLocalization S X → OreLocalization S X
-- Mathlib.NumberTheory.NumberField.CanonicalEmbedding.ConvexBody
NumberField.mixedEmbedding.convexBodySum_mem : ∀ (K : Type u_1) [inst : Field K] [inst_1 : NumberField K] (B : ℝ) {x : K},
  (NumberField.mixedEmbedding K) x ∈ NumberField.mixedEmbedding.convexBodySum K B ↔ ∑ w, ↑w.mult * ↑w x ≤ B
-- Mathlib.Analysis.InnerProductSpace.Symmetric
LinearMap.IsSymmetric.conj_inner_sym : ∀ {𝕜 : Type u_1} {E : Type u_2} [inst : RCLike 𝕜] [inst_1 : SeminormedAddCommGroup E] [inst_2 : InnerProductSpace 𝕜 E]
  {T : E →ₗ[𝕜] E}, T.IsSymmetric → ∀ (x y : E), (starRingEnd 𝕜) (inner 𝕜 (T x) y) = inner 𝕜 (T y) x
-- Mathlib.CategoryTheory.ObjectProperty.ColimitsOfShape
CategoryTheory.ObjectProperty.isClosedUnderColimitsOfShape_iff_op : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] (P : CategoryTheory.ObjectProperty C) (J : Type u')
  [inst_1 : CategoryTheory.Category.{v', u'} J], P.IsClosedUnderColimitsOfShape J ↔ P.op.IsClosedUnderLimitsOfShape Jᵒᵖ
-- Mathlib.CategoryTheory.FiberedCategory.BasedCategory
/-- The bicategory of based categories.  -/
CategoryTheory.BasedCategory.bicategory : {𝒮 : Type u₁} → [inst : CategoryTheory.Category.{v₁, u₁} 𝒮] → CategoryTheory.Bicategory (CategoryTheory.BasedCategory 𝒮)