mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Algebra.Homology.ShortComplex.Linear
CategoryTheory.ShortComplex.rightHomologyFunctor_linear : ∀ {R : Type u_1} {C : Type u_2} [inst : Semiring R] [inst_1 : CategoryTheory.Category.{v_1, u_2} C]
  [inst_2 : CategoryTheory.Preadditive C] [inst_3 : CategoryTheory.Linear R C]
  [inst_4 : CategoryTheory.Limits.HasKernels C] [inst_5 : CategoryTheory.Limits.HasCokernels C],
  CategoryTheory.Functor.Linear R (CategoryTheory.ShortComplex.rightHomologyFunctor C)
-- Init.Data.SInt.Bitwise
Int32.shiftLeft_zero : ∀ {a : Int32}, a <<< 0 = a
-- Mathlib.Combinatorics.Additive.Corner.Roth
_private.Mathlib.Combinatorics.Additive.Corner.Roth.0.Corners.noAccidental : ∀ {G : Type u_1} [inst : AddCommGroup G] {A : Finset (G × G)},
  IsCornerFree ↑A → SimpleGraph.TripartiteFromTriangles.NoAccidental (Corners.triangleIndices✝ A)
-- Mathlib.Topology.ApproximateUnit
/-- In a topological unital magma, `𝓝 1` is the largest approximate unit.  -/
Filter.IsApproximateUnit.iff_le_nhds_one : ∀ {α : Type u_1} [inst : TopologicalSpace α] [inst_1 : MulOneClass α] [SeparatelyContinuousMul α] {l : Filter α}
  [l.NeBot], l.IsApproximateUnit ↔ l ≤ nhds 1
-- Mathlib.Analysis.Asymptotics.Defs
Asymptotics.IsLittleO.const_mul_right : ∀ {α : Type u_1} {E : Type u_3} [inst : Norm E] {S : Type u_17} [inst_1 : NormedRing S] [NormMulClass S] {f : α → E}
  {l : Filter α} {g : α → S} {c : S}, c ≠ 0 → f =o[l] g → f =o[l] fun x => c * g x
-- Mathlib.AlgebraicTopology.ModelCategory.Cylinder
HomotopicalAlgebra.Precylinder.map_i₀ : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {X : C} (P : HomotopicalAlgebra.Precylinder X) {D : Type u_1}
  [inst_1 : CategoryTheory.Category.{v_1, u_1} D] (F : CategoryTheory.Functor C D), (P.map F).i₀ = F.map P.i₀
-- Mathlib.Order.Filter.Pointwise
Filter.smul_le_smul_right : ∀ {α : Type u_2} {β : Type u_3} [inst : SMul α β] {f₁ f₂ : Filter α} {g : Filter β}, f₁ ≤ f₂ → f₁ • g ≤ f₂ • g
-- Std.Do.SPred.DerivedLaws
Std.Do.SPred.Tactic.Cases.pure : ∀ {σs : List (Type u_1)} {Q T : Std.Do.SPred σs}, (Q ∧ ⌜True⌝ ⊢ₛ T) → Q ⊢ₛ T
-- Mathlib.Algebra.Category.ModuleCat.Sheaf
SheafOfModules.Hom.mk : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    {J : CategoryTheory.GrothendieckTopology C} →
      {R : CategoryTheory.Sheaf J RingCat} → {X Y : SheafOfModules R} → (X.val ⟶ Y.val) → X.Hom Y
-- Lean.CoreM
Lean.Core.instantiateValueLevelParams : Lean.ConstantInfo → List Lean.Level → optParam Bool false → Lean.CoreM Lean.Expr
-- Mathlib.Algebra.Ring.Subsemiring.Basic
Subsemiring.map_toSubmonoid : ∀ {R : Type u} {S : Type v} [inst : NonAssocSemiring R] [inst_1 : NonAssocSemiring S] (f : R →+* S) (s : Subsemiring R),
  (Subsemiring.map f s).toSubmonoid = { carrier := ⇑f '' ↑s, mul_mem' := ⋯, one_mem' := ⋯ }
