mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Topology.Category.Compactum
/-- The functor from Compactum to CompHaus.  -/
compactumToCompHaus : CategoryTheory.Functor Compactum CompHaus
-- Mathlib.CategoryTheory.Limits.Shapes.Kernels
/-- The cokernel of the image inclusion of a morphism `f` is isomorphic to the cokernel of `f`.

(This result requires that the factorisation through the image is an epimorphism.
This holds in any category with equalizers.)
 -/
CategoryTheory.Limits.cokernelImageι : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C] →
      {X Y : C} →
        (f : X ⟶ Y) →
          [inst_2 : CategoryTheory.Limits.HasImage f] →
            [inst_3 : CategoryTheory.Limits.HasCokernel (CategoryTheory.Limits.image.ι f)] →
              [inst_4 : CategoryTheory.Limits.HasCokernel f] →
                [CategoryTheory.Epi (CategoryTheory.Limits.factorThruImage f)] →
                  CategoryTheory.Limits.cokernel (CategoryTheory.Limits.image.ι f) ≅ CategoryTheory.Limits.cokernel f
-- Mathlib.Analysis.Asymptotics.Lemmas
Asymptotics.IsBigO.listProd : ∀ {α : Type u_1} {R : Type u_13} {𝕜 : Type u_15} [inst : SeminormedRing R] [inst_1 : NormedDivisionRing 𝕜]
  {l : Filter α} {ι : Type u_17} {L : List ι} {f : ι → α → R} {g : ι → α → 𝕜},
  (∀ i ∈ L, f i =O[l] g i) →
    (fun x => (List.map (fun x_1 => f x_1 x) L).prod) =O[l] fun x => (List.map (fun x_1 => g x_1 x) L).prod
-- Mathlib.LinearAlgebra.Projectivization.Subspace
Projectivization.Subspace.mk.congr_simp : ∀ {K : Type u_1} {V : Type u_2} [inst : DivisionRing K] [inst_1 : AddCommGroup V] [inst_2 : Module K V]
  (carrier carrier_1 : Set (Projectivization K V)) (e_carrier : carrier = carrier_1)
  (mem_add' :
    ∀ (v w : V) (hv : v ≠ 0) (hw : w ≠ 0) (hvw : v + w ≠ 0),
      Projectivization.mk K v hv ∈ carrier →
        Projectivization.mk K w hw ∈ carrier → Projectivization.mk K (v + w) hvw ∈ carrier),
  { carrier := carrier, mem_add' := mem_add' } = { carrier := carrier_1, mem_add' := ⋯ }
-- Mathlib.CategoryTheory.Limits.Shapes.Diagonal
CategoryTheory.Limits.pullback.instIsSplitEpiSnd : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] {X Y : C} (f : X ⟶ Y)
  [inst_1 : CategoryTheory.Limits.HasPullback f f], CategoryTheory.IsSplitEpi (CategoryTheory.Limits.pullback.snd f f)
-- Mathlib.Topology.Algebra.Module.Spaces.UniformConvergenceCLM
UniformConvergenceCLM.isUniformInducing_postcomp : ∀ {𝕜₁ : Type u_1} {𝕜₂ : Type u_2} [inst : NormedField 𝕜₁] [inst_1 : NormedField 𝕜₂] (σ : 𝕜₁ →+* 𝕜₂) {E : Type u_3}
  {F : Type u_4} {G : Type u_5} [inst_2 : AddCommGroup E] [inst_3 : Module 𝕜₁ E] [inst_4 : TopologicalSpace E]
  [inst_5 : AddCommGroup F] [inst_6 : Module 𝕜₂ F] [inst_7 : AddCommGroup G] [inst_8 : UniformSpace G]
  [inst_9 : IsUniformAddGroup G] {𝕜₃ : Type u_6} [inst_10 : NormedField 𝕜₃] [inst_11 : Module 𝕜₃ G] {τ : 𝕜₂ →+* 𝕜₃}
  {ρ : 𝕜₁ →+* 𝕜₃} [inst_12 : RingHomCompTriple σ τ ρ] [inst_13 : UniformSpace F] [inst_14 : IsUniformAddGroup F]
  (g : F →SL[τ] G), IsUniformInducing ⇑g → ∀ (𝔖 : Set (Set E)), IsUniformInducing g.comp
