mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Probability.Kernel.Basic
ProbabilityTheory.Kernel.const.instIsFiniteKernel : ∀ {α : Type u_1} {β : Type u_2} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} {μβ : MeasureTheory.Measure β}
  [MeasureTheory.IsFiniteMeasure μβ], ProbabilityTheory.IsFiniteKernel (ProbabilityTheory.Kernel.const α μβ)
-- Std.Data.Internal.List.Associative
Std.Internal.List.maxKey?_insertEntry : ∀ {α : Type u} {β : α → Type v} [inst : Ord α] [Std.TransOrd α] [inst_2 : BEq α] [Std.LawfulBEqOrd α] {k : α} {v : β k}
  {l : List ((a : α) × β a)},
  Std.Internal.List.DistinctKeys l →
    Std.Internal.List.maxKey? (Std.Internal.List.insertEntry k v l) =
      some ((Std.Internal.List.maxKey? l).elim k fun k' => if (compare k' k).isLE = true then k else k')
-- Mathlib.CategoryTheory.Square
CategoryTheory.Square.toArrowArrowFunctor'_obj_right_left : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] (sq : CategoryTheory.Square C),
  (CategoryTheory.Square.toArrowArrowFunctor'.obj sq).right.left = sq.X₃
-- Mathlib.Analysis.Normed.Lp.WithLp
WithLp.equiv_symm_apply : ∀ (p : ENNReal) (V : Type u_4), ⇑(WithLp.equiv p V).symm = WithLp.toLp p
-- Mathlib.Topology.Instances.AddCircle.Defs
AddCircle.addOrderOf_period_div : ∀ {𝕜 : Type u_1} [inst : Field 𝕜] {p : 𝕜} [inst_1 : LinearOrder 𝕜] [IsStrictOrderedRing 𝕜] [hp : Fact (0 < p)] {n : ℕ},
  0 < n → addOrderOf ↑(p / ↑n) = n
-- Mathlib.Probability.Kernel.Integral
ProbabilityTheory.Kernel.integral_piecewise : ∀ {α : Type u_1} {β : Type u_2} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} {κ : ProbabilityTheory.Kernel α β}
  {E : Type u_3} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] {η : ProbabilityTheory.Kernel α β} {s : Set α}
  {hs : MeasurableSet s} [inst_2 : DecidablePred fun x => x ∈ s] (a : α) (g : β → E),
  ∫ (b : β), g b ∂(ProbabilityTheory.Kernel.piecewise hs κ η) a =
    if a ∈ s then ∫ (b : β), g b ∂κ a else ∫ (b : β), g b ∂η a
-- Mathlib.NumberTheory.NumberField.Basic
/-- The canonical map from `𝓞 K` to `K` is injective.

This is a convenient abbreviation for `map_eq_zero_iff` applied to
`FaithfulSMul.algebraMap_injective`.
 -/
NumberField.RingOfIntegers.coe_eq_zero_iff : ∀ {K : Type u_1} [inst : Field K] {x : NumberField.RingOfIntegers K},
  (algebraMap (NumberField.RingOfIntegers K) K) x = 0 ↔ x = 0
-- Mathlib.RingTheory.PicardGroup
Module.Invertible.instTensorProduct_2 : ∀ (R : Type u) (M : Type v) (A : Type u_4) [inst : CommSemiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M]
  [Module.Invertible R M] [inst_4 : CommSemiring A] [inst_5 : Algebra R A] (L : Type u_5) [inst_6 : AddCommMonoid L]
  [inst_7 : Module R L] [inst_8 : Module A L] [inst_9 : IsScalarTower R A L] [Module.Invertible A L],
  Module.Invertible A (TensorProduct R L M)
-- Mathlib.CategoryTheory.Sites.Descent.DescentData
CategoryTheory.Pseudofunctor.DescentData.instIsIsoαCategoryObjLocallyDiscreteOppositeCatMkOpHom : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C]
  {F : CategoryTheory.Pseudofunctor (CategoryTheory.LocallyDiscrete Cᵒᵖ) CategoryTheory.Cat} {ι : Type t} {S : C}
  {X : ι → C} {f : (i : ι) → X i ⟶ S} (D : F.DescentData f) {Y : C} (q : Y ⟶ S) {i₁ i₂ : ι} (f₁ : Y ⟶ X i₁)
  (f₂ : Y ⟶ X i₂) (hf₁ : CategoryTheory.CategoryStruct.comp f₁ (f i₁) = q)
  (hf₂ : CategoryTheory.CategoryStruct.comp f₂ (f i₂) = q), CategoryTheory.IsIso (D.hom q f₁ f₂ hf₁ hf₂)
