mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Algebra.Group.Action.TransferInstance
/-- Transfer `SMulCommClass` across an `Equiv`  -/
Equiv.smulCommClass : ∀ (M : Type u_1) (N : Type u_2) {α : Type u_4} {β : Type u_5} [inst : SMul M β] [inst_1 : SMul N β] (e : α ≃ β)
  [SMulCommClass M N β], SMulCommClass M N α
-- Mathlib.Analysis.Convex.SpecificFunctions.Deriv
Finset.prod_nonneg_of_card_nonpos_even : ∀ {α : Type u_1} {β : Type u_2} [inst : CommRing β] [inst_1 : LinearOrder β] [IsStrictOrderedRing β] {f : α → β}
  [inst_3 : DecidablePred fun x => f x ≤ 0] {s : Finset α}, Even {x ∈ s | f x ≤ 0}.card → 0 ≤ ∏ x ∈ s, f x
-- Mathlib.Analysis.Distribution.TemperateGrowth
Function.HasTemperateGrowth.of_fderiv : ∀ {E : Type u_5} {F : Type u_6} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] [inst_2 : NormedAddCommGroup F]
  [inst_3 : NormedSpace ℝ F] {f : E → F},
  Function.HasTemperateGrowth (fderiv ℝ f) →
    Differentiable ℝ f → ∀ {k : ℕ} {C : ℝ}, (∀ (x : E), ‖f x‖ ≤ C * (1 + ‖x‖) ^ k) → Function.HasTemperateGrowth f
-- Mathlib.Combinatorics.SimpleGraph.Walk.Operations
SimpleGraph.Walk.reverseAux_append : ∀ {V : Type u} {G : SimpleGraph V} {u v w x : V} (p : G.Walk u v) (q : G.Walk u w) (r : G.Walk w x),
  (p.reverseAux q).append r = p.reverseAux (q.append r)
-- Mathlib.Topology.Algebra.ContinuousMonoidHom
ContinuousAddEquiv.instHomeomorphClass : ∀ {M : Type u_1} {N : Type u_2} [inst : TopologicalSpace M] [inst_1 : TopologicalSpace N] [inst_2 : Add M]
  [inst_3 : Add N], HomeomorphClass (M ≃ₜ+ N) M N