-- Mathlib.Analysis.SpecialFunctions.Log.Basic
Real.log_pow : ∀ (x : ℝ) (n : ℕ), Real.log (x ^ n) = ↑n * Real.log x
-- Lean.MetavarContext
Lean.MetavarContext.getExprAssignmentDomain : Lean.MetavarContext → Array Lean.MVarId
-- Mathlib.Algebra.BigOperators.ModEq
Int.prod_modEq_single : ∀ {α : Type u_1} {n : ℤ} {f : α → ℤ} {s : Finset α} {a : α},
  (a ∉ s → f a ≡ 1 [ZMOD n]) → (∀ x ∈ s, x ≠ a → f x ≡ 1 [ZMOD n]) → ∏ x ∈ s, f x ≡ f a [ZMOD n]
-- Mathlib.Data.Multiset.Powerset
Multiset.Nodup.powersetCard : ∀ {α : Type u_1} {n : ℕ} {s : Multiset α}, s.Nodup → (Multiset.powersetCard n s).Nodup
-- Mathlib.LinearAlgebra.Vandermonde
Matrix.det_vandermonde_id_eq_superFactorial : ∀ {R : Type u_1} [inst : CommRing R] (n : ℕ), (Matrix.vandermonde fun i => ↑↑i).det = ↑n.superFactorial
-- Std.Data.DTreeMap.Raw.Lemmas
Std.DTreeMap.Raw.getKey!_eq_default_of_contains_eq_false : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t : Std.DTreeMap.Raw α β cmp} [Std.TransCmp cmp]
  [inst : Inhabited α], t.WF → ∀ {a : α}, t.contains a = false → t.getKey! a = default
-- Init.Data.Repr
/-- Quotes the character to its representation as a character literal, surrounded by single quotes and
escaped as necessary.

Examples:
 * `'L'.quote = "'L'"`
 * `'"'.quote = "'\\\"'"`
 -/
Char.quote : Char → String
-- Mathlib.NumberTheory.FLT.Three
_private.Mathlib.NumberTheory.FLT.Three.0.FermatLastTheoremForThreeGen.Solution.lambda_sq_div_u₅_mul : ∀ {K : Type u_1} [inst : Field K] {ζ : K} {hζ : IsPrimitiveRoot ζ 3} (S : FermatLastTheoremForThreeGen.Solution✝ hζ)
  [inst_1 : NumberField K] [inst_2 : IsCyclotomicExtension {3} ℚ K],
  (hζ.toInteger - 1) ^ 2 ∣
    ↑(FermatLastTheoremForThreeGen.Solution.u₅✝ S) *
      ((hζ.toInteger - 1) ^ (FermatLastTheoremForThreeGen.Solution.multiplicity✝ S - 1) *
          FermatLastTheoremForThreeGen.Solution.X✝ S) ^
        3
-- Mathlib.Analysis.SpecialFunctions.Log.ENNRealLog
/-- The logarithm function defined on the extended nonnegative reals `ℝ≥0∞`
to the extended reals `EReal`. Coincides with the usual logarithm function
and with `Real.log` on positive reals, and takes values `log 0 = ⊥` and `log ⊤ = ⊤`.
Conventions about multiplication in `ℝ≥0∞` and addition in `EReal` make the identity
`log (x * y) = log x + log y` unconditional.  -/
ENNReal.log : ENNReal → EReal
-- Mathlib.CategoryTheory.Bicategory.Functor.Oplax
CategoryTheory.OplaxFunctor.mapComp'_eq_mapComp : ∀ {B : Type u₁} [inst : CategoryTheory.Bicategory B] {C : Type u₂} [inst_1 : CategoryTheory.Bicategory C]
  (F : CategoryTheory.OplaxFunctor B C) {b₀ b₁ b₂ : B} (f : b₀ ⟶ b₁) (g : b₁ ⟶ b₂),
  F.mapComp' f g (CategoryTheory.CategoryStruct.comp f g) ⋯ = F.mapComp f g
-- Mathlib.Data.Set.Basic
Set.nonempty_of_mem : ∀ {α : Type u} {s : Set α} {x : α}, x ∈ s → s.Nonempty
-- Mathlib.Combinatorics.Matroid.Rank.ENat
Matroid.one_le_eRank : ∀ {α : Type u_1} (M : Matroid α) [M.RankPos], 1 ≤ M.eRank
-- Mathlib.LinearAlgebra.SymplecticGroup
/-- The determinant of a symplectic matrix is 1 if its upper-left block is invertible.  -/
_private.Mathlib.LinearAlgebra.SymplecticGroup.0.SymplecticGroup.det_one_if_fromBlocks_invertible : ∀ {l : Type u_1} {R : Type u_2} [inst : DecidableEq l] [inst_1 : Fintype l] [inst_2 : CommRing R]
  {A B C D : Matrix l l R} [Invertible A],
  Matrix.fromBlocks A B C D ∈ Matrix.symplecticGroup l R → (Matrix.fromBlocks A B C D).det = 1