-- Init.Data.Iterators.Basic
/-- The relation of plausible successors on `IterM.TerminationMeasures.Finite`. It is well-founded
if there is a `Finite` instance.
 -/
Std.IterM.TerminationMeasures.Finite.Rel : {α : Type w} →
  {m : Type w → Type w'} →
    {β : Type w} →
      [inst : Std.Iterator α m β] →
        Std.IterM.TerminationMeasures.Finite α m → Std.IterM.TerminationMeasures.Finite α m → Prop
-- Mathlib.Topology.MetricSpace.UniformConvergence
UniformOnFun.edist_le : ∀ {α : Type u_1} {β : Type u_2} {𝔖 : Set (Set α)} [inst : PseudoEMetricSpace β] [inst_1 : Finite ↑𝔖]
  {f g : UniformOnFun α β 𝔖} {C : ENNReal},
  edist f g ≤ C ↔ ∀ x ∈ ⋃₀ 𝔖, edist ((UniformOnFun.toFun 𝔖) f x) ((UniformOnFun.toFun 𝔖) g x) ≤ C
-- Init.Data.Int.Linear
Int.Internal.Linear.Poly.combine'.match_1.congr_eq_4 : ∀ (motive : Int.Internal.Linear.Poly → Int.Internal.Linear.Poly → Sort u_1) (p₁ p₂ : Int.Internal.Linear.Poly)
  (h_1 : (k₁ k₂ : ℤ) → motive (Int.Internal.Linear.Poly.num k₁) (Int.Internal.Linear.Poly.num k₂))
  (h_2 :
    (k₁ a : ℤ) →
      (x : Int.Internal.Linear.Var) →
        (p : Int.Internal.Linear.Poly) → motive (Int.Internal.Linear.Poly.num k₁) (Int.Internal.Linear.Poly.add a x p))
  (h_3 :
    (a : ℤ) →
      (x : Int.Internal.Linear.Var) →
        (p : Int.Internal.Linear.Poly) →
          (k₂ : ℤ) → motive (Int.Internal.Linear.Poly.add a x p) (Int.Internal.Linear.Poly.num k₂))
  (h_4 :
    (a₁ : ℤ) →
      (x₁ : Int.Internal.Linear.Var) →
        (p₁ : Int.Internal.Linear.Poly) →
          (a₂ : ℤ) →
            (x₂ : Int.Internal.Linear.Var) →
              (p₂ : Int.Internal.Linear.Poly) →
                motive (Int.Internal.Linear.Poly.add a₁ x₁ p₁) (Int.Internal.Linear.Poly.add a₂ x₂ p₂))
  (a₁ : ℤ) (x₁ : Int.Internal.Linear.Var) (p₁_1 : Int.Internal.Linear.Poly) (a₂ : ℤ) (x₂ : Int.Internal.Linear.Var)
  (p₂_1 : Int.Internal.Linear.Poly),
  p₁ = Int.Internal.Linear.Poly.add a₁ x₁ p₁_1 →
    p₂ = Int.Internal.Linear.Poly.add a₂ x₂ p₂_1 →
      (match p₁, p₂ with
        | Int.Internal.Linear.Poly.num k₁, Int.Internal.Linear.Poly.num k₂ => h_1 k₁ k₂
        | Int.Internal.Linear.Poly.num k₁, Int.Internal.Linear.Poly.add a x p => h_2 k₁ a x p
        | Int.Internal.Linear.Poly.add a x p, Int.Internal.Linear.Poly.num k₂ => h_3 a x p k₂
        | Int.Internal.Linear.Poly.add a₁ x₁ p₁, Int.Internal.Linear.Poly.add a₂ x₂ p₂ => h_4 a₁ x₁ p₁ a₂ x₂ p₂) ≍
        h_4 a₁ x₁ p₁_1 a₂ x₂ p₂_1
-- Mathlib.NumberTheory.Height.Basic
/-- A type class capturing an admissible family of absolute values.  -/
Height.AdmissibleAbsValues : (K : Type u_1) → [Field K] → Type u_1
-- Mathlib.Algebra.FreeMonoid.Basic
FreeAddMonoid.recOn_of_add : ∀ {α : Type u_1} {motive : FreeAddMonoid α → Sort u_6} (x : α) (xs : FreeAddMonoid α) (zero : motive 0)
  (of_add : (x : α) → (xs : FreeAddMonoid α) → motive xs → motive (FreeAddMonoid.of x + xs)),
  FreeAddMonoid.recOn (FreeAddMonoid.of x + xs) zero of_add = of_add x xs (FreeAddMonoid.recOn xs zero of_add)
-- Mathlib.Algebra.Module.Submodule.Pointwise
Submodule.pointwise_smul_def : ∀ {α : Type u_1} {R : Type u_2} {M : Type u_3} [inst : Semiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M]
  [inst_3 : Monoid α] [inst_4 : DistribMulAction α M] [inst_5 : SMulCommClass α R M] {a : α} {S : Submodule R M},
  a • S = Submodule.map (DistribSMul.toLinearMap R M a) S
-- Mathlib.GroupTheory.Coxeter.Length
CoxeterSystem.length_eq_zero_iff : ∀ {B : Type u_1} {W : Type u_2} [inst : Group W] {M : CoxeterMatrix B} (cs : CoxeterSystem M W) {w : W},
  cs.length w = 0 ↔ w = 1
-- Mathlib.Order.Filter.Basic
/-- **Alias** of `LE.le.eventuallyLE`. -/
HasSubset.Subset.eventuallyLE : ∀ {α : Type u_1} {l : Filter α} {s t : Set α}, s ⊆ t → s ≤ᶠ[l] t
-- Mathlib.Analysis.InnerProductSpace.Orthogonal
Submodule.isOrtho_sup_right : ∀ {𝕜 : Type u_1} {E : Type u_2} [inst : RCLike 𝕜] [inst_1 : NormedAddCommGroup E] [inst_2 : InnerProductSpace 𝕜 E]
  {U V₁ V₂ : Submodule 𝕜 E}, U ⟂ V₁ ⊔ V₂ ↔ U ⟂ V₁ ∧ U ⟂ V₂
-- Mathlib.CategoryTheory.EquivalenceRelation
CategoryTheory.SymmetricRelation.symmetry₁_assoc : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] {R X : C} {p₁ p₂ : R ⟶ X}
  (self : CategoryTheory.SymmetricRelation p₁ p₂) {Z : C} (h : X ⟶ Z),
  CategoryTheory.CategoryStruct.comp self.s (CategoryTheory.CategoryStruct.comp p₁ h) =
    CategoryTheory.CategoryStruct.comp p₂ h