-- Mathlib.CategoryTheory.Functor.Trifunctor
/-- Auxiliary definition for `bifunctorComp₁₂Functor`.  -/
CategoryTheory.bifunctorComp₁₂FunctorMap : {C₁ : Type u_1} →
  {C₂ : Type u_2} →
    {C₃ : Type u_3} →
      {C₄ : Type u_4} →
        {C₁₂ : Type u_5} →
          [inst : CategoryTheory.Category.{v_1, u_1} C₁] →
            [inst_1 : CategoryTheory.Category.{v_2, u_2} C₂] →
              [inst_2 : CategoryTheory.Category.{v_3, u_3} C₃] →
                [inst_3 : CategoryTheory.Category.{v_4, u_4} C₄] →
                  [inst_4 : CategoryTheory.Category.{v_5, u_5} C₁₂] →
                    {F₁₂ F₁₂' : CategoryTheory.Functor C₁ (CategoryTheory.Functor C₂ C₁₂)} →
                      (F₁₂ ⟶ F₁₂') →
                        (CategoryTheory.bifunctorComp₁₂FunctorObj F₁₂ ⟶ CategoryTheory.bifunctorComp₁₂FunctorObj F₁₂')
-- Mathlib.Data.Complex.BigOperators
Complex.im_comp_balance : ∀ {ι : Type u_2} [inst : Fintype ι] (f : ι → ℂ), Complex.im ∘ Fintype.balance f = Fintype.balance (Complex.im ∘ f)
-- Init.Data.Vector.Attach
Vector.pmap.congr_simp : ∀ {α : Type u_1} {β : Type u_2} {n : ℕ} {P : α → Prop} (f f_1 : (a : α) → P a → β),
  f = f_1 → ∀ (xs xs_1 : Vector α n) (e_xs : xs = xs_1) (H : ∀ a ∈ xs, P a), Vector.pmap f xs H = Vector.pmap f_1 xs_1 ⋯
-- Mathlib.Order.Interval.Set.Fin
Fin.preimage_addNat_uIoc_addNat : ∀ {n : ℕ} (m : ℕ) (i j : Fin n), (fun x => x.addNat m) ⁻¹' Set.uIoc (i.addNat m) (j.addNat m) = Set.uIoc i j
-- Mathlib.Data.Set.Basic
Set.nonempty_iff_univ_nonempty : ∀ {α : Type u}, Nonempty α ↔ Set.univ.Nonempty
-- Mathlib.Analysis.SpecialFunctions.Trigonometric.Inverse
Real.arcsin_pos : ∀ {x : ℝ}, 0 < Real.arcsin x ↔ 0 < x
-- Mathlib.Analysis.Analytic.Composition
/-- Target set in the change of variables to compute the composition of partial sums of formal
power series, here given a a set.  -/
FormalMultilinearSeries.compPartialSumTargetSet : ℕ → ℕ → ℕ → Set ((n : ℕ) × Composition n)
-- Mathlib.Algebra.Group.Subgroup.MulOpposite
Subgroup.opEquiv.eq_1 : ∀ {G : Type u_2} [inst : Group G],
  Subgroup.opEquiv = { toFun := Subgroup.op, invFun := Subgroup.unop, left_inv := ⋯, right_inv := ⋯, map_rel_iff' := ⋯ }
-- Init.Data.List.Find
List.isSome_finIdxOf? : ∀ {α : Type u_1} [inst : BEq α] [PartialEquivBEq α] {l : List α} {a : α}, (List.finIdxOf? a l).isSome = l.contains a
-- Std.Data.ExtDTreeMap.Lemmas
Std.ExtDTreeMap.Const.minKey_modify : ∀ {α : Type u} {cmp : α → α → Ordering} {β : Type v} {t : Std.ExtDTreeMap α (fun x => β) cmp} [inst : Std.TransCmp cmp]
  {k : α} {f : β → β} {he : Std.ExtDTreeMap.Const.modify t k f ≠ ∅},
  (Std.ExtDTreeMap.Const.modify t k f).minKey he = if cmp (t.minKey ⋯) k = Ordering.eq then k else t.minKey ⋯
-- Mathlib.GroupTheory.Finiteness
AddSubmonoid.FG.biSup : ∀ {M : Type u_1} [inst : AddMonoid M] {ι : Type u_3} {s : Set ι},
  s.Finite → ∀ (P : ι → AddSubmonoid M), (∀ i ∈ s, (P i).FG) → (⨆ i ∈ s, P i).FG
-- Mathlib.GroupTheory.GroupAction.Blocks
/-- A fixed block is an invariant block.  -/
AddAction.IsFixedBlock.isInvariantBlock : ∀ {G : Type u_1} {X : Type u_2} [inst : VAdd G X] {B : Set X},
  AddAction.IsFixedBlock G B → AddAction.IsInvariantBlock G B
-- Mathlib.CategoryTheory.Sites.EffectiveEpimorphic
CategoryTheory.Sieve.generateFamily_eq : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {B : C} {α : Type u_1} (X : α → C) (π : (a : α) → X a ⟶ B),
  CategoryTheory.Sieve.generate (CategoryTheory.Presieve.ofArrows X π) = CategoryTheory.Sieve.generateFamily X π
-- Mathlib.Analysis.InnerProductSpace.Symmetric
/-- An operator `T` on an inner product space is symmetric if and only if it is
`LinearMap.IsSelfAdjoint` with respect to the sesquilinear form given by the inner product.  -/
LinearMap.isSymmetric_iff_sesqForm : ∀ {𝕜 : Type u_1} {E : Type u_2} [inst : RCLike 𝕜] [inst_1 : SeminormedAddCommGroup E] [inst_2 : InnerProductSpace 𝕜 E]
  (T : E →ₗ[𝕜] E), T.IsSymmetric ↔ (innerₛₗ 𝕜).flip.IsSelfAdjoint ⇑T
-- Mathlib.Logic.Small.Basic
small_quotient : ∀ {α : Type u} [Small.{v, u} α] (s : Setoid α), Small.{v, u} (Quotient s)
-- Mathlib.LinearAlgebra.PiTensorProduct.Basis
/-- Let `ι` be a `Finite` type and `M` be a family of modules indexed by `ι`. If `b i : κ i → M i`
is a basis for every `i` in `ι`, then `fun (p : Π i, κ i) ↦ ⨂ₜ[R] i, b i (p i)` is a basis
of `⨂[R] i, M i`.
 -/
Basis.piTensorProduct : {ι : Type u_1} →
  {R : Type u_2} →
    {M : ι → Type u_3} →
      {κ : ι → Type u_4} →
        [inst : CommSemiring R] →
          [inst_1 : (i : ι) → AddCommMonoid (M i)] →
            [inst_2 : (i : ι) → Module R (M i)] →
              [Finite ι] →
                ((i : ι) → Module.Basis (κ i) R (M i)) → Module.Basis ((i : ι) → κ i) R (PiTensorProduct R fun i => M i)
-- Mathlib.Order.Interval.Finset.Basic
Finset.Icc_subset_uIcc : ∀ {α : Type u_2} [inst : Lattice α] [inst_1 : LocallyFiniteOrder α] {a b : α}, Finset.Icc a b ⊆ Finset.uIcc a b
-- Mathlib.Analysis.Polynomial.MahlerMeasure
Polynomial.mapMahlerMeasure_le_sum_norm_coeff : ∀ {A : Type u_2} [inst : NormedRing A] (p : Polynomial A) (v : A →+* ℂ),
  Isometry ⇑v → p.mapMahlerMeasure v ≤ p.sum fun x a => ‖a‖
-- Mathlib.Analysis.RCLike.Basic
/-- The natural `ℝ`-linear isometry equivalence between `𝕜` satisfying `RCLike 𝕜` and `ℝ` when
`RCLike.I = 0`.  -/
RCLike.realLinearIsometryEquiv : {K : Type u_1} → [inst : RCLike K] → RCLike.I = 0 → K ≃ₗᵢ[ℝ] ℝ
-- Lean.LibrarySuggestions.Basic
/-- A library suggestion engine that returns locally defined theorems (those in the current file).  -/
Lean.LibrarySuggestions.currentFile : Lean.LibrarySuggestions.Selector
-- Mathlib.Algebra.Ring.Int.Parity
Int.not_even_two_mul_add_one : ∀ (n : ℤ), ¬Even (2 * n + 1)
-- Mathlib.CategoryTheory.Limits.Shapes.Biproducts
CategoryTheory.Limits.biproduct.map_desc_assoc : ∀ {J : Type w} {C : Type u} [inst : CategoryTheory.Category.{v, u} C]
  [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C] {f g : J → C} [inst_2 : CategoryTheory.Limits.HasBiproduct f]
  [inst_3 : CategoryTheory.Limits.HasBiproduct g] (p : (j : J) → f j ⟶ g j) {P : C} (k : (j : J) → g j ⟶ P) {Z : C}
  (h : P ⟶ Z),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.biproduct.map p)
      (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.biproduct.desc k) h) =
    CategoryTheory.CategoryStruct.comp
      (CategoryTheory.Limits.biproduct.desc fun j => CategoryTheory.CategoryStruct.comp (p j) (k j)) h
-- Lean.Meta.Match.SimpH
_private.Lean.Meta.Match.SimpH.0.Lean.Meta.Match.SimpH.processNextEq : Lean.Meta.Match.SimpH.M✝ Bool
-- Aesop.Util.EqualUpToIds
Aesop.EqualUpToIds.MVarValue.delayedAssignment.injEq : ∀ (da da_1 : Lean.DelayedMetavarAssignment),
  (Aesop.EqualUpToIds.MVarValue.delayedAssignment da = Aesop.EqualUpToIds.MVarValue.delayedAssignment da_1) =
    (da = da_1)
-- Init.Data.Rat.Lemmas
Rat.sub_self : ∀ {a : ℚ}, a - a = 0
-- Mathlib.Topology.MetricSpace.Similarity
/-- A similarity pairwise scales extended distance. Forward direction of
`similar_iff_exists_pairwise_edist_eq`.  -/
Similar.exists_pairwise_edist_eq : ∀ {ι : Type u_1} {P₁ : Type u_3} {P₂ : Type u_4} {v₁ : ι → P₁} {v₂ : ι → P₂} [inst : PseudoEMetricSpace P₁]
  [inst_1 : PseudoEMetricSpace P₂],
  Similar v₁ v₂ → ∃ r, r ≠ 0 ∧ Pairwise fun i₁ i₂ => edist (v₁ i₁) (v₁ i₂) = ↑r * edist (v₂ i₁) (v₂ i₂)
-- Mathlib.Algebra.Category.CoalgCat.Basic
CoalgCat.of_comul : ∀ {R : Type u} [inst : CommRing R] {X : Type v} [inst_1 : AddCommGroup X] [inst_2 : Module R X]
  [inst_3 : Coalgebra R X], CoalgebraStruct.comul = CoalgebraStruct.comul
-- Mathlib.SetTheory.Ordinal.Family
Ordinal.lt_lsub : ∀ {ι : Type u_3} (f : ι → Ordinal.{max u_4 u_3}) (i : ι), f i < Ordinal.lsub f
-- Std.Time.DateTime.PlainDateTime
/-- Subtracts a `Month.Offset` from a `PlainDateTime`, rolling over excess days to the following month if
needed.
 -/
Std.Time.PlainDateTime.addYearsClip : Std.Time.PlainDateTime → Std.Time.Year.Offset → Std.Time.PlainDateTime
-- Init.Data.String.Lemmas.Pattern.TakeDrop.Basic
String.Slice.skipPrefixWhile_eq_startPos_iff : ∀ {ρ : Type} {pat : ρ} [inst : String.Slice.Pattern.Model.PatternModel pat]
  [String.Slice.Pattern.Model.StrictPatternModel pat] [inst_2 : String.Slice.Pattern.ForwardPattern pat]
  [String.Slice.Pattern.Model.LawfulForwardPatternModel pat] {s : String.Slice},
  s.skipPrefixWhile pat = s.startPos ↔ s.startsWith pat = false
-- Batteries.Data.UInt
UInt8.max_def : ∀ (x y : UInt8), x ⊔ y = if x ≤ y then y else x
-- Mathlib.Condensed.Light.Module
instIsLeftAdjointLightCondSetLightCondModFree : ∀ (R : Type u) [inst : Ring R], (LightCondensed.free R).IsLeftAdjoint
-- Mathlib.LinearAlgebra.PiTensorProduct.Generators
PiTensorProduct.equivPiTensorComplSingletonTensor_symm_tmul : ∀ (R : Type u_1) {ι : Type u_2} [inst : DecidableEq ι] (M : ι → Type u_3) [inst_1 : CommSemiring R]
  [inst_2 : (i : ι) → AddCommMonoid (M i)] [inst_3 : (i : ι) → Module R (M i)] (i₀ : ι)
  (m : (i : ↑(Set.singleton i₀)ᶜ) → M ↑i) (x : M i₀),
  (PiTensorProduct.equivPiTensorComplSingletonTensor R M i₀).symm (((PiTensorProduct.tprod R) fun j => m j) ⊗ₜ[R] x) =
    ⨂ₜ[R] (i : ι), Function.subtypeNeLift i₀ m x i
-- Mathlib.CategoryTheory.Enriched.Ordinary.Basic
CategoryTheory.eHom_whisker_cancel_inv_assoc : ∀ (V : Type u') [inst : CategoryTheory.Category.{v', u'} V] [inst_1 : CategoryTheory.MonoidalCategory V] {C : Type u}
  [inst_2 : CategoryTheory.Category.{v, u} C] [inst_3 : CategoryTheory.EnrichedOrdinaryCategory V C] {X Y Y₁ Z : C}
  (α : Y ≅ Y₁) {Z_1 : V} (h : (X ⟶[V] Z) ⟶ Z_1),
  CategoryTheory.CategoryStruct.comp
      (CategoryTheory.MonoidalCategoryStruct.whiskerRight (CategoryTheory.eHomWhiskerLeft V X α.inv) (Y₁ ⟶[V] Z))
      (CategoryTheory.CategoryStruct.comp
        (CategoryTheory.MonoidalCategoryStruct.whiskerLeft (X ⟶[V] Y) (CategoryTheory.eHomWhiskerRight V α.hom Z))
        (CategoryTheory.CategoryStruct.comp (CategoryTheory.eComp V X Y Z) h)) =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.eComp V X Y₁ Z) h
-- Mathlib.Algebra.Group.Center
Set.centralizer_eq_top_iff_subset : ∀ {M : Type u_1} {S : Set M} [inst : Semigroup M], S.centralizer = Set.univ ↔ S ⊆ Set.center M
-- Mathlib.CategoryTheory.Category.Bipointed
Bipointed.hasForget : CategoryTheory.ConcreteCategory Bipointed Bipointed.HomSubtype
-- Mathlib.CategoryTheory.Monoidal.Mon
/-- Auxiliary definition for `counitIso`.  -/
CategoryTheory.AddMon.EquivLaxMonoidalFunctorPUnit.counitIsoAux : (C : Type u₁) →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    [inst_1 : CategoryTheory.MonoidalCategory C] →
      (F : CategoryTheory.AddMon C) →
        (((CategoryTheory.AddMon.EquivLaxMonoidalFunctorPUnit.addMonToLaxMonoidal C).comp
                  (CategoryTheory.AddMon.EquivLaxMonoidalFunctorPUnit.laxMonoidalToAddMon C)).obj
              F).X ≅
          ((CategoryTheory.Functor.id (CategoryTheory.AddMon C)).obj F).X
-- Mathlib.SetTheory.Cardinal.HasCardinalLT
hasCardinalLT_sigma : ∀ {ι : Type u} (α : ι → Type v) (κ : Cardinal.{w}) [Fact κ.IsRegular],
  HasCardinalLT ι κ → (∀ (i : ι), HasCardinalLT (α i) κ) → HasCardinalLT ((i : ι) × α i) κ
-- Mathlib.Algebra.Homology.ShortComplex.Exact
CategoryTheory.ShortComplex.Exact.lift.congr_simp : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Preadditive C]
  {S : CategoryTheory.ShortComplex C} [inst_2 : CategoryTheory.Balanced C] (hS : S.Exact) {A : C} (k k_1 : A ⟶ S.X₂)
  (e_k : k = k_1) (hk : CategoryTheory.CategoryStruct.comp k S.g = 0) [inst_3 : CategoryTheory.Mono S.f],
  hS.lift k hk = hS.lift k_1 ⋯
-- Mathlib.CategoryTheory.Bicategory.Strict.Pseudofunctor
CategoryTheory.Pseudofunctor.mapComp'₀₁₃_inv_comp_mapComp'₀₂₃_hom_assoc : ∀ {B : Type u₁} {C : Type u₂} [inst : CategoryTheory.Bicategory B] [inst_1 : CategoryTheory.Bicategory.Strict B]
  [inst_2 : CategoryTheory.Bicategory C] (F : CategoryTheory.Pseudofunctor B C) {b₀ b₁ b₂ b₃ : B} (f₀₁ : b₀ ⟶ b₁)
  (f₁₂ : b₁ ⟶ b₂) (f₂₃ : b₂ ⟶ b₃) (f₀₂ : b₀ ⟶ b₂) (f₁₃ : b₁ ⟶ b₃) (f : b₀ ⟶ b₃)
  (h₀₂ : CategoryTheory.CategoryStruct.comp f₀₁ f₁₂ = f₀₂) (h₁₃ : CategoryTheory.CategoryStruct.comp f₁₂ f₂₃ = f₁₃)
  (hf : CategoryTheory.CategoryStruct.comp f₀₁ f₁₃ = f) {Z : F.obj b₀ ⟶ F.obj b₃}
  (h : CategoryTheory.CategoryStruct.comp (F.map f₀₂) (F.map f₂₃) ⟶ Z),
  CategoryTheory.CategoryStruct.comp (F.mapComp' f₀₁ f₁₃ f ⋯).inv
      (CategoryTheory.CategoryStruct.comp (F.mapComp' f₀₂ f₂₃ f ⋯).hom h) =
    CategoryTheory.CategoryStruct.comp
      (CategoryTheory.Bicategory.whiskerLeft (F.map f₀₁) (F.mapComp' f₁₂ f₂₃ f₁₃ h₁₃).hom)
      (CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.associator (F.map f₀₁) (F.map f₁₂) (F.map f₂₃)).inv
        (CategoryTheory.CategoryStruct.comp
          (CategoryTheory.Bicategory.whiskerRight (F.mapComp' f₀₁ f₁₂ f₀₂ h₀₂).inv (F.map f₂₃)) h))
-- Mathlib.Topology.Algebra.ContinuousAffineEquiv
ContinuousAffineEquiv.toAffineEquiv_constVSub : ∀ (k : Type u_1) {P₁ : Type u_2} {V₁ : Type u_6} [inst : Ring k] [inst_1 : AddCommGroup V₁] [inst_2 : Module k V₁]
  [inst_3 : AddTorsor V₁ P₁] [inst_4 : TopologicalSpace P₁] [inst_5 : TopologicalSpace V₁]
  [inst_6 : IsTopologicalAddTorsor P₁] {p : P₁}, ↑(ContinuousAffineEquiv.constVSub k p) = AffineEquiv.constVSub k p
-- Mathlib.AlgebraicGeometry.Cover.Open
/-- The affine cover of a scheme.  -/
AlgebraicGeometry.Scheme.affineCover : (X : AlgebraicGeometry.Scheme) → X.OpenCover
-- Lean.Parser.Term.Basic
Lean.Parser.Term.omission.parenthesizer : Lean.PrettyPrinter.Parenthesizer
-- Mathlib.Data.List.AList
AList.keys_singleton : ∀ {α : Type u} {β : α → Type v} (a : α) (b : β a), (AList.singleton a b).keys = [a]
-- Mathlib.AlgebraicTopology.SimplicialSet.AnodyneExtensions.RelativeCellComplex
SSet.Subcomplex.Pairing.RankFunction.filtration_def : ∀ {X : SSet} {A : X.Subcomplex} {P : A.Pairing} {ι : Type v} [inst : LinearOrder ι] (f : P.RankFunction ι) (i : ι),
  f.filtration i = A ⊔ ⨆ j, ⨆ (_ : j < i), ⨆ c, (↑(P.p c.s)).subcomplex
-- Mathlib.CategoryTheory.Limits.Cones
/-- A `c : Cocone F` is
* an object `c.pt` and
* a natural transformation `c.ι : F ⟶ c.pt` from `F` to the constant `c.pt` functor.

For example, if the source `J` of `F` is a partially ordered set, then to give
`c : Cocone F` is to give a collection of morphisms `ιⱼ : F j ⟶ c.pt` and, for
all `j ≤ k` in `J`, morphisms `ιⱼₖ : F j ⟶ F k` such that `Fⱼₖ ≫ Fₖ = Fⱼ` for all `j ≤ k`.

`Cocone F` is equivalent, via `Cone.equiv` below, to `Σ X, F.cocones.obj X`.
 -/
CategoryTheory.Limits.Cocone : {J : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} J] →
    {C : Type u₃} →
      [inst_1 : CategoryTheory.Category.{v₃, u₃} C] → CategoryTheory.Functor J C → Type (max (max u₁ u₃) v₃)
-- Mathlib.LinearAlgebra.RootSystem.Hom
RootPairing.Hom.id_coweightMap_apply : ∀ {ι : Type u_1} {R : Type u_2} {M : Type u_3} {N : Type u_4} [inst : CommRing R] [inst_1 : AddCommGroup M]
  [inst_2 : Module R M] [inst_3 : AddCommGroup N] [inst_4 : Module R N] (P : RootPairing ι R M N) (x : N),
  (RootPairing.Hom.id P).coweightMap x = x
-- Init.Data.Int.DivMod.Lemmas
Int.emod_natAbs_of_neg : ∀ {x : ℤ}, x < 0 → ∀ {n : ℕ}, n ≠ 0 → x.natAbs % n = if ↑n ∣ x then 0 else n - (x % ↑n).toNat
-- Init.Grind.Ring.CommSolver
Lean.Grind.CommRing.Expr.add : Lean.Grind.CommRing.Expr → Lean.Grind.CommRing.Expr → Lean.Grind.CommRing.Expr
-- Init.Data.Range.Polymorphic.IntLemmas
Int.getElem_toArray_rco : ∀ {m n : ℤ} {i : ℕ} (_h : i < (m...n).toArray.size), (m...n).toArray[i] = m + ↑i
-- Mathlib.CategoryTheory.Limits.Shapes.MultiequalizerPullback
CategoryTheory.Limits.Multicofork.IsColimit.isPushout.multicofork_π_eq_inl : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] {J : CategoryTheory.Limits.MultispanShape}
  [inst_1 : Unique J.L] {I : CategoryTheory.Limits.MultispanIndex J C} (h : {J.fst default, J.snd default} = Set.univ)
  (h' : J.fst default ≠ J.snd default) (s : CategoryTheory.Limits.PushoutCocone (I.fst default) (I.snd default)),
  (CategoryTheory.Limits.Multicofork.IsColimit.isPushout.multicofork h h' s).π (J.fst default) = s.inl
-- Mathlib.Order.Filter.Bases.Basic
Filter.hasBasis_iInf_of_directed : ∀ {α : Type u_1} {ι : Type u_6} {ι' : Type u_7} [Nonempty ι] {l : ι → Filter α} (s : ι → ι' → Set α)
  (p : ι → ι' → Prop),
  (∀ (i : ι), (l i).HasBasis (p i) (s i)) →
    Directed (fun x1 x2 => x1 ≥ x2) l → (⨅ i, l i).HasBasis (fun ii' => p ii'.1 ii'.2) fun ii' => s ii'.1 ii'.2
-- Mathlib.Analysis.Calculus.Deriv.Polynomial
Polynomial.differentiable : ∀ {𝕜 : Type u} [inst : NontriviallyNormedField 𝕜] (p : Polynomial 𝕜), Differentiable 𝕜 fun x => Polynomial.eval x p
-- Init.Data.Nat.Coprime
Nat.Coprime.gcd_mul_left_cancel : ∀ {k n : ℕ} (m : ℕ), k.Coprime n → (k * m).gcd n = m.gcd n
-- Batteries.Data.MLList.Basic
_private.Batteries.Data.MLList.Basic.0.MLList.Spec.cons : {m : Type u → Type u} →
  (self : MLList.Spec✝ m) → {α : Type u} → α → MLList.Spec.listM✝ self α → MLList.Spec.listM✝ self α
-- Mathlib.CategoryTheory.Galois.Basic
/-- An epimorphism induces a surjective map on fibers.  -/
CategoryTheory.PreGaloisCategory.surjective_on_fiber_of_epi : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{u₂, u₁} C] (F : CategoryTheory.Functor C FintypeCat)
  [inst_1 : CategoryTheory.PreGaloisCategory C] [CategoryTheory.PreGaloisCategory.FiberFunctor F] {X Y : C} (f : X ⟶ Y)
  [CategoryTheory.Epi f], Function.Surjective ⇑(CategoryTheory.ConcreteCategory.hom (F.map f))
-- Lean.Meta.Sym.AbstractS
_private.Lean.Meta.Sym.AbstractS.0.Lean.Meta.Sym.abstractFVarsRange.go.eq_def : ∀ (start : ℕ) (xs : Array Lean.Expr) (fvarId : Lean.FVarId) (bidx i : ℕ) (h : i < xs.size),
  Lean.Meta.Sym.abstractFVarsRange.go✝ start xs fvarId bidx i h =
    if (xs[i].fvarId! == fvarId) = true then some bidx
    else if i > start then Lean.Meta.Sym.abstractFVarsRange.go✝ start xs fvarId (bidx + 1) (i - 1) ⋯ else none
-- Lean.Data.Lsp.Window
Lean.Lsp.MessageActionItem : Type
-- Mathlib.CategoryTheory.Generator.Presheaf
CategoryTheory.Presheaf.freeYonedaHomEquiv_symm_comp : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {A : Type u'} [inst_1 : CategoryTheory.Category.{v', u'} A]
  [inst_2 : CategoryTheory.Limits.HasCoproducts A] {X : C} {M : A} {F G : CategoryTheory.Functor Cᵒᵖ A}
  (α : M ⟶ F.obj (Opposite.op X)) (f : F ⟶ G),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.Presheaf.freeYonedaHomEquiv.symm α) f =
    CategoryTheory.Presheaf.freeYonedaHomEquiv.symm (CategoryTheory.CategoryStruct.comp α (f.app (Opposite.op X)))
-- Mathlib.Algebra.Group.Prod
Prod.addCommMagma : {M : Type u_3} → {N : Type u_4} → [AddCommMagma M] → [AddCommMagma N] → AddCommMagma (M × N)
-- Std.Http.Data.Response
Std.Http.Response.Head.mk.inj : ∀ {status : Std.Http.Status} {version : Std.Http.Version} {headers : Std.Http.Headers} {status_1 : Std.Http.Status}
  {version_1 : Std.Http.Version} {headers_1 : Std.Http.Headers},
  { status := status, version := version, headers := headers } =
      { status := status_1, version := version_1, headers := headers_1 } →
    status = status_1 ∧ version = version_1 ∧ headers = headers_1
-- Mathlib.Algebra.Group.Action.Units
Units.smul_isUnit : ∀ {M : Type u_3} {α : Type u_5} [inst : Monoid M] [inst_1 : SMul M α] {m : M} (hm : IsUnit m) (a : α),
  hm.unit • a = m • a
-- Mathlib.Data.Int.Init
/-- For use in `Mathlib/Tactic/NormNum/Pow.lean`  -/
Int.pow_eq : ∀ (m : ℤ) (n : ℕ), m.pow n = m ^ n
-- Init.PropLemmas
not_not_em : ∀ (a : Prop), ¬¬(a ∨ ¬a)
-- Mathlib.CategoryTheory.Preadditive.AdditiveFunctor
CategoryTheory.exactFunctor_le_additiveFunctor : ∀ (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]
  [CategoryTheory.Limits.HasZeroObject C] [CategoryTheory.Limits.HasZeroObject D]
  [CategoryTheory.Limits.HasBinaryBiproducts C], CategoryTheory.exactFunctor C D ≤ CategoryTheory.additiveFunctor C D
-- Mathlib.Combinatorics.Configuration
/-- The order of a projective plane is one less than the number of lines through an arbitrary point.
Equivalently, it is one less than the number of points on an arbitrary line.  -/
Configuration.ProjectivePlane.order : (P : Type u_1) → (L : Type u_2) → [inst : Membership P L] → [Configuration.ProjectivePlane P L] → ℕ
-- Std.Internal.Do.WP.Basic
/-- The weakest precondition transformer for a program.  -/
Std.Internal.Do.WP.wpTrans : {Prog : Type u} →
  {Value : outParam (Type v)} →
    {Pred : outParam (Type w)} →
      {EPred : outParam (Type w')} →
        {inst : Std.Internal.Do.Assertion Pred} →
          {inst_1 : Std.Internal.Do.Assertion EPred} →
            [self : Std.Internal.Do.WP Prog Value Pred EPred] → Prog → Std.Internal.Do.PredTrans Pred EPred Value
-- Init.Data.Iterators.Lemmas.Combinators.Take
_private.Init.Data.Iterators.Lemmas.Combinators.Take.0.Std.IterM.step_take.match_1.eq_2 : ∀ {α : Type u_1} {m : Type u_1 → Type u_2} {β : Type u_1} [inst : Std.Iterator α m β] {it : Std.IterM m β}
  (motive : it.Step → Sort u_3) (it' : Std.IterM m β) (h : it.IsPlausibleStep (Std.IterStep.skip it'))
  (h_1 :
    (it' : Std.IterM m β) →
      (out : β) → (h : it.IsPlausibleStep (Std.IterStep.yield it' out)) → motive ⟨Std.IterStep.yield it' out, h⟩)
  (h_2 : (it' : Std.IterM m β) → (h : it.IsPlausibleStep (Std.IterStep.skip it')) → motive ⟨Std.IterStep.skip it', h⟩)
  (h_3 : (h : it.IsPlausibleStep Std.IterStep.done) → motive ⟨Std.IterStep.done, h⟩),
  (match ⟨Std.IterStep.skip it', h⟩ with
    | ⟨Std.IterStep.yield it' out, h⟩ => h_1 it' out h
    | ⟨Std.IterStep.skip it', h⟩ => h_2 it' h
    | ⟨Std.IterStep.done, h⟩ => h_3 h) =
    h_2 it' h
-- Mathlib.CategoryTheory.Limits.Shapes.Reflexive
CategoryTheory.Limits.π_reflexiveCoequalizerIsoCoequalizer_inv_assoc : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C]
  (F : CategoryTheory.Functor CategoryTheory.Limits.WalkingReflexivePair C)
  [inst_1 :
    CategoryTheory.Limits.HasCoequalizer (F.map CategoryTheory.Limits.WalkingReflexivePair.Hom.left)
      (F.map CategoryTheory.Limits.WalkingReflexivePair.Hom.right)]
  {Z : C} (h : CategoryTheory.Limits.colimit F ⟶ Z),
  CategoryTheory.CategoryStruct.comp
      (CategoryTheory.Limits.coequalizer.π (F.map CategoryTheory.Limits.WalkingReflexivePair.Hom.left)
        (F.map CategoryTheory.Limits.WalkingReflexivePair.Hom.right))
      (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.reflexiveCoequalizerIsoCoequalizer F).inv h) =
    CategoryTheory.CategoryStruct.comp
      (CategoryTheory.Limits.colimit.ι F CategoryTheory.Limits.WalkingReflexivePair.zero) h
-- Mathlib.Order.SetDissipate
Set.dissipate_subset : ∀ {α : Type u_1} {β : Type u_2} {s : α → Set β} [inst : LE α] {x y : α}, y ≤ x → Set.dissipate s x ⊆ s y