-- Mathlib.Analysis.MellinTransform
mellin_comp_rpow : ∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℂ E] (f : ℝ → E) (s : ℂ) (a : ℝ),
  mellin (fun t => f (t ^ a)) s = |a|⁻¹ • mellin f (s / ↑a)
-- Mathlib.CategoryTheory.Limits.Preserves.Opposites
/-- If `F : C ⥤ Dᵒᵖ` reflects finite colimits, then `F.leftOp : Cᵒᵖ ⥤ D` reflects finite
limits.  -/
CategoryTheory.Limits.reflectsFiniteLimits_leftOp : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  (F : CategoryTheory.Functor C Dᵒᵖ) [CategoryTheory.Limits.ReflectsFiniteColimits F],
  CategoryTheory.Limits.ReflectsFiniteLimits F.leftOp
-- Mathlib.CategoryTheory.Types.Basic
CategoryTheory.FunctorToTypes.map_id_apply : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] (F : CategoryTheory.Functor C (Type w)) {X : C} (a : F.obj X),
  (CategoryTheory.ConcreteCategory.hom (F.map (CategoryTheory.CategoryStruct.id X))) a = a
-- Std.Data.String.ToNat
_private.Std.Data.String.ToNat.0.String.Slice.toNat?.eq_1 : ∀ (s : String.Slice),
  s.toNat? =
    if s.isNat = true then
      some (String.Slice.foldl (fun n c => if c = '_' then n else n * 10 + (c.toNat - '0'.toNat)) 0 s)
    else none
-- Mathlib.Geometry.Euclidean.Incenter
Affine.Simplex.excenterWeights.eq_1 : ∀ {V : Type u_1} {P : Type u_2} [inst : NormedAddCommGroup V] [inst_1 : InnerProductSpace ℝ V] [inst_2 : MetricSpace P]
  [inst_3 : NormedAddTorsor V P] {n : ℕ} [inst_4 : NeZero n] (s : Affine.Simplex ℝ P n) (signs : Finset (Fin (n + 1))),
  s.excenterWeights signs = (∑ i, s.excenterWeightsUnnorm signs i)⁻¹ • s.excenterWeightsUnnorm signs
-- Mathlib.MeasureTheory.Integral.Bochner.SumMeasure
MeasureTheory.Integrable.summable_of_dirac : ∀ {ι : Type u_1} {X : Type u_2} {E : Type u_3} {mX : MeasurableSpace X} [inst : NormedAddCommGroup E] {f : X → E}
  [MeasurableSingletonClass X] {x : ι → X} {c : ι → ENNReal},
  MeasureTheory.Integrable f (MeasureTheory.Measure.sum fun i => c i • MeasureTheory.Measure.dirac (x i)) →
    Summable fun i => (c i).toReal * ‖f (x i)‖
-- Std.Data.HashMap.Lemmas
Std.HashMap.Equiv.beq : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} {β : Type v} {m₁ m₂ : Std.HashMap α β} [inst : BEq β] [EquivBEq α]
  [LawfulHashable α] [ReflBEq β], m₁.Equiv m₂ → (m₁ == m₂) = true
-- Mathlib.AlgebraicTopology.SimplicialSet.StdSimplex
SSet.stdSimplex.instFiniteObjSimplexCategory : ∀ (n : SimplexCategory), (SSet.stdSimplex.obj n).Finite
-- Lean.Meta.Tactic.Split
Lean.Meta.Split.mkDiscrGenErrorMsg : Lean.Expr → Lean.MessageData
-- Init.Data.List.Scan.Lemmas
_private.Init.Data.List.Scan.Lemmas.0.List.scanAuxM.go.eq_2 : ∀ {m : Type u_1 → Type u_2} {β : Type u_1} {α : Type u_3} [inst : Monad m] (f : β → α → m β) (a : β) (a_1 : List β)
  (x_3 : α) (xs : List α),
  List.scanAuxM.go✝ f (x_3 :: xs) a a_1 = do
    let __do_lift ← f a x_3
    List.scanAuxM.go✝ f xs __do_lift (a :: a_1)