-- Mathlib.Logic.Equiv.PartialEquiv
PartialEquiv.mapsTo : ∀ {α : Type u_1} {β : Type u_2} (e : PartialEquiv α β), Set.MapsTo (↑e) e.source e.target
-- Mathlib.Algebra.Ring.Opposite
/-- The 'unopposite' of a non-unital ring hom `Rᵐᵒᵖ →ₙ+* Sᵐᵒᵖ`. Inverse to
`NonUnitalRingHom.op`.  -/
NonUnitalRingHom.unop : {R : Type u_2} →
  {S : Type u_3} →
    [inst : NonUnitalNonAssocSemiring R] → [inst_1 : NonUnitalNonAssocSemiring S] → (Rᵐᵒᵖ →ₙ+* Sᵐᵒᵖ) ≃ (R →ₙ+* S)
-- Mathlib.Topology.ContinuousMap.ZeroAtInfty
ZeroAtInftyContinuousMap.instNonUnitalSemiring : {α : Type u} →
  {β : Type v} →
    [inst : TopologicalSpace α] →
      [inst_1 : TopologicalSpace β] →
        [inst_2 : NonUnitalSemiring β] → [IsTopologicalSemiring β] → NonUnitalSemiring (ZeroAtInftyContinuousMap α β)
-- Mathlib.NumberTheory.Ostrowski
/-- The absolute value of `p` is `p ^ (-t)` for some positive real number `t`.  -/
Rat.AbsoluteValue.exists_pos_eq_pow_neg : ∀ {f : AbsoluteValue ℚ ℝ} {p : ℕ},
  0 < f ↑p → f ↑p < 1 → (∀ (m : ℕ), 0 < f ↑m ∧ f ↑m < 1 → p ≤ m) → ∃ t, 0 < t ∧ f ↑p = ↑p ^ (-t)
-- Mathlib.Logic.Equiv.Defs
Equiv.congr_fun : ∀ {α : Sort u} {β : Sort v} {f g : α ≃ β}, f = g → ∀ (x : α), f x = g x
-- Lean.Meta.Tactic.Grind.Theorems
/-- Inserts a `thm` with symbols `[s_1, ..., s_n]` to `s`.
We add `s_1 -> { thm with symbols := [s_2, ..., s_n] }`.
When `grind` internalizes a term containing symbol `s`, we
process all theorems `thm` associated with key `s`.
If their `thm.symbols` is empty, we say they are activated.
Otherwise, we reinsert into `map`.
 -/
Lean.Meta.Grind.Theorems.insert : {α : Type} → [Lean.Meta.Grind.TheoremLike α] → Lean.Meta.Grind.Theorems α → α → Lean.Meta.Grind.Theorems α
-- Init.Data.Nat.Bitwise.Lemmas
Nat.shiftLeft_or_distrib : ∀ {i a b : ℕ}, (a ||| b) <<< i = a <<< i ||| b <<< i
-- Mathlib.Data.Int.ModEq
Int.ModEq.add_left_cancel : ∀ {n a b c d : ℤ}, a ≡ b [ZMOD n] → a + c ≡ b + d [ZMOD n] → c ≡ d [ZMOD n]
-- Mathlib.Order.LiminfLimsup
Filter.liminf_congr : ∀ {β : Type u_2} {α : Type u_6} [inst : ConditionallyCompleteLattice β] {f : Filter α} {u v : α → β},
  (∀ᶠ (a : α) in f, u a = v a) → Filter.liminf u f = Filter.liminf v f
-- Mathlib.Algebra.Polynomial.Splits
Polynomial.Splits.of_natDegree_eq_one : ∀ {R : Type u_1} [inst : DivisionSemiring R] {f : Polynomial R}, f.natDegree = 1 → f.Splits
-- Std.Data.DTreeMap.Raw.Lemmas
Std.DTreeMap.Raw.Const.get!_unitOfList : ∀ {α : Type u} {cmp : α → α → Ordering} {l : List α} {k : α},
  Std.DTreeMap.Raw.Const.get! (Std.DTreeMap.Raw.Const.unitOfList l cmp) k = ()
-- Mathlib.Order.Lattice
Prod.mk_sup_mk : ∀ (α : Type u) (β : Type v) [inst : Max α] [inst_1 : Max β] (a₁ a₂ : α) (b₁ b₂ : β),
  (a₁, b₁) ⊔ (a₂, b₂) = (a₁ ⊔ a₂, b₁ ⊔ b₂)