-- Mathlib.Algebra.GroupWithZero.Associated
Associates.le_zero : ∀ {M : Type u_1} [inst : CommMonoidWithZero M] (a : Associates M), a ≤ 0
-- Mathlib.LinearAlgebra.Matrix.Echelon.Pivot
/-- The pivots of a matrix are unique.  -/
Matrix.IsPivotedBy.unique : ∀ {m : Type u_1} {n : Type u_2} {R : Type u_3} [inst : Zero R] {A : Matrix m n R} {l : m → WithTop n}
  [inst_1 : LinearOrder n] [inst_2 : LT m] {l' : m → WithTop n}, A.IsPivotedBy l → A.IsPivotedBy l' → l = l'
-- Mathlib.RingTheory.Ideal.Height
Ideal.finiteHeight_iff : ∀ {R : Type u_1} [inst : CommRing R] (I : Ideal R), I.FiniteHeight ↔ I = ⊤ ∨ I.height ≠ ⊤
-- Mathlib.Probability.Kernel.IonescuTulcea.Traj
ProbabilityTheory.Kernel.partialTraj_compProd_eq_map_traj : ∀ {X : ℕ → Type u_1} [inst : (n : ℕ) → MeasurableSpace (X n)]
  {κ : (n : ℕ) → ProbabilityTheory.Kernel ((i : ↥(Finset.Iic n)) → X ↑i) (X (n + 1))}
  [inst_1 : ∀ (n : ℕ), ProbabilityTheory.IsMarkovKernel (κ n)] {a b : ℕ},
  a ≤ b →
    ∀ {x₀ : (n : ↥(Finset.Iic a)) → X ↑n},
      ((ProbabilityTheory.Kernel.partialTraj κ a b) x₀).compProd (κ b) =
        MeasureTheory.Measure.map (fun x => (Preorder.frestrictLe b x, x (b + 1)))
          ((ProbabilityTheory.Kernel.traj κ a) x₀)
-- Lean.Meta.Tactic.Grind.Arith.Cutsat.Types
Lean.Meta.Grind.Arith.Cutsat.DvdCnstrProof.reorder.sizeOf_spec : ∀ (c : Lean.Meta.Grind.Arith.Cutsat.DvdCnstr),
  sizeOf (Lean.Meta.Grind.Arith.Cutsat.DvdCnstrProof.reorder c) = 1 + sizeOf c
-- Mathlib.RingTheory.QuotSMulTop
QuotSMulTop.equivTensorQuot_naturality : ∀ {R : Type u_2} [inst : CommRing R] (r : R) {M : Type u_1} {M' : Type u_3} [inst_1 : AddCommGroup M]
  [inst_2 : Module R M] [inst_3 : AddCommGroup M'] [inst_4 : Module R M'] (f : M →ₗ[R] M'),
  ↑(QuotSMulTop.equivTensorQuot r M') ∘ₗ (QuotSMulTop.map r) f =
    LinearMap.rTensor (R ⧸ Ideal.span {r}) f ∘ₗ ↑(QuotSMulTop.equivTensorQuot r M)
-- Init.Data.String.Lemmas.Pattern.Find.Pred
String.Slice.find?_bool_eq_some_iff_splits : ∀ {p : Char → Bool} {s : String.Slice} {pos : s.Pos},
  s.find? p = some pos ↔ ∃ t c u, pos.Splits t (String.singleton c ++ u) ∧ p c = true ∧ ∀ d ∈ t.toList, p d = false
-- Mathlib.Probability.Independence.ZeroOne
ProbabilityTheory.Kernel.measure_zero_or_one_of_measurableSet_limsup_atTop : ∀ {α : Type u_1} {Ω : Type u_2} {ι : Type u_3} {_mα : MeasurableSpace α} {s : ι → MeasurableSpace Ω}
  {m0 : MeasurableSpace Ω} {κ : ProbabilityTheory.Kernel α Ω} {μα : MeasureTheory.Measure α} [inst : SemilatticeSup ι]
  [NoMaxOrder ι] [Nonempty ι],
  (∀ (n : ι), s n ≤ m0) →
    ProbabilityTheory.Kernel.iIndep s κ μα → ∀ {t : Set Ω}, MeasurableSet t → ∀ᵐ (a : α) ∂μα, (κ a) t = 0 ∨ (κ a) t = 1
-- Mathlib.Geometry.Euclidean.Projection
/-- A point equals its orthogonal projection if and only if it lies in
the subspace.  -/
EuclideanGeometry.orthogonalProjection_eq_self_iff : ∀ {𝕜 : Type u_1} {V : Type u_2} {P : Type u_3} [inst : RCLike 𝕜] [inst_1 : NormedAddCommGroup V]
  [inst_2 : InnerProductSpace 𝕜 V] [inst_3 : MetricSpace P] [inst_4 : NormedAddTorsor V P] {s : AffineSubspace 𝕜 P}
  [inst_5 : Nonempty ↥s] [inst_6 : s.direction.HasOrthogonalProjection] {p : P},
  ↑((EuclideanGeometry.orthogonalProjection s) p) = p ↔ p ∈ s
-- Lean.Elab.Tactic.Omega.Frontend
/-- Implementation of the `omega` algorithm, and handling disjunctions.  -/
Lean.Elab.Tactic.Omega.omegaImpl : Lean.Elab.Tactic.Omega.MetaProblem → Lean.Elab.Tactic.Omega.OmegaM Lean.Expr
-- Mathlib.RingTheory.HahnSeries.Addition
HahnSeries.coeff_add' : ∀ {Γ : Type u_1} {R : Type u_3} [inst : PartialOrder Γ] [inst_1 : AddMonoid R] (x y : HahnSeries Γ R),
  (x + y).coeff = x.coeff + y.coeff
-- Mathlib.CategoryTheory.Sites.Descent.DescentDataPrime
/-- The compatibility morphisms after pulling back to the chosen pullbacks. It follows
from the conditions `pullHom'_hom_self` and `pullHom'_hom_comp` that these morphisms
are isomorphisms.  -/
CategoryTheory.Pseudofunctor.DescentData'.hom : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    {F : CategoryTheory.Pseudofunctor (CategoryTheory.LocallyDiscrete Cᵒᵖ) CategoryTheory.Cat} →
      {ι : Type t} →
        {S : C} →
          {X : ι → C} →
            {f : (i : ι) → X i ⟶ S} →
              {sq : (i j : ι) → CategoryTheory.Limits.ChosenPullback (f i) (f j)} →
                {sq₃ : (i₁ i₂ i₃ : ι) → CategoryTheory.Limits.ChosenPullback₃ (sq i₁ i₂) (sq i₂ i₃) (sq i₁ i₃)} →
                  (self : F.DescentData' sq sq₃) →
                    (i j : ι) →
                      (F.map (sq i j).p₁.op.toLoc).toFunctor.obj (self.obj i) ⟶
                        (F.map (sq i j).p₂.op.toLoc).toFunctor.obj (self.obj j)
-- Mathlib.RingTheory.Unramified.Locus
/-- A prime `𝔭` of `R` is unramified in `A` if every prime ideal `𝔓` of `A` lying over `𝔭` is
unramified .  -/
Algebra.IsUnramifiedIn : {R : Type u_1} → [inst : CommRing R] → (A : Type u_2) → [inst_1 : CommRing A] → [Algebra R A] → Ideal R → Prop
-- Lean.Compiler.IR.Basic
Lean.IR.Alt.ctor.sizeOf_spec : ∀ (info : Lean.IR.CtorInfo) (b : Lean.IR.FnBody), sizeOf (Lean.IR.Alt.ctor info b) = 1 + sizeOf info + sizeOf b
-- Mathlib.Order.Max
NoTopOrder.to_noMaxOrder : ∀ (α : Type u_3) [inst : LinearOrder α] [NoTopOrder α], NoMaxOrder α
-- Mathlib.LinearAlgebra.Matrix.Ideal
TwoSidedIdeal.asIdeal_matrix : ∀ {R : Type u_1} (n : Type u_2) [inst : Ring R] [inst_1 : Fintype n] [inst_2 : DecidableEq n] (I : TwoSidedIdeal R),
  TwoSidedIdeal.asIdeal (TwoSidedIdeal.matrix n I) = Ideal.matrix n (TwoSidedIdeal.asIdeal I)
-- Mathlib.Analysis.InnerProductSpace.Symmetric
LinearMap.IsSymmetric.smul : ∀ {𝕜 : Type u_1} {E : Type u_2} [inst : RCLike 𝕜] [inst_1 : SeminormedAddCommGroup E] [inst_2 : InnerProductSpace 𝕜 E]
  {c : 𝕜}, (starRingEnd 𝕜) c = c → ∀ {T : E →ₗ[𝕜] E}, T.IsSymmetric → (c • T).IsSymmetric
-- Mathlib.NumberTheory.Cyclotomic.Basic
/-- If `S` is finite and `IsCyclotomicExtension S A B`, then `B` is a finite `A`-algebra.  -/
IsCyclotomicExtension.finite : ∀ (S : Set ℕ) (A : Type u) (B : Type v) [inst : CommRing A] [inst_1 : CommRing B] [inst_2 : Algebra A B] [IsDomain B]
  [h₁ : Finite ↑S] [h₂ : IsCyclotomicExtension S A B], Module.Finite A B
-- Mathlib.FieldTheory.Separable
IsSeparable.of_integral : ∀ (F : Type u_1) [inst : Field F] {K : Type u_2} [inst_1 : Ring K] [inst_2 : Algebra F K] [IsDomain K]
  [Algebra.IsIntegral F K] [CharZero F] (x : K), IsSeparable F x
-- Mathlib.Topology.ContinuousMap.Algebra
ContinuousMap.instAddZeroClassOfContinuousAdd : {α : Type u_1} →
  {β : Type u_2} →
    [inst : TopologicalSpace α] →
      [inst_1 : TopologicalSpace β] → [inst_2 : AddZeroClass β] → [ContinuousAdd β] → AddZeroClass C(α, β)
-- Init.Data.Iterators.Consumers.Monadic.Loop
/-- Internal implementation detail of the iterator library.  -/
Std.IteratorLoop.WithWF.it : {α : Type w} →
  {m : Type w → Type w'} →
    {β : Type w} →
      [inst : Std.Iterator α m β] →
        {γ : Type x} →
          {PlausibleForInStep : β → γ → ForInStep γ → Prop} →
            {hwf : Std.IteratorLoop.WellFounded α m PlausibleForInStep} →
              Std.IteratorLoop.WithWF α m PlausibleForInStep hwf → Std.IterM m β
-- Std.Data.TreeSet.Lemmas
Std.TreeSet.contains_emptyc : ∀ {α : Type u} {cmp : α → α → Ordering} {k : α}, ∅.contains k = false
-- Mathlib.CategoryTheory.Limits.Shapes.Products
/-- Construct a morphism between categorical products (indexed by the same type)
from a family of morphisms between the factors.
 -/
CategoryTheory.Limits.Pi.map : {β : Type w} →
  {C : Type u} →
    [inst : CategoryTheory.Category.{v, u} C] →
      {f g : β → C} →
        [inst_1 : CategoryTheory.Limits.HasProduct f] →
          [inst_2 : CategoryTheory.Limits.HasProduct g] → ((b : β) → f b ⟶ g b) → (∏ᶜ f ⟶ ∏ᶜ g)
-- Std.Data.HashMap.RawLemmas
/-- This is a restatement of `contains_of_contains_insertIfNew` that is written to exactly match the proof
obligation in the statement of `getElem_insertIfNew`.  -/
Std.HashMap.Raw.contains_of_contains_insertIfNew' : ∀ {α : Type u} {β : Type v} {m : Std.HashMap.Raw α β} [inst : BEq α] [inst_1 : Hashable α] [EquivBEq α]
  [LawfulHashable α],
  m.WF →
    ∀ {k a : α} {v : β},
      (m.insertIfNew k v).contains a = true → ¬((k == a) = true ∧ m.contains k = false) → m.contains a = true
-- Mathlib.Algebra.Group.WithOne.Basic
WithOne.lift_symm_apply : ∀ {α : Type u} {β : Type v} [inst : Mul α] [inst_1 : MulOneClass β] (f : WithOne α →* β) (x : α),
  (WithOne.lift.symm f) x = f ↑x
-- Mathlib.Algebra.Order.Monoid.Unbundled.Basic
instIsLeftCancelAddOfAddLeftReflectLE : ∀ {α : Type u_1} [inst : Add α] [inst_1 : PartialOrder α] [AddLeftReflectLE α], IsLeftCancelAdd α
-- Init.Data.List.Basic
List.isPrefixOf_cons_nil : ∀ {α : Type u} {a : α} {as : List α} [inst : BEq α], (a :: as).isPrefixOf [] = false
-- Mathlib.MeasureTheory.Measure.LogLikelihoodRatio
MeasureTheory.integral_rnDeriv_mul_log : ∀ {α : Type u_1} {mα : MeasurableSpace α} {μ ν : MeasureTheory.Measure α} [MeasureTheory.SigmaFinite μ]
  [μ.HaveLebesgueDecomposition ν],
  μ.AbsolutelyContinuous ν →
    ∫ (a : α), (μ.rnDeriv ν a).toReal * Real.log (μ.rnDeriv ν a).toReal ∂ν = ∫ (a : α), MeasureTheory.llr μ ν a ∂μ
-- Mathlib.CategoryTheory.Limits.Preserves.Basic
CategoryTheory.Limits.comp_reflectsLimitsOfShape : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  {J : Type w} [inst_2 : CategoryTheory.Category.{w', w} J] {E : Type u₃} [ℰ : CategoryTheory.Category.{v₃, u₃} E]
  (F : CategoryTheory.Functor C D) (G : CategoryTheory.Functor D E) [CategoryTheory.Limits.ReflectsLimitsOfShape J F]
  [CategoryTheory.Limits.ReflectsLimitsOfShape J G], CategoryTheory.Limits.ReflectsLimitsOfShape J (F.comp G)
-- Mathlib.Combinatorics.Additive.AP.Three.Defs
mulRothNumber.eq_1 : ∀ {α : Type u_2} [inst : DecidableEq α] [inst_1 : Monoid α],
  mulRothNumber =
    { toFun := fun s => Nat.findGreatest (fun m => ∃ t ⊆ s, t.card = m ∧ ThreeGPFree ↑t) s.card, monotone' := ⋯ }
-- Lean.Data.Lsp.Capabilities
Lean.Lsp.WindowClientCapabilities.mk.injEq : ∀ (showDocument? showDocument?_1 : Option Lean.Lsp.ShowDocumentClientCapabilities),
  ({ showDocument? := showDocument? } = { showDocument? := showDocument?_1 }) = (showDocument? = showDocument?_1)
-- Mathlib.Computability.AkraBazzi.SumTransform
AkraBazziRecurrence.min_bi.congr_simp : ∀ {α : Type u_1} [inst : Finite α] [inst_1 : Nonempty α] (b b_1 : α → ℝ),
  b = b_1 → AkraBazziRecurrence.min_bi b = AkraBazziRecurrence.min_bi b_1
-- Mathlib.Probability.Independence.Basic
ProbabilityTheory.iIndep_iff : ∀ {Ω : Type u_1} {ι : Type u_2} (m : ι → MeasurableSpace Ω) {_mΩ : MeasurableSpace Ω} (μ : MeasureTheory.Measure Ω),
  ProbabilityTheory.iIndep m μ ↔
    ∀ (s : Finset ι) {f : ι → Set Ω}, (∀ i ∈ s, MeasurableSet (f i)) → μ (⋂ i ∈ s, f i) = ∏ i ∈ s, μ (f i)
-- Init.Data.List.Pairwise
List.Pairwise.and_mem : ∀ {α : Type u_1} {R : α → α → Prop} {l : List α}, List.Pairwise R l ↔ List.Pairwise (fun x y => x ∈ l ∧ y ∈ l ∧ R x y) l
-- Lean.Data.Lsp.Window
Lean.Lsp.ShowMessageParams.mk.injEq : ∀ (type : Lean.Lsp.MessageType) (message : String) (type_1 : Lean.Lsp.MessageType) (message_1 : String),
  ({ type := type, message := message } = { type := type_1, message := message_1 }) =
    (type = type_1 ∧ message = message_1)
-- Mathlib.MeasureTheory.Group.FundamentalDomain
MeasureTheory.IsFundamentalDomain.nullMeasurableSet_smul : ∀ {G : Type u_1} {α : Type u_3} [inst : Group G] [inst_1 : MulAction G α] [inst_2 : MeasurableSpace α] {s : Set α}
  {μ : MeasureTheory.Measure α} [MeasurableConstSMul G α] [MeasureTheory.SMulInvariantMeasure G α μ],
  MeasureTheory.IsFundamentalDomain G s μ → ∀ (g : G), MeasureTheory.NullMeasurableSet (g • s) μ
-- Mathlib.Data.Sum.Order
OrderIso.sumLexCongr_refl : ∀ {α : Type u_1} {β : Type u_2} [inst : LE α] [inst_1 : LE β],
  (OrderIso.refl α).sumLexCongr (OrderIso.refl β) = OrderIso.refl (α ⊕ₗ β)
-- Std.Data.ExtDTreeMap.Lemmas
Std.ExtDTreeMap.mem_insertIfNew_self : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t : Std.ExtDTreeMap α β cmp} [inst : Std.TransCmp cmp] {k : α}
  {v : β k}, k ∈ t.insertIfNew k v
-- Mathlib.CategoryTheory.Adjunction.Additive
/-- If we have an adjunction `adj : F ⊣ G` of functors between preadditive categories,
and if `F` is additive, then the hom set equivalence upgrades to an `AddEquiv`.
Note that `F` is additive if and only if `G` is, by `Adjunction.right_adjoint_additive` and
`Adjunction.left_adjoint_additive`.
 -/
CategoryTheory.Adjunction.homAddEquiv : {C : Type u₁} →
  {D : Type u₂} →
    [inst : CategoryTheory.Category.{v₁, u₁} C] →
      [inst_1 : CategoryTheory.Category.{v₂, u₂} D] →
        [inst_2 : CategoryTheory.Preadditive C] →
          [inst_3 : CategoryTheory.Preadditive D] →
            {F : CategoryTheory.Functor C D} →
              {G : CategoryTheory.Functor D C} →
                (F ⊣ G) → [F.Additive] → (X : C) → (Y : D) → (F.obj X ⟶ Y) ≃+ (X ⟶ G.obj Y)
-- Mathlib.Order.GaloisConnection.Basic
/-- Lift the suprema along a Galois coinsertion  -/
GaloisCoinsertion.liftSemilatticeSup : {α : Type u} →
  {β : Type v} →
    {u : α → β} →
      {l : β → α} → [inst : PartialOrder β] → [inst_1 : SemilatticeSup α] → GaloisCoinsertion l u → SemilatticeSup β
-- Lean.Meta.Tactic.Grind.Arith.Simproc
Lean.Meta.Grind.Arith.normFieldInv : Lean.Meta.Simp.Simproc
-- Mathlib.Computability.Encoding
/-- An encoding function of the positive binary numbers in `Bool`.  -/
Computability.encodePosNum : PosNum → List Bool
-- Mathlib.Algebra.Module.Congruence.Defs
/-- The kernel of an `AddActionHom` as a congruence relation.  -/
VAddCon.ker : {R : Type u_1} →
  {S : Type u_2} →
    {M : Type u_3} → {N : Type u_4} → [inst : VAdd R M] → [inst_1 : VAdd S N] → {φ : R → S} → (M →ₑ[φ] N) → VAddCon R M
-- Lean.Elab.Quotation
Lean.Elab.Term.Quotation.instReprMatchResult : Repr Lean.Elab.Term.Quotation.MatchResult
-- Mathlib.Algebra.Category.AlgCat.Limits
/-- `limit.π (F ⋙ forget (AlgCat R)) j` as an `AlgHom`.  -/
AlgCat.limitπAlgHom : {R : Type u} →
  [inst : CommRing R] →
    {J : Type v} →
      [inst_1 : CategoryTheory.Category.{t, v} J] →
        (F : CategoryTheory.Functor J (AlgCat R)) →
          [inst_2 : Small.{w, max v w} ↑(F.comp (CategoryTheory.forget (AlgCat R))).sections] →
            (j : J) →
              (CategoryTheory.Limits.Types.Small.limitCone (F.comp (CategoryTheory.forget (AlgCat R)))).pt →ₐ[R]
                (F.comp (CategoryTheory.forget (AlgCat R))).obj j
-- Mathlib.Analysis.CStarAlgebra.ApproximateUnit
CStarAlgebra.instNeBotApproximateUnit : ∀ (A : Type u_1) [inst : NonUnitalCStarAlgebra A] [inst_1 : PartialOrder A] [inst_2 : StarOrderedRing A],
  (CStarAlgebra.approximateUnit A).NeBot
-- Init.Data.Range.Polymorphic.NatLemmas
Nat.toArray_rio_eq_nil : ∀ {n : ℕ}, n = 0 → (*...n).toArray = #[]
-- Init.Data.Rat.Basic
/-- The inverse of a rational number. Note: `inv 0 = 0`. (This definition is `@[irreducible]`
because you don't want to unfold it. Use `Rat.inv_def` instead.)
 -/
Rat.inv : ℚ → ℚ
-- Mathlib.CategoryTheory.Subobject.ArtinianObject
CategoryTheory.isArtinianObject_iff_not_strictAnti : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] (X : C),
  CategoryTheory.IsArtinianObject X ↔ ∀ (f : ℕ → CategoryTheory.Subobject X), ¬StrictAnti f
-- Mathlib.MeasureTheory.MeasurableSpace.Embedding
/-- The space `Π i : Fin 2, α i` is measurably equivalent to `α 0 × α 1`.  -/
MeasurableEquiv.piFinTwo : (α : Fin 2 → Type u_8) → [inst : (i : Fin 2) → MeasurableSpace (α i)] → ((i : Fin 2) → α i) ≃ᵐ α 0 × α 1
-- Lean.Meta.Tactic.Grind.AC.Types
Lean.Meta.Grind.AC.EqCnstrProof.simp_ac.injEq : ∀ (lhs : Bool) (s : Lean.Grind.AC.Seq) (c₁ c₂ : Lean.Meta.Grind.AC.EqCnstr) (lhs_1 : Bool) (s_1 : Lean.Grind.AC.Seq)
  (c₁_1 c₂_1 : Lean.Meta.Grind.AC.EqCnstr),
  (Lean.Meta.Grind.AC.EqCnstrProof.simp_ac lhs s c₁ c₂ = Lean.Meta.Grind.AC.EqCnstrProof.simp_ac lhs_1 s_1 c₁_1 c₂_1) =
    (lhs = lhs_1 ∧ s = s_1 ∧ c₁ = c₁_1 ∧ c₂ = c₂_1)
-- Mathlib.Combinatorics.Schnirelmann
/-- If two sets `A` and `B` have Schnirelmann densities with sum at least 1, and both sets
contain zero, then every natural number is sum of an element of `A` and an element of `B`.
Note that we cannot omit the assumption that both sets contain zero, as shown by the
counterexample `A = B = Odd`.
 -/
add_eq_univ_of_one_le_schirelmannDensity_add_schnirelmannDensity : ∀ {A B : Set ℕ} [inst : DecidablePred fun x => x ∈ A] [inst_1 : DecidablePred fun x => x ∈ B],
  0 ∈ A → 0 ∈ B → 1 ≤ schnirelmannDensity A + schnirelmannDensity B → A + B = Set.univ