-- Mathlib.Dynamics.BirkhoffSum.Average
/-- If a function `g` is invariant under a function `f` (i.e., `g ∘ f = g`), then the Birkhoff
average of `g` over `f` for `n` iterations is equal to `g`. Requires that `0 < n`.  -/
birkhoffAverage_of_comp_eq : ∀ (R : Type u_1) {α : Type u_2} {M : Type u_3} [inst : DivisionSemiring R] [inst_1 : AddCommMonoid M]
  [inst_2 : Module R M] {f : α → α} {g : α → M}, g ∘ f = g → ∀ {n : ℕ}, ↑n ≠ 0 → birkhoffAverage R f g n = g
-- Lean.DocString.Extension
/-- Text to be inserted after the prior snippet's ending text.  -/
Lean.VersoModuleDocs.Snippet.text : Lean.VersoModuleDocs.Snippet → Array (Lean.Doc.Block Lean.ElabInline Lean.ElabBlock)
-- Mathlib.CategoryTheory.Monoidal.Cartesian.Comon_
CategoryTheory.ComonObj.mk.congr_simp : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.MonoidalCategory C] {X : C}
  (counit counit_1 : X ⟶ CategoryTheory.MonoidalCategoryStruct.tensorUnit C) (e_counit : counit = counit_1)
  (comul comul_1 : X ⟶ CategoryTheory.MonoidalCategoryStruct.tensorObj X X) (e_comul : comul = comul_1)
  (counit_comul :
    CategoryTheory.CategoryStruct.comp comul (CategoryTheory.MonoidalCategoryStruct.whiskerRight counit X) =
      (CategoryTheory.MonoidalCategoryStruct.leftUnitor X).inv)
  (comul_counit :
    CategoryTheory.CategoryStruct.comp comul (CategoryTheory.MonoidalCategoryStruct.whiskerLeft X counit) =
      (CategoryTheory.MonoidalCategoryStruct.rightUnitor X).inv)
  (comul_assoc :
    CategoryTheory.CategoryStruct.comp comul (CategoryTheory.MonoidalCategoryStruct.whiskerLeft X comul) =
      CategoryTheory.CategoryStruct.comp comul
        (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerRight comul X)
          (CategoryTheory.MonoidalCategoryStruct.associator X X X).hom)),
  { counit := counit, comul := comul, counit_comul := counit_comul, comul_counit := comul_counit,
      comul_assoc := comul_assoc } =
    { counit := counit_1, comul := comul_1, counit_comul := ⋯, comul_counit := ⋯, comul_assoc := ⋯ }
-- Mathlib.RingTheory.UniqueFactorizationDomain.Basic
UniqueFactorizationMonoid.factors_eq_zero : ∀ {α : Type u_1} [inst : CommMonoidWithZero α] [inst_1 : UniqueFactorizationMonoid α] {x : α},
  x ≠ 0 → (UniqueFactorizationMonoid.factors x = 0 ↔ IsUnit x)
-- Lean.Meta.Eqns
_private.Lean.Meta.Eqns.0.Lean.Meta.mkSimpleEqThm.doRealize : Lean.Name → Lean.DefinitionVal → Lean.MetaM Unit
-- Mathlib.Combinatorics.SimpleGraph.Diam
SimpleGraph.eccent_def : ∀ {α : Type u_1} {G : SimpleGraph α}, G.eccent = fun u => ⨆ v, G.edist u v
-- Init.Data.BitVec.Bitblast
/-- Bitwise addition implemented via a ripple carry adder.  -/
BitVec.adc : {w : ℕ} → BitVec w → BitVec w → Bool → Bool × BitVec w
-- Init.Data.List.Pairwise
List.pairwise_pmap : ∀ {β : Type u_1} {α : Type u_2} {R : α → α → Prop} {p : β → Prop} {f : (b : β) → p b → α} {l : List β}
  (h : ∀ x ∈ l, p x),
  List.Pairwise R (List.pmap f l h) ↔ List.Pairwise (fun b₁ b₂ => ∀ (h₁ : p b₁) (h₂ : p b₂), R (f b₁ h₁) (f b₂ h₂)) l
-- Mathlib.AlgebraicGeometry.Morphisms.Basic
AlgebraicGeometry.HasAffineProperty.iff_of_isAffine : ∀ {P : CategoryTheory.MorphismProperty AlgebraicGeometry.Scheme} {Q : AlgebraicGeometry.AffineTargetMorphismProperty}
  [AlgebraicGeometry.HasAffineProperty P Q] {X Y : AlgebraicGeometry.Scheme} {f : X ⟶ Y}
  [inst : AlgebraicGeometry.IsAffine Y], P f ↔ Q f