-- Std.Data.ExtDHashMap.Lemmas
Std.ExtDHashMap.Const.getKeyD_filter : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} {β : Type v} {m : Std.ExtDHashMap α fun x => β} [inst : EquivBEq α]
  [inst_1 : LawfulHashable α] {f : α → β → Bool} {k fallback : α},
  (Std.ExtDHashMap.filter f m).getKeyD k fallback =
    ((m.getKey? k).pfilter fun x_2 h' => f x_2 (Std.ExtDHashMap.Const.get m x_2 ⋯)).getD fallback
-- Mathlib.Order.Basic
/-- **Alias** of `eq_of_le_of_not_lt'`. -/
LE.le.eq_of_not_lt' : ∀ {α : Type u_2} [inst : PartialOrder α] {a b : α}, b ≤ a → ¬b < a → a = b
-- Mathlib.Algebra.Category.Semigrp.Basic
AddSemigrp.Hom.ext : ∀ {A B : AddSemigrp} {x y : A.Hom B}, x.hom' = y.hom' → x = y
-- Mathlib.RingTheory.Congruence.Opposite
RingCon.unop_iff : ∀ {R : Type u_1} [inst : Add R] [inst_1 : Mul R] {c : RingCon Rᵐᵒᵖ} {x y : R},
  c.unop x y ↔ c (MulOpposite.op y) (MulOpposite.op x)
-- Mathlib.Data.Num.ZNum
ZNum.bit0_of_bit0 : ∀ (n : ZNum), n + n = n.bit0
-- Mathlib.CategoryTheory.WithTerminal.Basic
CategoryTheory.WithTerminal.mapId_inv_app : ∀ (C : Type u_1) [inst : CategoryTheory.Category.{v_1, u_1} C] (X : CategoryTheory.WithTerminal C),
  (CategoryTheory.WithTerminal.mapId C).inv.app X =
    (match X with
      | CategoryTheory.WithTerminal.of a => CategoryTheory.Iso.refl (CategoryTheory.WithTerminal.of a)
      | CategoryTheory.WithTerminal.star => CategoryTheory.Iso.refl CategoryTheory.WithTerminal.star).inv
-- Mathlib.Algebra.Category.Grp.FiniteGrp
FiniteGrp.instCategory : CategoryTheory.Category.{u_1, u_1 + 1} FiniteGrp.{u_1}
-- Mathlib.CategoryTheory.Limits.Shapes.Pullback.Cospan
/-- A functor applied to a cospan is a cospan.  -/
CategoryTheory.Limits.cospanCompIso : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    {D : Type u₂} →
      [inst_1 : CategoryTheory.Category.{v₂, u₂} D] →
        (F : CategoryTheory.Functor C D) →
          {X Y Z : C} →
            (f : X ⟶ Z) →
              (g : Y ⟶ Z) → (CategoryTheory.Limits.cospan f g).comp F ≅ CategoryTheory.Limits.cospan (F.map f) (F.map g)
-- Std.Time.Time.Unit.Nanosecond
Std.Time.Nanosecond.Ordinal.instLawfulEqOrdOfDay : Std.LawfulEqOrd Std.Time.Nanosecond.Ordinal.OfDay
-- Mathlib.Data.Set.Insert
Set.notMem_singleton_empty : ∀ {α : Type u_1} {s : Set α}, s ∉ {∅} ↔ s.Nonempty
-- Mathlib.CategoryTheory.Opposites
CategoryTheory.Functor.instFaithfulOppositeOp : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  {F : CategoryTheory.Functor C D} [F.Faithful], F.op.Faithful
-- Mathlib.Analysis.Calculus.TangentCone.Real
uniqueDiffWithinAt_Iio : ∀ (a : ℝ), UniqueDiffWithinAt ℝ (Set.Iio a) a
-- Init.Data.SInt.Lemmas
Int8.ofInt_eq_ofNat : ∀ {n : ℕ}, Int8.ofInt ↑n = Int8.ofNat n
-- Mathlib.Tactic.Widget.Conv
/-- Return the text for the link in the conv widget that inserts the replacement,
and also return the replacement, and the range within the file to highlight after the
replacement is inserted. The highlighted range will always be the trailing `skip`.  -/
Mathlib.Tactic.Conv.insertEnter : Array Lean.SubExpr.GoalsLocation →
  Lean.Expr → SelectInsertParams → Lean.MetaM (String × String × Option (String.Pos.Raw × String.Pos.Raw))
-- Mathlib.AlgebraicTopology.SimplexCategory.Augmented.Basic
AugmentedSimplexCategory.equivAugmentedSimplicialObjectFunctorCompToArrowIso_hom_app_right : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C]
  (X : CategoryTheory.Functor AugmentedSimplexCategoryᵒᵖ C),
  (AugmentedSimplexCategory.equivAugmentedSimplicialObjectFunctorCompToArrowIso.hom.app X).right =
    CategoryTheory.CategoryStruct.id (X.obj (Opposite.op CategoryTheory.WithInitial.star))
