mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.CategoryTheory.Core
CategoryTheory.Equivalence.core_counitIso_inv_app_iso_inv : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  (E : C ≌ D) (X : CategoryTheory.Core D), (E.core.counitIso.inv.app X).iso.inv = E.counitIso.hom.app X.of
-- Mathlib.GroupTheory.SpecificGroups.Dihedral
DihedralGroup.one_def : ∀ {n : ℕ}, 1 = DihedralGroup.r 0
-- Mathlib.Geometry.Euclidean.Angle.Unoriented.Affine
/-- If ∠ABC = π then dist C B ≠ 0.  -/
EuclideanGeometry.right_dist_ne_zero_of_angle_eq_pi : ∀ {V : Type u_1} {P : Type u_2} [inst : NormedAddCommGroup V] [inst_1 : InnerProductSpace ℝ V] [inst_2 : MetricSpace P]
  [inst_3 : NormedAddTorsor V P] {p₁ p₂ p₃ : P}, EuclideanGeometry.angle p₁ p₂ p₃ = Real.pi → dist p₃ p₂ ≠ 0
-- Mathlib.CategoryTheory.Presentable.Finite
CategoryTheory.IsFinitelyPresentable.exists_hom_of_isColimit : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {J : Type w} [inst_1 : CategoryTheory.SmallCategory J]
  [CategoryTheory.IsFiltered J] {D : CategoryTheory.Functor J C} {c : CategoryTheory.Limits.Cocone D}
  (hc : CategoryTheory.Limits.IsColimit c) {X : C} [CategoryTheory.IsFinitelyPresentable X] (f : X ⟶ c.pt),
  ∃ j p, CategoryTheory.CategoryStruct.comp p (c.ι.app j) = f