-- Std.Data.DTreeMap.Lemmas
Std.DTreeMap.Const.forMUncurried_eq_forM_toArray : ∀ {α : Type u} {cmp : α → α → Ordering} {m : Type w → Type w'} {β : Type v} {t : Std.DTreeMap α (fun x => β) cmp}
  [inst : Monad m] [LawfulMonad m] {f : α × β → m PUnit.{w + 1}},
  Std.DTreeMap.Const.forMUncurried f t = Array.forM f (Std.DTreeMap.Const.toArray t)
-- Mathlib.Order.UpperLower.Principal
LowerSet.Iic_inj : ∀ {α : Type u_1} [inst : PartialOrder α] {a b : α}, LowerSet.Iic a = LowerSet.Iic b ↔ a = b
-- Lean.Elab.Tactic.Induction
_private.Lean.Elab.Tactic.Induction.0.Lean.Elab.Tactic.getAltLhses : Lean.Syntax → Lean.Syntax
-- Mathlib.CategoryTheory.Limits.HasLimits
CategoryTheory.Limits.HasLimitsOfSize.mk : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C],
  autoParam (∀ (J : Type u₁) [inst_1 : CategoryTheory.Category.{v₁, u₁} J], CategoryTheory.Limits.HasLimitsOfShape J C)
      CategoryTheory.Limits.HasLimitsOfSize.has_limits_of_shape._autoParam →
    CategoryTheory.Limits.HasLimitsOfSize.{v₁, u₁, v, u} C
-- Mathlib.Algebra.Order.Monoid.Unbundled.Basic
Right.one_lt_mul_of_right : ∀ {α : Type u_1} [inst : MulOneClass α] [inst_1 : Preorder α] [IsBotOneClass α] [MulRightMono α] {b : α},
  1 < b → ∀ (a : α), 1 < a * b
-- Mathlib.Algebra.Module.ZLattice.Basic
ZSpan.fundamentalDomain_subset_parallelepiped : ∀ {E : Type u_1} {ι : Type u_2} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] (b : Module.Basis ι ℝ E)
  [inst_2 : Fintype ι], ZSpan.fundamentalDomain b ⊆ parallelepiped ⇑b
-- Mathlib.Algebra.ContinuedFractions.Computation.TerminatesIffRat
/-- Every finite convergent corresponds to a rational number.  -/
GenContFract.exists_rat_eq_nth_conv : ∀ {K : Type u_1} [inst : Field K] [inst_1 : LinearOrder K] [inst_2 : FloorRing K] (v : K) (n : ℕ),
  ∃ q, (GenContFract.of v).convs n = ↑q
-- Mathlib.LinearAlgebra.DFinsupp
DFinsupp.lsum_apply_apply : ∀ {ι : Type u_1} {R : Type u_3} (S : Type u_4) {M : ι → Type u_5} {N : Type u_6} [inst : Semiring R]
  [inst_1 : (i : ι) → AddCommMonoid (M i)] [inst_2 : (i : ι) → Module R (M i)] [inst_3 : AddCommMonoid N]
  [inst_4 : Module R N] [inst_5 : DecidableEq ι] [inst_6 : Semiring S] [inst_7 : Module S N]
  [inst_8 : SMulCommClass R S N] (F : (i : ι) → M i →ₗ[R] N) (a : Π₀ (i : ι), M i),
  ((DFinsupp.lsum S) F) a = (DFinsupp.sumAddHom fun i => (F i).toAddMonoidHom) a
-- Mathlib.Topology.Constructions
instDiscreteTopologyULift : ∀ {X : Type u} [inst : TopologicalSpace X] [DiscreteTopology X], DiscreteTopology (ULift.{u_5, u} X)
-- Std.Data.Iterators.Lemmas.Combinators.Zip
_private.Std.Data.Iterators.Lemmas.Combinators.Zip.0.Std.Iter.atIdxSlow?_eq_match.match_1.splitter : (motive : ℕ → Sort u_1) → (n : ℕ) → (Unit → motive 0) → ((n : ℕ) → motive n.succ) → motive n
-- Mathlib.Algebra.GroupWithZero.Units.Basic
eq_div_iff_mul_eq : ∀ {G₀ : Type u_3} [inst : GroupWithZero G₀] {a b c : G₀}, c ≠ 0 → (a = b / c ↔ a * c = b)
-- Mathlib.Algebra.Category.Grp.EpiMono
GrpCat.SurjectiveOfEpiAuxs.τ_apply_fromCoset' : ∀ {A B : GrpCat} (f : A ⟶ B),
  ∀ x ∈ (GrpCat.Hom.hom f).range,
    (GrpCat.SurjectiveOfEpiAuxs.tau f)
        (GrpCat.SurjectiveOfEpiAuxs.XWithInfinity.fromCoset ⟨x • ↑(GrpCat.Hom.hom f).range, ⋯⟩) =
      GrpCat.SurjectiveOfEpiAuxs.XWithInfinity.infinity