-- Init.Data.UInt.Lemmas
UInt32.ofBitVec_sub : ∀ (a b : BitVec 32), { toBitVec := a - b } = { toBitVec := a } - { toBitVec := b }
-- Mathlib.CategoryTheory.Localization.FiniteProducts
/-- The (candidate) limit functor for the localized category.
It is induced by `lim ⋙ L : (Discrete J ⥤ C) ⥤ D`.  -/
CategoryTheory.Localization.HasProductsOfShapeAux.limitFunctor : {C : Type u₁} →
  {D : Type u₂} →
    [inst : CategoryTheory.Category.{v₁, u₁} C] →
      [inst_1 : CategoryTheory.Category.{v₂, u₂} D] →
        (L : CategoryTheory.Functor C D) →
          (W : CategoryTheory.MorphismProperty C) →
            [L.IsLocalization W] →
              (J : Type) →
                [CategoryTheory.Limits.HasProductsOfShape J C] →
                  [W.IsStableUnderProductsOfShape J] →
                    [W.ContainsIdentities] →
                      [Finite J] → CategoryTheory.Functor (CategoryTheory.Functor (CategoryTheory.Discrete J) D) D
-- Mathlib.Data.Fin.SuccPred
Fin.predAbove_of_lt_succ : ∀ {n : ℕ} (p : Fin n) (i : Fin (n + 1)) (h : i < p.succ), p.predAbove i = i.castPred ⋯
-- Mathlib.Algebra.Group.Defs
isRightCancelMul_iff : ∀ (G : Type u) [inst : Mul G], IsRightCancelMul G ↔ ∀ (a : G), IsRightRegular a
-- Mathlib.Algebra.Homology.ShortComplex.HomologicalComplex
HomologicalComplex.isoHomologyπ.congr_simp : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  {ι : Type u_2} {c : ComplexShape ι} (K : HomologicalComplex C c) (i i_1 : ι) (e_i : i = i_1) (j : ι)
  (hi : c.prev j = i) (h : K.d i j = 0) [inst_2 : K.HasHomology j], K.isoHomologyπ i j hi h = K.isoHomologyπ i_1 j ⋯ ⋯
-- Lean.Elab.MutualInductive
/-- Auxiliary function for checking whether the types in mutually inductive declaration are compatible.
 -/
_private.Lean.Elab.MutualInductive.0.Lean.Elab.Command.checkHeaders : Array Lean.Elab.Command.PreElabHeaderResult → ℕ → ℕ → Option Lean.Expr → Lean.Elab.TermElabM Unit
-- Mathlib.Combinatorics.Hypergraph.Basic
Hypergraph.not_isNonempty_iff : ∀ {α : Type u_1} {H : Hypergraph α}, ¬H.IsNonempty ↔ H = ⊥
-- Init.Data.Array.Lemmas
Array.getElem_shrink : ∀ {α : Type u_1} {xs : Array α} {i j : ℕ} (h : j < (xs.shrink i).size), (xs.shrink i)[j] = xs[j]
-- Mathlib.Analysis.Calculus.ContDiff.FaaDiBruno
OrderedFinpartition.extend.eq_2 : ∀ {n : ℕ} (c : OrderedFinpartition n) (i_2 : Fin c.length), c.extend (some i_2) = c.extendMiddle i_2
-- Init.Data.String.Lemmas.Pattern.Pred
String.Slice.Pattern.Model.CharPred.Decidable.matchAt?_eq_matchAt?_decide : ∀ {p : Char → Prop} [inst : DecidablePred p] {s : String.Slice} {pos : s.Pos},
  String.Slice.Pattern.Model.matchAt? p pos = String.Slice.Pattern.Model.matchAt? (fun x => decide (p x)) pos
-- Mathlib.AlgebraicGeometry.Birational.Composition
AlgebraicGeometry.Scheme.RationalMap.comp_id : ∀ {X Y : AlgebraicGeometry.Scheme} [inst : PreirreducibleSpace ↥X] [inst_1 : Nonempty ↥Y] (f : X.RationalMap Y)
  [inst_2 : f.IsDominant], f.comp (AlgebraicGeometry.Scheme.RationalMap.id Y) = f