-- Mathlib.Algebra.Ring.Prod
/-- `Prod.map` as a `NonUnitalRingHom`.  -/
NonUnitalRingHom.prodMap : {R : Type u_1} →
  {R' : Type u_2} →
    {S : Type u_3} →
      {S' : Type u_4} →
        [inst : NonUnitalNonAssocSemiring R] →
          [inst_1 : NonUnitalNonAssocSemiring S] →
            [inst_2 : NonUnitalNonAssocSemiring R'] →
              [inst_3 : NonUnitalNonAssocSemiring S'] → (R →ₙ+* R') → (S →ₙ+* S') → R × S →ₙ+* R' × S'
-- Mathlib.Algebra.Homology.ShortComplex.LeftHomology
/-- The inclusion `S.cycles ⟶ S.X₂`.  -/
CategoryTheory.ShortComplex.iCycles : {C : Type u_1} →
  [inst : CategoryTheory.Category.{v_1, u_1} C] →
    [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C] →
      (S : CategoryTheory.ShortComplex C) → [inst_2 : S.HasLeftHomology] → S.cycles ⟶ S.X₂
-- Mathlib.RepresentationTheory.Homological.GroupHomology.Functoriality
groupHomology.cyclesIso₀_inv_comp_cyclesMap_assoc : ∀ {k G H : Type u} [inst : CommRing k] [inst_1 : Group G] [inst_2 : Group H] {A : Rep.{u, u, u} k G}
  {B : Rep.{u, u, u} k H} (f : G →* H) (φ : A ⟶ Rep.res f B) {Z : ModuleCat k} (h : groupHomology.cycles B 0 ⟶ Z),
  CategoryTheory.CategoryStruct.comp (groupHomology.cyclesIso₀ A).inv
      (CategoryTheory.CategoryStruct.comp (groupHomology.cyclesMap f φ 0) h) =
    CategoryTheory.CategoryStruct.comp (Rep.Hom.toModuleCatHom φ)
      (CategoryTheory.CategoryStruct.comp (groupHomology.cyclesIso₀ B).inv h)
-- Mathlib.CategoryTheory.Limits.Shapes.Biproducts
CategoryTheory.Limits.biproduct.whiskerEquiv_hom_eq_lift : ∀ {J : Type w} {K : Type u_1} {C : Type u} [inst : CategoryTheory.Category.{v, u} C]
  [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C] {f : J → C} {g : K → C} (e : J ≃ K) (w : (j : J) → g (e j) ≅ f j)
  [inst_2 : CategoryTheory.Limits.HasBiproduct f] [inst_3 : CategoryTheory.Limits.HasBiproduct g],
  (CategoryTheory.Limits.biproduct.whiskerEquiv e w).hom =
    CategoryTheory.Limits.biproduct.lift fun k =>
      CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.biproduct.π f (e.symm k))
        (CategoryTheory.CategoryStruct.comp (w (e.symm k)).inv (CategoryTheory.eqToHom ⋯))
-- Mathlib.RingTheory.LocalProperties.Basic
Ideal.localized₀_eq_restrictScalars_map : ∀ {R : Type u_1} (S : Type u_2) [inst : CommSemiring R] [inst_1 : CommSemiring S] [inst_2 : Algebra R S]
  (p : Submonoid R) [inst_3 : IsLocalization p S] (I : Ideal R),
  Submodule.localized₀ p (Algebra.linearMap R S) I = Submodule.restrictScalars R (Ideal.map (algebraMap R S) I)
-- Mathlib.Order.BooleanAlgebra.Set
Set.sdiff_inter_sdiff : ∀ {α : Type u_1} {s t u : Set α}, s \ t ∩ (s \ u) = s \ (t ∪ u)
-- Aesop.Tracing
Aesop.resolveTraceOption : Lean.Ident → Lean.MacroM Lean.Name
-- Mathlib.Algebra.Star.CHSH
IsCHSHTuple.A₁_inv : ∀ {R : Type u_1} [inst : Monoid R] [inst_1 : StarMul R] {A₀ A₁ B₀ B₁ : R}, IsCHSHTuple A₀ A₁ B₀ B₁ → A₁ ^ 2 = 1
-- Mathlib.Geometry.Euclidean.Circumcenter
Affine.Simplex.dist_circumcenter_sq_eq_sq_sub_circumradius : ∀ {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 : ℕ} {r : ℝ} (s : Affine.Simplex ℝ P n) {p₁ : P},
  (∀ (i : Fin (n + 1)), dist (s.points i) p₁ = r) →
    ↑(s.orthogonalProjectionSpan p₁) = s.circumcenter →
      s.points 0 ∈ affineSpan ℝ (Set.range s.points) →
        dist p₁ s.circumcenter * dist p₁ s.circumcenter = r * r - s.circumradius * s.circumradius
-- Mathlib.FieldTheory.SeparableClosure
/-- The finite inseparable degree for a general field extension `E / F` is defined
to be the degree of `E / separableClosure F E` as a natural number. It is defined to be zero
if such field extension is infinite.  -/
Field.finInsepDegree : (F : Type u) → (E : Type v) → [inst : Field F] → [inst_1 : Field E] → [Algebra F E] → ℕ
-- Mathlib.Algebra.Group.Units.Defs
divp_eq_div : ∀ {α : Type u} [inst : DivisionMonoid α] (a : α) (u : αˣ), a /ₚ u = a / ↑u
-- Mathlib.Algebra.Category.MonCat.Basic
/-- Typecheck an `AddMonoidHom` as a morphism in `AddMonCat`.  -/
AddMonCat.ofHom : {X Y : Type u} → [inst : AddMonoid X] → [inst_1 : AddMonoid Y] → (X →+ Y) → (AddMonCat.of X ⟶ AddMonCat.of Y)
-- Mathlib.CategoryTheory.Limits.Shapes.Biproducts
CategoryTheory.Limits.Bicone.instIsSplitMonoι : ∀ {J : Type w} {C : Type uC} [inst : CategoryTheory.Category.{uC', uC} C]
  [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C] {F : J → C} (B : CategoryTheory.Limits.Bicone F) (j : J),
  CategoryTheory.IsSplitMono (B.ι j)
-- Aesop.Rule.Name
_private.Aesop.Rule.Name.0.Aesop.RuleName.instToJsonJson.toJson : Aesop.RuleName.Json✝ → Lean.Json
-- Mathlib.Analysis.Convex.Visible
/-- A set whose convex hull is closed lies in the cone based at a point `x` generated by its points
visible from `x` through its convex hull.  -/
IsClosed.convexHull_subset_affineSpan_isVisible : ∀ {V : Type u_2} [inst : AddCommGroup V] [inst_1 : Module ℝ V] {s : Set V} {x : V} [inst_2 : TopologicalSpace V]
  [IsTopologicalAddGroup V] [ContinuousSMul ℝ V],
  IsClosed ((convexHull ℝ) s) →
    x ∉ (convexHull ℝ) s → (convexHull ℝ) s ⊆ ↑(affineSpan ℝ ({x} ∪ {y | y ∈ s ∧ IsVisible ℝ ((convexHull ℝ) s) x y}))
-- Mathlib.Geometry.Euclidean.Volume.Measure
/-- The scalar that defines `μHE[d]` is non-zero.  -/
MeasureTheory.Measure.addHaarScalarFactor_volume_hausdorffMeasure_ne_zero : ∀ (d : ℕ), MeasureTheory.volume.addHaarScalarFactor (MeasureTheory.Measure.hausdorffMeasure ↑d) ≠ 0
-- Mathlib.Order.Minimal
/-- **Alias** of the forward direction of `minimal_toDual`. -/
Minimal.of_dual : ∀ {α : Type u_2} {P : α → Prop} {x : α} [inst : LE α],
  Minimal (fun x => P (OrderDual.ofDual x)) (OrderDual.toDual x) → Maximal P x
-- Std.Time.Time.Unit.Nanosecond
Std.Time.Nanosecond.instDecidableLeSpan : {x y : Std.Time.Nanosecond.Span} → Decidable (x ≤ y)
-- Mathlib.Algebra.Order.Monoid.Unbundled.MinMax
fn_min_add_fn_max : ∀ {α : Type u_1} {β : Type u_2} [inst : LinearOrder α] [inst_1 : AddCommSemigroup β] (f : α → β) (a b : α),
  f (min a b) + f (max a b) = f a + f b
-- Mathlib.CategoryTheory.Limits.Shapes.Products
/-- The natural transformation induced by `Sigma.ι`.  -/
CategoryTheory.Limits.Sigma.functorι : {α : Type w₂} →
  {C : Type u} →
    [inst : CategoryTheory.Category.{v, u} C] →
      [inst_1 : CategoryTheory.Limits.HasCoproductsOfShape α C] →
        (a : α) → CategoryTheory.Pi.eval (fun x => C) a ⟶ CategoryTheory.Limits.Sigma.functor α
-- Mathlib.Combinatorics.SimpleGraph.Extremal.Turan
SimpleGraph.turanGraph_cliqueFree : ∀ {n r : ℕ}, 0 < r → (SimpleGraph.turanGraph n r).CliqueFree (r + 1)
-- Init.Classical
Classical.imp_iff_right_iff : ∀ {a b : Prop}, (a → b ↔ b) ↔ a ∨ b
-- Std.Data.HashMap.Lemmas
Std.HashMap.contains_map : ∀ {α : Type u} {β : Type v} {γ : Type w} {x : BEq α} {x_1 : Hashable α} {m : Std.HashMap α β} [EquivBEq α]
  [LawfulHashable α] {f : α → β → γ} {k : α}, (Std.HashMap.map f m).contains k = m.contains k
-- Mathlib.Geometry.Euclidean.Projection
/-- A point in the subspace is equidistant from another point and its
reflection.  -/
EuclideanGeometry.dist_reflection_eq_of_mem : ∀ {𝕜 : 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},
  p₁ ∈ s → ∀ (p₂ : P), dist p₁ ((EuclideanGeometry.reflection s) p₂) = dist p₁ p₂
-- Mathlib.Algebra.MonoidAlgebra.ToDirectSum
addMonoidAlgebraRingEquivDirectSum_symm_apply : ∀ {ι : Type u_1} {M : Type u_3} [inst : DecidableEq ι] [inst_1 : AddMonoid ι] [inst_2 : Semiring M]
  [inst_3 : (m : M) → Decidable (m ≠ 0)], ⇑addMonoidAlgebraRingEquivDirectSum.symm = DirectSum.toAddMonoidAlgebra
-- Mathlib.Combinatorics.Matroid.Basic
Matroid.indep_of_not_dep : ∀ {α : Type u_1} {M : Matroid α} {I : Set α},
  ¬M.Dep I → autoParam (I ⊆ M.E) Matroid.indep_of_not_dep._auto_1 → M.Indep I
-- Mathlib.Tactic.Ring.Basic
Mathlib.Tactic.Ring.cast_nnrat : ∀ {n d : ℕ} {R : Type u_2} [inst : DivisionSemiring R] {a : R},
  Mathlib.Meta.NormNum.IsNNRat a n d → a = NNRat.rawCast n d + 0
-- Mathlib.Topology.Sheaves.Presheaf
TopCat.Presheaf.pushforward_eq' : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {X Y : TopCat} {f g : X ⟶ Y},
  f = g → ∀ (ℱ : TopCat.Presheaf C X), (TopCat.Presheaf.pushforward C f).obj ℱ = (TopCat.Presheaf.pushforward C g).obj ℱ
-- Mathlib.Lean.Expr.ReplaceRec
/-- A version of `Expr.replace` where the replacement function is available to the function `f?`.

`replaceRec f? e` will call `f? r e` where `r = replaceRec f?`.
If `f? r e = none` then `r` will be called on each immediate subexpression of `e` and reassembled.
If it is `some x`, traversal terminates and `x` is returned.
If you wish to recursively replace things in the implementation of `f?`, you can apply `r`.

The function is also memoised, which means that if the
same expression (by reference) is encountered the cached replacement is used.  -/
Lean.Expr.replaceRec : ((Lean.Expr → Lean.Expr) → Lean.Expr → Option Lean.Expr) → Lean.Expr → Lean.Expr
-- Mathlib.Data.Finsupp.WellFounded
Finsupp.Colex.wellFoundedLT : ∀ {α : Type u_3} {N : Type u_4} [inst : LT α] [Std.Trichotomous fun x1 x2 => x1 < x2] [WellFoundedLT α]
  [inst_3 : AddMonoid N] [inst_4 : PartialOrder N] [IsBotZeroClass N] [WellFoundedLT N], WellFoundedLT (Colex (α →₀ N))
-- Mathlib.Algebra.Module.Presentation.Basic
/-- Given `relations : Relations A` and an `A`-module `M`, this is a constructor
for `relations.Solution M` for which the data is given as
a linear map `π : (relations.G →₀ A) →ₗ[A] M`. (See also `ofπ'` for an alternate
vanishing criterion.)  -/
Module.Relations.Solution.ofπ : {A : Type u} →
  [inst : Ring A] →
    {relations : Module.Relations A} →
      {M : Type v} →
        [inst_1 : AddCommGroup M] →
          [inst_2 : Module A M] →
            (π : (relations.G →₀ A) →ₗ[A] M) →
              (∀ (r : relations.R), π (relations.relation r) = 0) → relations.Solution M
-- Lean.Language.Lean.Types
/-- Resulting syntax tree.  -/
Lean.Language.Lean.HeaderParsedSnapshot.stx : Lean.Language.Lean.HeaderParsedSnapshot → Lean.Syntax
-- Mathlib.CategoryTheory.MorphismProperty.Local
CategoryTheory.MorphismProperty.IsLocalAtTarget.toRespects : ∀ {C : Type u} {inst : CategoryTheory.Category.{v, u} C} {P : CategoryTheory.MorphismProperty C}
  (K : CategoryTheory.Precoverage C) [self : P.IsLocalAtTarget K],
  P.Respects (CategoryTheory.MorphismProperty.isomorphisms C)
-- Std.Data.DTreeMap.Internal.Zipper
Std.DTreeMap.Internal.Unit.RoiSliceData.range : {α : Type u} → [inst : Ord α] → Std.DTreeMap.Internal.Unit.RoiSliceData α → Std.Roi α
-- Mathlib.Tactic.ClickSuggestions.FindPremises
/-- Compute the discrimination trees for the local variables in `lctx`.
We restrict to the variables in `lctx` to avoid using introduced bound variables.  -/
Mathlib.Tactic.ClickSuggestions.computeLCtxDiscrTrees : Mathlib.Tactic.ClickSuggestions.Choice →
  Lean.LocalContext → Option Lean.FVarId → Lean.MetaM Mathlib.Tactic.ClickSuggestions.PreDiscrTrees
-- Mathlib.Topology.Category.Profinite.Product
Profinite.IndexFunctor.surjective_π_app : ∀ {ι : Type u} {X : ι → Type} [inst : (i : ι) → TopologicalSpace (X i)] (C : Set ((i : ι) → X i)) {J : ι → Prop},
  Function.Surjective ⇑(Profinite.IndexFunctor.π_app C J)
-- Mathlib.Algebra.Module.Presentation.Tautological
/-- The system of equations corresponding to the tautological presentation of an `A`-module.  -/
Module.Presentation.tautologicalRelations : (A : Type u) → [inst : Ring A] → (M : Type v) → [inst_1 : AddCommGroup M] → [Module A M] → Module.Relations A
-- Std.Tactic.BVDecide.Bitblast.BVExpr.Circuit.Lemmas.Operations.Udiv
Std.Tactic.BVDecide.BVExpr.bitblast.blastUdiv.go_denote_mem_prefix : ∀ {α : Type} [inst : Hashable α] [inst_1 : DecidableEq α] {w : ℕ} {assign : α → Bool} {inv : Bool} (aig : Std.Sat.AIG α)
  (curr : ℕ) (n d q r : aig.RefVec w) (wn wr start : ℕ) (hstart : start < aig.decls.size),
  ⟦assign,
      { aig := (Std.Tactic.BVDecide.BVExpr.bitblast.blastUdiv.go aig curr n d wn wr q r).aig,
        ref := { gate := start, invert := inv, hgate := ⋯ } }⟧ =
    ⟦assign, { aig := aig, ref := { gate := start, invert := inv, hgate := hstart } }⟧
-- Init.Core
instInhabitedNonScalar : Inhabited NonScalar
-- Mathlib.Algebra.Group.Opposite
MulOpposite.instDivisionMonoid.eq_1 : ∀ {α : Type u_1} [inst : DivisionMonoid α],
  MulOpposite.instDivisionMonoid =
    { toDivInvMonoid := MulOpposite.instDivInvMonoid, inv_inv := ⋯, mul_inv_rev := ⋯, inv_eq_of_mul := ⋯ }
-- Mathlib.CategoryTheory.Limits.Shapes.Pullback.IsPullback.Defs
/-- The proposition that a square
```
  P --fst--> X
  |          |
 snd         f
  |          |
  v          v
  Y ---g---> Z

```
is a pullback square. (Also known as a fibered product or Cartesian square.)
 -/
CategoryTheory.IsPullback : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] → {P X Y Z : C} → (P ⟶ X) → (P ⟶ Y) → (X ⟶ Z) → (Y ⟶ Z) → Prop
-- Mathlib.Probability.Distributions.Exponential
ProbabilityTheory.exponentialPDFReal.eq_1 : ∀ (r x : ℝ), ProbabilityTheory.exponentialPDFReal r x = ProbabilityTheory.gammaPDFReal 1 r x
-- Mathlib.Algebra.Group.Subgroup.Ker
AddMonoidHom.comap_bot : ∀ {G : Type u_1} [inst : AddGroup G] {N : Type u_5} [inst_1 : AddGroup N] (f : G →+ N), AddSubgroup.comap f ⊥ = f.ker
-- Mathlib.MeasureTheory.Covering.DensityTheorem
/-- In the Vitali family `IsUnifLocDoublingMeasure.vitaliFamily K`, the sets based at `x`
contain all balls `closedBall y r` when `dist x y ≤ K * r`.  -/
IsUnifLocDoublingMeasure.closedBall_mem_vitaliFamily_of_dist_le_mul : ∀ {α : Type u_1} [inst : PseudoMetricSpace α] [inst_1 : MeasurableSpace α] (μ : MeasureTheory.Measure α)
  [inst_2 : IsUnifLocDoublingMeasure μ] [inst_3 : SecondCountableTopology α] [inst_4 : BorelSpace α]
  [inst_5 : MeasureTheory.IsLocallyFiniteMeasure μ] {K : ℝ} {x y : α} {r : ℝ},
  dist x y ≤ K * r → 0 < r → Metric.closedBall y r ∈ (IsUnifLocDoublingMeasure.vitaliFamily μ K).setsAt x
-- Mathlib.MeasureTheory.Integral.Bochner.Set
measure_le_lintegral_thickenedIndicatorAux : ∀ {X : Type u_1} [inst : MeasurableSpace X] [inst_1 : PseudoEMetricSpace X] (μ : MeasureTheory.Measure X) {E : Set X},
  MeasurableSet E → ∀ (δ : ℝ), μ E ≤ ∫⁻ (x : X), thickenedIndicatorAux δ E x ∂μ
-- Mathlib.Lean.Meta.RefinedDiscrTree
/-- `findMatches` combines `findImportMatches` and `findModuleMatches`.

* `ext` should be an environment extension with an `IO.Ref` for caching the `RefinedDiscrTree`.
* `addEntry` is the function for creating `RefinedDiscrTree` entries from constants.
* `ty` is the expression type.
* `constantsPerTask` is the number of constants in imported modules to be used for each
  new task.
* `capacityPerTask` is the initial capacity of the `HashMap` at the root of the
  `RefinedDiscrTree` for each new task.
 -/
Lean.Meta.RefinedDiscrTree.findMatches : {α : Type} →
  Lean.EnvExtension (IO.Ref (Option (Lean.Meta.RefinedDiscrTree α))) →
    (Lean.Name →
        Lean.ConstantInfo →
          Lean.MetaM (List (α × List (Lean.Meta.RefinedDiscrTree.Key × Lean.Meta.RefinedDiscrTree.LazyEntry)))) →
      Lean.Expr →
        optParam ℕ 1000 →
          optParam ℕ 128 →
            Lean.MetaM (Lean.Meta.RefinedDiscrTree.MatchResult α × Lean.Meta.RefinedDiscrTree.MatchResult α)
-- Init.Data.Nat.Lemmas
Nat.sub_eq_sub_min : ∀ (n m : ℕ), n - m = n - min n m
-- Mathlib.Topology.Algebra.FilterBasis
GroupFilterBasis.mul : ∀ {G : Type u} [inst : Group G] {B : GroupFilterBasis G} {U : Set G}, U ∈ B → ∃ V ∈ B, V * V ⊆ U
-- Mathlib.Analysis.Convex.Function
StrictConcaveOn.comp_strictConvexOn : ∀ {𝕜 : Type u_1} {E : Type u_2} {α : Type u_4} {β : Type u_5} [inst : Semiring 𝕜] [inst_1 : PartialOrder 𝕜]
  [inst_2 : AddCommMonoid E] [inst_3 : AddCommMonoid α] [inst_4 : PartialOrder α] [inst_5 : AddCommMonoid β]
  [inst_6 : PartialOrder β] [inst_7 : SMul 𝕜 E] [inst_8 : SMul 𝕜 α] [inst_9 : SMul 𝕜 β] {s : Set E} {f : E → β}
  {g : β → α},
  StrictConcaveOn 𝕜 (f '' s) g →
    StrictConvexOn 𝕜 s f → StrictAntiOn g (f '' s) → Set.InjOn f s → StrictConcaveOn 𝕜 s (g ∘ f)
-- Mathlib.Tactic.Linarith.Oracle.FourierMotzkin
/-- `elimWithSet a p comps` collects the result of calling `pelimVar p p' a`
for every `p' ∈ comps`.
 -/
Mathlib.Tactic.Linarith.elimWithSet : ℕ → Mathlib.Tactic.Linarith.PComp → Mathlib.Tactic.Linarith.PCompSet → Mathlib.Tactic.Linarith.PCompSet
-- Mathlib.CategoryTheory.Localization.LocalizerMorphism
/-- When the underlying functor `Φ.functor` of `Φ : LocalizerMorphism W₁ W₂` is
an equivalence of categories and that `W₁` and `W₂` essentially correspond to each
other via this equivalence, then `Φ` is a localized equivalence.  -/
CategoryTheory.LocalizerMorphism.IsLocalizedEquivalence.of_equivalence : ∀ {C₁ : Type u₁} {C₂ : Type u₂} [inst : CategoryTheory.Category.{v₁, u₁} C₁]
  [inst_1 : CategoryTheory.Category.{v₂, u₂} C₂] {W₁ : CategoryTheory.MorphismProperty C₁}
  {W₂ : CategoryTheory.MorphismProperty C₂} (Φ : CategoryTheory.LocalizerMorphism W₁ W₂) [Φ.functor.IsEquivalence],
  W₂ ≤ W₁.map Φ.functor → Φ.IsLocalizedEquivalence
-- Mathlib.CategoryTheory.Limits.Preserves.Shapes.Pullbacks
/-- The property of preserving pushouts expressed in terms of binary cofans.  -/
CategoryTheory.Limits.isColimitPushoutCoconeMapOfIsColimit : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    {D : Type u₂} →
      [inst_1 : CategoryTheory.Category.{v₂, u₂} D] →
        (G : CategoryTheory.Functor C D) →
          {W X Y Z : C} →
            {h : X ⟶ Z} →
              {k : Y ⟶ Z} →
                {f : W ⟶ X} →
                  {g : W ⟶ Y} →
                    (comm : CategoryTheory.CategoryStruct.comp f h = CategoryTheory.CategoryStruct.comp g k) →
                      [CategoryTheory.Limits.PreservesColimit (CategoryTheory.Limits.span f g) G] →
                        CategoryTheory.Limits.IsColimit (CategoryTheory.Limits.PushoutCocone.mk h k comm) →
                          CategoryTheory.Limits.IsColimit (CategoryTheory.Limits.PushoutCocone.mk (G.map h) (G.map k) ⋯)
-- Std.Time.Format.Basic
_private.Std.Time.Format.Basic.0.Std.Time.GenericFormat.DateBuilder.mk.inj : ∀ {G : Option Std.Time.Year.Era} {y u Y : Option Std.Time.Year.Offset} {D : Option (Sigma Std.Time.Day.Ordinal.OfYear)}
  {M L : Option Std.Time.Month.Ordinal} {d : Option Std.Time.Day.Ordinal} {Q q : Option Std.Time.Month.Quarter}
  {w : Option Std.Time.Week.OfYear.Ordinal} {W : Option Std.Time.Week.Ordinal} {E e c : Option Std.Time.Weekday}
  {F : Option (Std.Time.Internal.Bounded.LE 1 5)} {a : Option Std.Time.HourMarker} {b : Option Std.Time.DayPeriod}
  {B : Option Std.Time.ExtendedDayPeriod} {h : Option (Std.Time.Internal.Bounded.LE 1 12)}
  {K : Option (Std.Time.Internal.Bounded.LE 0 11)} {k : Option (Std.Time.Internal.Bounded.LE 1 24)}
  {H : Option Std.Time.Hour.Ordinal} {m : Option Std.Time.Minute.Ordinal} {s : Option (Std.Time.Second.Ordinal true)}
  {S : Option Std.Time.Nanosecond.Ordinal} {A : Option Std.Time.Millisecond.Offset}
  {n : Option Std.Time.Nanosecond.Ordinal} {N : Option Std.Time.Nanosecond.Offset} {V z zabbrev v : Option String}
  {O X x Z : Option Std.Time.TimeZone.Offset} {G_1 : Option Std.Time.Year.Era}
  {y_1 u_1 Y_1 : Option Std.Time.Year.Offset} {D_1 : Option (Sigma Std.Time.Day.Ordinal.OfYear)}
  {M_1 L_1 : Option Std.Time.Month.Ordinal} {d_1 : Option Std.Time.Day.Ordinal}
  {Q_1 q_1 : Option Std.Time.Month.Quarter} {w_1 : Option Std.Time.Week.OfYear.Ordinal}
  {W_1 : Option Std.Time.Week.Ordinal} {E_1 e_1 c_1 : Option Std.Time.Weekday}
  {F_1 : Option (Std.Time.Internal.Bounded.LE 1 5)} {a_1 : Option Std.Time.HourMarker} {b_1 : Option Std.Time.DayPeriod}
  {B_1 : Option Std.Time.ExtendedDayPeriod} {h_1 : Option (Std.Time.Internal.Bounded.LE 1 12)}
  {K_1 : Option (Std.Time.Internal.Bounded.LE 0 11)} {k_1 : Option (Std.Time.Internal.Bounded.LE 1 24)}
  {H_1 : Option Std.Time.Hour.Ordinal} {m_1 : Option Std.Time.Minute.Ordinal}
  {s_1 : Option (Std.Time.Second.Ordinal true)} {S_1 : Option Std.Time.Nanosecond.Ordinal}
  {A_1 : Option Std.Time.Millisecond.Offset} {n_1 : Option Std.Time.Nanosecond.Ordinal}
  {N_1 : Option Std.Time.Nanosecond.Offset} {V_1 z_1 zabbrev_1 v_1 : Option String}
  {O_1 X_1 x_1 Z_1 : Option Std.Time.TimeZone.Offset}, ⋯ → ⋯
-- Mathlib.AlgebraicTopology.SimplexCategory.Basic
SimplexCategory.eqToHom_toOrderHom : ∀ {x y : SimplexCategory} (h : x = y),
  SimplexCategory.Hom.toOrderHom (CategoryTheory.eqToHom h) = (Fin.castOrderIso ⋯).toOrderEmbedding.toOrderHom
-- Mathlib.Analysis.Convex.Join
convexJoin_empty_right : ∀ {𝕜 : Type u_2} {E : Type u_3} [inst : Semiring 𝕜] [inst_1 : PartialOrder 𝕜] [inst_2 : AddCommMonoid E]
  [inst_3 : Module 𝕜 E] (s : Set E), convexJoin 𝕜 s ∅ = ∅
-- Init.Data.Array.MinMax
_private.Init.Data.Array.MinMax.0.Array.max.eq_1 : ∀ {α : Type u_1} [inst : Max α] (arr : Array α) (h : arr ≠ #[]), arr.max h = Array.foldl max arr[0] arr 1
-- Mathlib.CategoryTheory.Limits.Fubini
CategoryTheory.Limits.diagramOfCoconesInhabited : {J : Type u_1} →
  {K : Type u_2} →
    [inst : CategoryTheory.Category.{v_1, u_1} J] →
      [inst_1 : CategoryTheory.Category.{v_2, u_2} K] →
        {C : Type u_3} →
          [inst_2 : CategoryTheory.Category.{v_3, u_3} C] →
            (F : CategoryTheory.Functor J (CategoryTheory.Functor K C)) →
              [CategoryTheory.Limits.HasColimitsOfShape K C] → Inhabited (CategoryTheory.Limits.DiagramOfCocones F)
-- Mathlib.Util.FormatTable
/-- Possible alignment modes for each table item: left-aligned, right-aligned and centered.  -/
Alignment : Type
-- Mathlib.SetTheory.Ordinal.Exponential
Ordinal.natCast_pow : ∀ (m n : ℕ), ↑(m ^ n) = ↑m ^ n
-- Mathlib.Data.Set.Function
Set.mapsTo_range_iff : ∀ {α : Type u_1} {β : Type u_2} {ι : Sort u_5} {t : Set β} {f : α → β} {g : ι → α},
  Set.MapsTo f (Set.range g) t ↔ ∀ (i : ι), f (g i) ∈ t
-- Mathlib.Data.Finset.Card
Finset.card_singleton_inter : ∀ {α : Type u_1} {s : Finset α} {a : α} [inst : DecidableEq α], ({a} ∩ s).card ≤ 1
-- Mathlib.ModelTheory.DirectLimit
FirstOrder.Language.DirectLimit.equiv_lift_of : ∀ (L : FirstOrder.Language) (ι : Type v) [inst : Preorder ι] (G : ι → Type w) [inst_1 : (i : ι) → L.Structure (G i)]
  (f : (i j : ι) → i ≤ j → L.Embedding (G i) (G j)) [inst_2 : IsDirectedOrder ι]
  [inst_3 : DirectedSystem G fun i j h => ⇑(f i j h)] [inst_4 : Nonempty ι] (G' : ι → Type w')
  [inst_5 : (i : ι) → L.Structure (G' i)] (f' : (i j : ι) → i ≤ j → L.Embedding (G' i) (G' j))
  (g : (i : ι) → L.Equiv (G i) (G' i)) [inst_6 : DirectedSystem G' fun i j h => ⇑(f' i j h)]
  (H_commuting : ∀ (i j : ι) (hij : i ≤ j) (x : G i), (g j) ((f i j hij) x) = (f' i j hij) ((g i) x)) {i : ι} (x : G i),
  (FirstOrder.Language.DirectLimit.equiv_lift L ι G f G' f' g H_commuting)
      ((FirstOrder.Language.DirectLimit.of L ι G f i) x) =
    (FirstOrder.Language.DirectLimit.of L ι G' f' i) ((g i) x)
-- Mathlib.Algebra.Category.CommAlgCat.Basic
/-- The universe lift functor for commutative algebras is fully faithful.  -/
CommAlgCat.fullyFaithfulUliftFunctor : (R : Type u) → [inst : CommRing R] → (CommAlgCat.uliftFunctor R).FullyFaithful