-- Mathlib.MeasureTheory.Measure.Stieltjes
StieltjesFunction.measure_univ_of_tendsto_atTop_atTop : ∀ {R : Type u_1} [inst : LinearOrder R] [inst_1 : TopologicalSpace R] (f : StieltjesFunction R)
  [inst_2 : OrderTopology R] [inst_3 : CompactIccSpace R] [inst_4 : MeasurableSpace R] [inst_5 : BorelSpace R]
  [inst_6 : SecondCountableTopology R] [inst_7 : DenselyOrdered R] [Nonempty R],
  Filter.Tendsto (↑f) Filter.atTop Filter.atTop → f.measure Set.univ = ⊤
-- Mathlib.Order.Filter.Map
Filter.mem_map_iff_exists_image : ∀ {α : Type u_1} {β : Type u_2} {f : Filter α} {m : α → β} {t : Set β}, t ∈ Filter.map m f ↔ ∃ s ∈ f, m '' s ⊆ t
-- Mathlib.Data.Sigma.Lex
Sigma.instTotalLexOfTrichotomous : ∀ {ι : Type u_1} {α : ι → Type u_2} {r : ι → ι → Prop} {s : (i : ι) → α i → α i → Prop} [Std.Trichotomous r]
  [∀ (i : ι), Std.Total (s i)], Std.Total (Sigma.Lex r s)
-- Mathlib.Topology.UniformSpace.CompleteSeparated
/-- In a separated space, a complete set is closed.  -/
IsComplete.isClosed : ∀ {α : Type u_1} [inst : UniformSpace α] [T0Space α] {s : Set α}, IsComplete s → IsClosed s
-- Mathlib.CategoryTheory.Limits.Preserves.Shapes.BinaryProducts
/-- The property of preserving coproducts expressed in terms of binary cofans.  -/
CategoryTheory.Limits.mapIsColimitOfPreservesOfIsColimit : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    {D : Type u₂} →
      [inst_1 : CategoryTheory.Category.{v₂, u₂} D] →
        (G : CategoryTheory.Functor C D) →
          {P X Y : C} →
            (f : X ⟶ P) →
              (g : Y ⟶ P) →
                [CategoryTheory.Limits.PreservesColimit (CategoryTheory.Limits.pair X Y) G] →
                  CategoryTheory.Limits.IsColimit (CategoryTheory.Limits.BinaryCofan.mk f g) →
                    CategoryTheory.Limits.IsColimit (CategoryTheory.Limits.BinaryCofan.mk (G.map f) (G.map g))
-- Mathlib.RingTheory.Ideal.Maps
RingHom.eq_liftOfSurjective : ∀ {A : Type u_1} {B : Type u_2} {C : Type u_3} [inst : Ring A] [inst_1 : Ring B] [inst_2 : Ring C] (f : A →+* B)
  (hf : Function.Surjective ⇑f) (g : A →+* C) (hg : RingHom.ker f ≤ RingHom.ker g) (h : B →+* C),
  h.comp f = g → h = (f.liftOfSurjective hf) ⟨g, hg⟩
-- Mathlib.CategoryTheory.Bicategory.Yoneda
/-- Left unitor as a 2-isomorphism in `Cat`.  -/
CategoryTheory.Bicategory.leftUnitorNatIsoCat : {B : Type u} →
  [inst : CategoryTheory.Bicategory B] →
    (a b : B) →
      (CategoryTheory.Bicategory.precomposingCat a a b).obj (CategoryTheory.CategoryStruct.id a) ≅
        CategoryTheory.CategoryStruct.id (CategoryTheory.Cat.of (a ⟶ b))