-- Mathlib.Data.Finset.Max
Finset.min_le_of_eq : ∀ {α : Type u_2} [inst : LinearOrder α] {s : Finset α} {a b : α}, b ∈ s → s.min = ↑a → a ≤ b
-- Mathlib.RingTheory.MvPowerSeries.Rename
/-- Given an embedding `e : σ ↪ τ`, `MvPowerSeries.killComplFun e` is the function from
`R⟦τ⟧` to `R⟦σ⟧` that is left inverse to `rename e.injective.fiberFinite : R⟦σ⟧ → R⟦τ⟧`
and sends the variables in the complement of the range of `e` to `0`.  -/
MvPowerSeries.killCompl : {σ : Type u_1} →
  {τ : Type u_2} → {R : Type u_4} → [inst : CommSemiring R] → (σ ↪ τ) → MvPowerSeries τ R →ₐ[R] MvPowerSeries σ R
-- Mathlib.NumberTheory.DiophantineApproximation.Basic
_private.Mathlib.NumberTheory.DiophantineApproximation.Basic.0.Real.aux₃ : ∀ {ξ : ℝ} {u v : ℤ},
  2 ≤ v →
    Real.ContfracLegendre.Ass ξ u v →
      |(Int.fract ξ)⁻¹ - ↑v / (↑u - ↑⌊ξ⌋ * ↑v)| < ((↑u - ↑⌊ξ⌋ * ↑v) * (2 * (↑u - ↑⌊ξ⌋ * ↑v) - 1))⁻¹
-- Mathlib.Dynamics.PeriodicPts.Defs
Function.mem_periodicOrbit_iff : ∀ {α : Type u_1} {f : α → α} {x y : α}, x ∈ Function.periodicPts f → (y ∈ Function.periodicOrbit f x ↔ ∃ n, f^[n] x = y)
-- Lean.Parser.Basic
Lean.Parser.trailingLoop : Lean.Parser.PrattParsingTables → Lean.Parser.ParserContext → Lean.Parser.ParserState → Lean.Parser.ParserState
-- Mathlib.AlgebraicTopology.SimplicialSet.ProdStdSimplex
SSet.prodStdSimplex.strictMono_orderHomOfSimplex : ∀ {p q n : ℕ}
  (x :
    ↑((CategoryTheory.MonoidalCategoryStruct.tensorObj (SSet.stdSimplex.obj { len := p })
            (SSet.stdSimplex.obj { len := q })).nonDegenerate
        n))
  {m : ℕ} (hm : p + q = m), StrictMono ⇑(SSet.prodStdSimplex.orderHomOfSimplex (↑x) hm)
-- Mathlib.Data.Matrix.PEquiv
PEquiv.toMatrix_refl : ∀ {n : Type u_4} {α : Type u_5} [inst : DecidableEq n] [inst_1 : Zero α] [inst_2 : One α], (PEquiv.refl n).toMatrix = 1
-- Mathlib.Analysis.Normed.Group.Uniform
Isometry.norm_map_of_map_one : ∀ {E : Type u_2} {F : Type u_3} [inst : SeminormedGroup E] [inst_1 : SeminormedGroup F] {f : E → F},
  Isometry f → f 1 = 1 → ∀ (x : E), ‖f x‖ = ‖x‖
-- Mathlib.NumberTheory.LSeries.Convergence
/-- If `‖f n‖` is bounded by a constant times `n^x`, then the abscissa of absolute convergence
of `f` is bounded by `x + 1`.  -/
LSeries.abscissaOfAbsConv_le_of_le_const_mul_rpow : ∀ {f : ℕ → ℂ} {x : ℝ}, (∃ C, ∀ (n : ℕ), n ≠ 0 → ‖f n‖ ≤ C * ↑n ^ x) → LSeries.abscissaOfAbsConv f ≤ ↑x + 1
-- Mathlib.LinearAlgebra.TensorProduct.Tower
/-- Heterobasic version of `TensorProduct.lcurry`:

Given a linear map `M ⊗[R] N →[A] P`, compose it with the canonical
bilinear map `M →[A] N →[R] M ⊗[R] N` to form a bilinear map `M →[A] N →[R] P`.  -/
TensorProduct.AlgebraTensorModule.lcurry : (R : Type uR) →
  (A : Type uA) →
    (B : Type uB) →
      (M : Type uM) →
        (N : Type uN) →
          (P : Type uP) →
            [inst : CommSemiring R] →
              [inst_1 : Semiring A] →
                [inst_2 : Semiring B] →
                  [inst_3 : Algebra R A] →
                    [inst_4 : Algebra R B] →
                      [inst_5 : AddCommMonoid M] →
                        [inst_6 : Module R M] →
                          [inst_7 : Module A M] →
                            [inst_8 : IsScalarTower R A M] →
                              [inst_9 : AddCommMonoid N] →
                                [inst_10 : Module R N] →
                                  [inst_11 : AddCommMonoid P] →
                                    [inst_12 : Module R P] →
                                      [inst_13 : Module A P] →
                                        [inst_14 : IsScalarTower R A P] →
                                          [inst_15 : Module B P] →
                                            [inst_16 : IsScalarTower R B P] →
                                              [inst_17 : SMulCommClass A B P] →
                                                (TensorProduct R M N →ₗ[A] P) →ₗ[B] M →ₗ[A] N →ₗ[R] P
-- Mathlib.Analysis.Calculus.FDeriv.Symmetric
second_derivative_symmetric_of_eventually : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} {F : Type u_3} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F] {f : E → F}
  [IsRCLikeNormedField 𝕜] {f' : E → E →L[𝕜] F} {x : E} {f'' : E →L[𝕜] E →L[𝕜] F},
  (∀ᶠ (y : E) in nhds x, HasFDerivAt f (f' y) y) → HasFDerivAt f' f'' x → ∀ (v w : E), (f'' v) w = (f'' w) v
-- Mathlib.Topology.EMetricSpace.Lipschitz
/-- `f : α → β` is called **locally Lipschitz continuous** iff every point `x`
has a neighbourhood on which `f` is Lipschitz.  -/
LocallyLipschitz : {α : Type u} → {β : Type v} → [PseudoEMetricSpace α] → [PseudoEMetricSpace β] → (α → β) → Prop
-- Init.Data.Int.DivMod.Lemmas
Int.tdiv.eq_1 : ∀ (m n : ℕ), (Int.ofNat m).tdiv (Int.ofNat n) = Int.ofNat (m / n)
-- Lean.Meta.Tactic.Simp.SimpAll
Lean.Meta.simpAll : Lean.MVarId →
  Lean.Meta.Simp.Context →
    optParam Lean.Meta.Simp.SimprocsArray #[] →
      optParam Lean.Meta.Simp.Stats { } → Lean.MetaM (Option Lean.MVarId × Lean.Meta.Simp.Stats)
-- Mathlib.CategoryTheory.Limits.Creates
/-- If `F` creates limits and `F ≅ G`, then `G` creates limits.  -/
CategoryTheory.createsLimitsOfNatIso : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    {D : Type u₂} →
      [inst_1 : CategoryTheory.Category.{v₂, u₂} D] →
        {F G : CategoryTheory.Functor C D} →
          (F ≅ G) →
            [CategoryTheory.CreatesLimitsOfSize.{w, w', v₁, v₂, u₁, u₂} F] →
              CategoryTheory.CreatesLimitsOfSize.{w, w', v₁, v₂, u₁, u₂} G
-- Std.Time.Format.Modifier
/-- `classify` classifies the number of pattern letters into a `ZoneId` format.
- If 1 letter, it returns the unknown form.
- If 2 letters, it returns the short form.
- If 4 letters, it returns the full form.
- Otherwise, it returns none.
 -/
Std.Time.ZoneId.classify : ℕ → Option Std.Time.ZoneId
-- Mathlib.CategoryTheory.Category.Cat.CartesianClosed
CategoryTheory.Cat.exp_map : ∀ (C : Type u) [inst : CategoryTheory.Category.{v, u} C] {X Y : CategoryTheory.Cat} (F : X ⟶ Y),
  (CategoryTheory.Cat.exp C).map F = ((CategoryTheory.Functor.whiskeringRight C ↑X ↑Y).obj F.toFunctor).toCatHom
-- Mathlib.Algebra.Tropical.Basic
Tropical.trop_untrop : ∀ {R : Type u} (x : Tropical R), Tropical.trop (Tropical.untrop x) = x
-- Mathlib.Order.Basic
Prod.mk_le_mk : ∀ {α : Type u_2} {β : Type u_3} [inst : LE α] [inst_1 : LE β] {a₁ a₂ : α} {b₁ b₂ : β},
  (a₁, b₁) ≤ (a₂, b₂) ↔ a₁ ≤ a₂ ∧ b₁ ≤ b₂
-- Lean.PrettyPrinter.Parenthesizer
Lean.PrettyPrinter.Parenthesizer.withoutInfo.parenthesizer : Lean.PrettyPrinter.Parenthesizer → Lean.PrettyPrinter.Parenthesizer
-- Batteries.Data.String.Matcher
/-- Find all substrings of `s` matching `m.pattern`.  -/
String.Matcher.findAll : String.Matcher → Substring.Raw → Array Substring.Raw
-- Mathlib.AlgebraicGeometry.Cover.MorphismProperty
/-- A coverage `K` on `Scheme` is called jointly surjective if every covering family in `K`
is jointly surjective.  -/
AlgebraicGeometry.Scheme.JointlySurjective : CategoryTheory.Precoverage AlgebraicGeometry.Scheme → Prop
-- Lean.LocalContext
Lean.LocalContext.usesUserName : Lean.LocalContext → Lean.Name → Bool
-- Mathlib.Algebra.Order.Ring.Archimedean
ArchimedeanClass.instLinearOrderedAddCommMonoidWithTop : {R : Type u_1} →
  [inst : LinearOrder R] →
    [inst_1 : CommRing R] → [inst_2 : IsStrictOrderedRing R] → LinearOrderedAddCommMonoidWithTop (ArchimedeanClass R)
-- Aesop.Util.Basic
/-- A generalized variant of `Meta.SavedState.runMetaM`  -/
Aesop.runInMetaState : {m : Type → Type u_1} →
  {α : Type} → [Monad m] → [MonadLiftT Lean.MetaM m] → [MonadFinally m] → Lean.Meta.SavedState → m α → m α
-- Mathlib.Analysis.Real.Hyperreal
Hyperreal.st_le_of_le : ∀ {x y : ℝ*}, ¬x.Infinite → ¬y.Infinite → x ≤ y → x.st ≤ y.st
-- Mathlib.FieldTheory.RatFunc.Basic
RatFunc.denom_zero : ∀ {K : Type u} [inst : Field K], RatFunc.denom 0 = 1
-- Mathlib.RingTheory.Perfection
ModP.v_p_lt_val : ∀ {K : Type u₁} [inst : Field K] {v : Valuation K NNReal} {O : Type u₂} [inst_1 : CommRing O] [inst_2 : Algebra O K],
  v.Integers O → ∀ {p : ℕ} {x : O}, v ↑p < v ((algebraMap O K) x) ↔ (Ideal.Quotient.mk (Ideal.span {↑p})) x ≠ 0
-- Std.Data.TreeSet.Lemmas
Std.TreeSet.size_inter_eq_size_right : ∀ {α : Type u} {cmp : α → α → Ordering} {t₁ t₂ : Std.TreeSet α cmp} [Std.TransCmp cmp],
  (∀ a ∈ t₂, a ∈ t₁) → (t₁ ∩ t₂).size = t₂.size
-- Lean.Environment
Lean.ConstantKind.axiom.sizeOf_spec : sizeOf Lean.ConstantKind.axiom = 1
-- Mathlib.Algebra.Lie.Extension
LieAlgebra.of_symm_add : ∀ {R : Type u_1} {L : Type u_3} {M : Type u_4} [inst : CommRing R] [inst_1 : LieRing L] [inst_2 : LieAlgebra R L]
  [inst_3 : AddCommGroup M] [inst_4 : Module R M] [inst_5 : LieRingModule L M] [inst_6 : LieModule R L M]
  (c : ↥(LieModule.Cohomology.twoCocycle R L M)) (x y : LieAlgebra.ofTwoCocycle c),
  (LieAlgebra.ofProd c).symm (x + y) = (LieAlgebra.ofProd c).symm x + (LieAlgebra.ofProd c).symm y
-- Mathlib.NumberTheory.LucasLehmer
_private.Mathlib.NumberTheory.LucasLehmer.0.LucasLehmer.norm_num_ext.sModNatTR.go.eq_1 : ∀ (q a : ℕ), LucasLehmer.norm_num_ext.sModNatTR.go✝ q 0 a = a
-- Mathlib.MeasureTheory.Integral.Bochner.Set
MeasureTheory.setIntegral_nonneg_of_ae : ∀ {X : Type u_1} {mX : MeasurableSpace X} {μ : MeasureTheory.Measure X} {f : X → ℝ} {s : Set X},
  0 ≤ᵐ[μ] f → 0 ≤ ∫ (x : X) in s, f x ∂μ
-- Mathlib.Algebra.BigOperators.Fin
List.alternatingSum.eq_2 : ∀ {G : Type u_4} [inst : Zero G] [inst_1 : Add G] [inst_2 : Neg G] (g : G), [g].alternatingSum = g
-- Mathlib.Tactic.Abel
/-- `abel` solves equations in the language of *additive*, commutative monoids and groups.

`abel` and its variants work as both tactics and conv tactics.

* `abel1` fails if the target is not an equality that is provable by the axioms of
  commutative monoids/groups.
* `abel_nf` rewrites all group expressions into a normal form.
  * `abel_nf at h` rewrites in a hypothesis.
  * `abel_nf (config := cfg)` allows for additional configuration:
    * `red`: the reducibility setting (overridden by `!`).
    * `zetaDelta`: if true, local `let` variables can be unfolded (overridden by `!`).
    * `recursive`: if true, `abel_nf` also recurses into atoms.
* `abel!`, `abel1!`, `abel_nf!` use a more aggressive reducibility setting to identify atoms.

Examples:
```
example [AddCommMonoid α] (a b : α) : a + (b + a) = a + a + b := by abel
example [AddCommGroup α] (a : α) : (3 : ℤ) • a = a + (2 : ℤ) • a := by abel
```
 -/
Mathlib.Tactic.Abel.convAbel_nf!_ : Lean.ParserDescr
-- Init.Data.Bool
Bool.cond_then_not_self : ∀ (c b : Bool), (bif c then !c else b) = (!c && b)
-- Mathlib.Combinatorics.Enumerative.Composition
Composition.sizeUpTo_zero : ∀ {n : ℕ} (c : Composition n), c.sizeUpTo 0 = 0
-- Mathlib.RingTheory.RingHom.Flat
RingHom.Flat.of_isField : ∀ {R : Type u_1} {S : Type u_2} [inst : CommRing R] [inst_1 : CommRing S], IsField R → ∀ (f : R →+* S), f.Flat
-- Mathlib.FieldTheory.Separable
Algebra.isSeparable_iff : ∀ {F : Type u_1} {K : Type u_3} [inst : CommRing F] [inst_1 : Ring K] [inst_2 : Algebra F K],
  Algebra.IsSeparable F K ↔ ∀ (x : K), IsIntegral F x ∧ IsSeparable F x
-- Mathlib.Algebra.Group.WithOne.Defs
WithOne.one_ne_coe : ∀ {α : Type u} {a : α}, 1 ≠ ↑a
-- Mathlib.Algebra.Group.Action.Pointwise.Set.Basic
Set.image_smul_distrib : ∀ {F : Type u_1} {α : Type u_2} {β : Type u_3} [inst : Mul α] [inst_1 : Mul β] [inst_2 : FunLike F α β]
  [MulHomClass F α β] (f : F) (a : α) (s : Set α), ⇑f '' (a • s) = f a • ⇑f '' s
-- Lean.DocString.Syntax
Lean.Doc.Syntax.text : Lean.ParserDescr
-- Mathlib.CategoryTheory.Limits.Shapes.BinaryBiproducts
/-- A cokernel cofork for the cokernel of `biprod.inr`. It consists of the
morphism `biprod.fst`.  -/
CategoryTheory.Limits.biprod.inrCokernelCofork : {C : Type uC} →
  [inst : CategoryTheory.Category.{uC', uC} C] →
    [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C] →
      (X Y : C) →
        [inst_2 : CategoryTheory.Limits.HasBinaryBiproduct X Y] →
          CategoryTheory.Limits.CokernelCofork CategoryTheory.Limits.biprod.inr
-- Mathlib.Data.ENNReal.Inv
ENNReal.mul_inv : ∀ {a b : ENNReal}, a ≠ 0 ∨ b ≠ ⊤ → a ≠ ⊤ ∨ b ≠ 0 → (a * b)⁻¹ = a⁻¹ * b⁻¹
-- Init.Grind.Offset
Lean.Grind.Nat.le_eq_true_of_lo : ∀ (u v k : ℕ), u + k ≤ v → (u ≤ v) = True