-- Std.Data.DHashMap.Lemmas
Std.DHashMap.Const.get_inter : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} {β : Type v} {m₁ m₂ : Std.DHashMap α fun x => β} [inst : EquivBEq α]
  [inst_1 : LawfulHashable α] {k : α} {h_mem : k ∈ m₁ ∩ m₂},
  Std.DHashMap.Const.get (m₁.inter m₂) k h_mem = Std.DHashMap.Const.get m₁ k ⋯
-- Mathlib.Analysis.SpecialFunctions.Trigonometric.Angle
Real.Angle.toReal_coe_eq_self_iff : ∀ {θ : ℝ}, (↑θ).toReal = θ ↔ -Real.pi < θ ∧ θ ≤ Real.pi
-- Mathlib.Topology.Algebra.OpenSubgroup
OpenNormalAddSubgroup.toAddSubgroup_injective : ∀ {G : Type u} [inst : AddGroup G] [inst_1 : TopologicalSpace G], Function.Injective fun H => ↑H.toOpenAddSubgroup
-- Lean.Level
Lean.Level.hashEx : Lean.Level → UInt32
-- Std.Data.TreeMap.Lemmas
Std.TreeMap.contains_maxKey? : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Std.TreeMap α β cmp} [Std.TransCmp cmp] {km : α},
  t.maxKey? = some km → t.contains km = true
-- Mathlib.LinearAlgebra.Quotient.Basic
/-- The correspondence theorem for modules: there is an order isomorphism between submodules of the
quotient of `M` by `p`, and submodules of `M` larger than `p`.  -/
Submodule.comapMkQRelIso : {R : Type u_1} →
  {M : Type u_2} →
    [inst : Ring R] →
      [inst_1 : AddCommGroup M] → [inst_2 : Module R M] → (p : Submodule R M) → Submodule R (M ⧸ p) ≃o ↑(Set.Ici p)
-- Mathlib.RingTheory.Ideal.Quotient.Operations
Ideal.quotientInfEquivQuotientProd_snd : ∀ {R : Type u_2} [inst : CommRing R] (I J : Ideal R) (coprime : IsCoprime I J) (x : R ⧸ I ⊓ J),
  ((I.quotientInfEquivQuotientProd J coprime) x).2 = (Ideal.Quotient.factor ⋯) x
-- Mathlib.GroupTheory.OrderOfElement
addOrderOf_dvd_card : ∀ {G : Type u_1} [inst : AddGroup G] [inst_1 : Fintype G] {x : G}, addOrderOf x ∣ Fintype.card G
-- Mathlib.Logic.Relation
Quot.eqvGen_exact : ∀ {α : Type u_1} {r : α → α → Prop} {a b : α}, Quot.mk r a = Quot.mk r b → Relation.EqvGen r a b
-- Mathlib.Topology.Algebra.InfiniteSum.NatInt
HasSum.of_nat_of_neg : ∀ {G : Type u_2} [inst : AddCommGroup G] {g g' : G} [inst_1 : TopologicalSpace G] [IsTopologicalAddGroup G] {f : ℤ → G},
  HasSum (fun n => f ↑n) g → HasSum (fun n => f (-↑n)) g' → HasSum f (g + g' - f 0)
-- Mathlib.GroupTheory.Exponent
add_comm_of_exponent_two : ∀ {G : Type u} [inst : AddMonoid G] [IsCancelAdd G], AddMonoid.exponent G = 2 → ∀ (a b : G), a + b = b + a
-- Mathlib.Combinatorics.Graph.Subgraph
Graph.IsClosedSubgraph.mem_iff_of_isLink : ∀ {α : Type u_1} {β : Type u_2} {x y : α} {e : β} {G H : Graph α β},
  G.IsLink e x y → H.IsClosedSubgraph G → (x ∈ H.vertexSet ↔ y ∈ H.vertexSet)
-- Mathlib.Algebra.Star.Unitary
Unitary.map_mem : ∀ {R : Type u_2} {S : Type u_3} [inst : Monoid R] [inst_1 : StarMul R] [inst_2 : Monoid S] [inst_3 : StarMul S]
  {F : Type u_5} [inst_4 : FunLike F R S] [StarHomClass F R S] [MonoidHomClass F R S] (f : F) {r : R},
  r ∈ unitary R → f r ∈ unitary S
-- Std.Data.HashSet.Lemmas
Std.HashSet.contains_of_contains_insert : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} {m : Std.HashSet α} [EquivBEq α] [LawfulHashable α] {k a : α},
  (m.insert k).contains a = true → (k == a) = false → m.contains a = true
-- Init.Data.String.Defs
String.Pos.Raw.isValid_rawEndPos : ∀ {s : String}, String.Pos.Raw.IsValid s s.rawEndPos
-- Mathlib.Topology.Sets.Compacts
TopologicalSpace.Compacts.instDistribLatticeOfT2Space : {α : Type u_1} → [inst : TopologicalSpace α] → [T2Space α] → DistribLattice (TopologicalSpace.Compacts α)
-- Mathlib.Logic.Equiv.Fin.Rotate
finRotate_last' : ∀ {n : ℕ}, (finRotate (n + 1)) ⟨n, ⋯⟩ = ⟨0, ⋯⟩
-- Mathlib.AlgebraicGeometry.EllipticCurve.NormalForms
WeierstrassCurve.b₄_of_isShortNF : ∀ {R : Type u_1} [inst : CommRing R] (W : WeierstrassCurve R) [W.IsShortNF], W.b₄ = 2 * W.a₄
-- Init.Data.List.Perm
List.Perm.congr_right : ∀ {α : Type u_1} {l₁ l₂ : List α}, l₁.Perm l₂ → ∀ (l₃ : List α), l₃.Perm l₁ ↔ l₃.Perm l₂
-- Mathlib.Data.Set.Restrict
Set.image_restrictPreimage : ∀ {α : Type u_1} {β : Type u_2} (s : Set α) (t : Set β) (f : α → β),
  t.restrictPreimage f '' Subtype.val ⁻¹' s = Subtype.val ⁻¹' f '' s
-- Mathlib.MeasureTheory.Measure.Typeclasses.SFinite
MeasureTheory.sfiniteSeq_le : ∀ {α : Type u_1} {m0 : MeasurableSpace α} (μ : MeasureTheory.Measure α) [inst : MeasureTheory.SFinite μ] (n : ℕ),
  MeasureTheory.sfiniteSeq μ n ≤ μ
-- Mathlib.Algebra.Order.IsBotOne
not_lt_one : ∀ {α : Type u_1} {a : α} [inst : Preorder α] [inst_1 : One α] [IsBotOneClass α], ¬a < 1
-- Mathlib.Data.Finset.Preimage
Finset.mem_preimage : ∀ {α : Type u} {β : Type v} {f : α → β} {s : Finset β} {hf : Set.InjOn f (f ⁻¹' ↑s)} {x : α},
  x ∈ s.preimage f hf ↔ f x ∈ s
-- Mathlib.Algebra.Module.Equiv.Basic
LinearEquiv.coe_neg : ∀ {R : Type u_1} {M : Type u_5} [inst : Semiring R] [inst_1 : AddCommGroup M] [inst_2 : Module R M],
  ⇑(LinearEquiv.neg R) = -id
-- Mathlib.Order.Filter.AtTopBot.Defs
Antitone.piecewise_eventually_eq_iInter : ∀ {ι : Type u_1} {α : Type u_3} {β : α → Type u_6} [inst : Preorder ι] {s : ι → Set α}
  [inst_1 : (i : ι) → DecidablePred fun x => x ∈ s i] [inst_2 : DecidablePred fun x => x ∈ ⋂ i, s i],
  Antitone s →
    ∀ (f g : (a : α) → β a) (a : α), ∀ᶠ (i : ι) in Filter.atTop, (s i).piecewise f g a = (⋂ i, s i).piecewise f g a
-- Init.Grind.Ring.CommSolver
Lean.Grind.CommRing.Poly.mulC_nc : Lean.Grind.CommRing.Poly → Lean.Grind.CommRing.Poly → ℕ → Lean.Grind.CommRing.Poly
-- Batteries.Data.UInt
instLawfulOrdUInt32 : Std.LawfulOrd UInt32
-- Std.Tactic.BVDecide.Bitblast.BVExpr.Basic
Std.Tactic.BVDecide.BVBinOp.toString : Std.Tactic.BVDecide.BVBinOp → String
-- Mathlib.Data.Fin.Fin2
Fin2.IsLT.succ : ∀ (m n : ℕ) [l : Fin2.IsLT m n], Fin2.IsLT m.succ n.succ
-- Mathlib.Logic.Pairwise
/-- **Alias** of `Std.Refl.set_pairwise_iff`. -/
Reflexive.set_pairwise_iff : ∀ {α : Type u_1} {r : α → α → Prop} {s : Set α} [Std.Refl r], s.Pairwise r ↔ ∀ ⦃a : α⦄, a ∈ s → ∀ ⦃b : α⦄, b ∈ s → r a b