mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.MeasureTheory.Group.Arithmetic
AEMeasurable.fun_neg : ∀ {G : Type u_2} {α : Type u_3} [inst : Neg G] [inst_1 : MeasurableSpace G] [MeasurableNeg G] {m : MeasurableSpace α}
  {f : α → G} {μ : MeasureTheory.Measure α}, AEMeasurable f μ → AEMeasurable (fun i => -f i) μ
-- Mathlib.CategoryTheory.SmallObject.IsCardinalForSmallObjectArgument
CategoryTheory.SmallObject.hasPushouts : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] (I : CategoryTheory.MorphismProperty C) (κ : Cardinal.{w})
  [inst_1 : Fact κ.IsRegular] [inst_2 : OrderBot κ.ord.ToType] [I.IsCardinalForSmallObjectArgument κ],
  CategoryTheory.Limits.HasPushouts C
-- Mathlib.Algebra.Group.Subgroup.MulOppositeLemmas
AddSubgroup.op.instNormal : ∀ {G : Type u_2} [inst : AddGroup G] {H : AddSubgroup G} [H.Normal], H.op.Normal
-- Mathlib.LinearAlgebra.SesquilinearForm.Basic
LinearMap.BilinForm.apply_apply_same_eq_zero_iff : ∀ {R : Type u_1} {M : Type u_5} [inst : CommRing R] [inst_1 : LinearOrder R] [IsStrictOrderedRing R]
  [inst_3 : AddCommGroup M] [inst_4 : Module R M] (B : LinearMap.BilinForm R M),
  (∀ (x : M), 0 ≤ (B x) x) → LinearMap.IsSymm B → ∀ {x : M}, (B x) x = 0 ↔ x ∈ LinearMap.ker B
-- Mathlib.Analysis.Analytic.Composition
/-- **Alias** of `AnalyticAt.fun_comp_of_eq`.

---

Eta-expanded form of `AnalyticAt.comp_of_eq`

---

Version of `AnalyticAt.comp` where point equality is a separate hypothesis.  -/
AnalyticAt.comp_of_eq' : ∀ {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} {G : Type u_4} [inst : NontriviallyNormedField 𝕜]
  [inst_1 : NormedAddCommGroup E] [inst_2 : NormedSpace 𝕜 E] [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F]
  [inst_5 : NormedAddCommGroup G] [inst_6 : NormedSpace 𝕜 G] {g : F → G} {f : E → F} {y : F} {x : E},
  AnalyticAt 𝕜 g y → AnalyticAt 𝕜 f x → f x = y → AnalyticAt 𝕜 (fun x => g (f x)) x
-- Mathlib.Logic.Equiv.Basic
Equiv.piCongr'.eq_1 : ∀ {α : Sort u_1} {β : Sort u_4} {W : α → Sort w} {Z : β → Sort z} (h₁ : α ≃ β) (h₂ : (b : β) → W (h₁.symm b) ≃ Z b),
  h₁.piCongr' h₂ = (h₁.symm.piCongr fun b => (h₂ b).symm).symm
-- Mathlib.CategoryTheory.Bicategory.Strict.Pseudofunctor
CategoryTheory.LaxFunctor.mapComp'.congr_simp : ∀ {B : Type u₁} [inst : CategoryTheory.Bicategory B] {C : Type u₂} [inst_1 : CategoryTheory.Bicategory C]
  (F : CategoryTheory.LaxFunctor B C) {b₀ b₁ b₂ : B} (f : b₀ ⟶ b₁) (g : b₁ ⟶ b₂) (fg : b₀ ⟶ b₂)
  (h : CategoryTheory.CategoryStruct.comp f g = fg), F.mapComp' f g fg h = F.mapComp' f g fg h
-- Init.Data.Fin.Lemmas
Fin.cast_addNat : ∀ {n : ℕ} (m : ℕ) (i : Fin n), Fin.cast ⋯ (i.addNat m) = Fin.natAdd m i
-- Mathlib.CategoryTheory.Triangulated.Opposite.Pretriangulated
CategoryTheory.Limits.IsZero.iso.congr_simp : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {X Y : C} (hX : CategoryTheory.Limits.IsZero X)
  (hY : CategoryTheory.Limits.IsZero Y), hX.iso hY = hX.iso hY
-- Mathlib.CategoryTheory.Shift.CommShiftTwo
CategoryTheory.Functor.CommShift₂.commShiftObj : {C₁ : Type u_1} →
  {C₂ : Type u_3} →
    {D : Type u_5} →
      {inst : CategoryTheory.Category.{v_1, u_1} C₁} →
        {inst_1 : CategoryTheory.Category.{v_3, u_3} C₂} →
          {inst_2 : CategoryTheory.Category.{v_5, u_5} D} →
            {M : Type u_6} →
              {inst_3 : AddCommMonoid M} →
                {inst_4 : CategoryTheory.HasShift C₁ M} →
                  {inst_5 : CategoryTheory.HasShift C₂ M} →
                    {inst_6 : CategoryTheory.HasShift D M} →
                      {G : CategoryTheory.Functor C₁ (CategoryTheory.Functor C₂ D)} →
                        (h : CategoryTheory.CommShift₂Setup D M) →
                          [self : G.CommShift₂ h] → (X₁ : C₁) → (G.obj X₁).CommShift M
-- Mathlib.Data.List.Duplicate
List.nodup_iff_forall_not_duplicate : ∀ {α : Type u_1} {l : List α}, l.Nodup ↔ ∀ (x : α), ¬List.Duplicate x l
-- Init.Data.Int.Linear
_private.Init.Data.Int.Linear.0.Int.Internal.Linear.mul_eq_zero_iff : ∀ (a k : ℤ), k > 0 → (k * a = 0 ↔ a = 0)
-- Mathlib.Data.Multiset.AddSub
Multiset.le_iff_exists_add : ∀ {α : Type u_1} {s t : Multiset α}, s ≤ t ↔ ∃ u, t = s + u
-- Lean.Declaration
/-- Number of auxiliary data types produced from nested occurrences.
An inductive definition `T` is nested when there is a constructor with an argument `x : F T`,
 where `F : Type → Type` is some suitably behaved (ie strictly positive) function (Eg `Array T`, `List T`, `T × T`, ...).   -/
Lean.InductiveVal.numNested : Lean.InductiveVal → ℕ
-- Batteries.Recycling.RBTree.WF
/-- The `balance2` function does nothing if the second argument is already balanced.  -/
RBTree.RBNode.balance2_eq : ∀ {α : Type u_1} {c : RBTree.RBColor} {n : ℕ} {l : RBTree.RBNode α} {v : α} {r : RBTree.RBNode α},
  r.Balanced c n → l.balance2 v r = RBTree.RBNode.node RBTree.RBColor.black l v r
-- Mathlib.Algebra.Homology.DerivedCategory.DerivabilityStructureInjectives
HomotopyCategory.Plus.quasiIso.eq_1 : ∀ (A : Type u_3) [inst : CategoryTheory.Category.{v_3, u_3} A] [inst_1 : CategoryTheory.Abelian A],
  HomotopyCategory.Plus.quasiIso A =
    (HomotopyCategory.quasiIso A (ComplexShape.up ℤ)).inverseImage (HomotopyCategory.Plus.ι A)
-- Std.Data.TreeMap.Raw.Lemmas
Std.TreeMap.Raw.insertMany_list_equiv_foldl : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t₁ : Std.TreeMap.Raw α β cmp} {l : List (α × β)},
  (t₁.insertMany l).Equiv (List.foldl (fun acc p => acc.insert p.1 p.2) t₁ l)
-- Mathlib.Algebra.Order.Ring.Canonical
AddLECancellable.tsub_mul : ∀ {R : Type u} [inst : NonUnitalNonAssocSemiring R] [inst_1 : PartialOrder R] [CanonicallyOrderedAdd R] [inst_3 : Sub R]
  [OrderedSub R] [Std.Total fun x1 x2 => x1 ≤ x2] [MulRightMono R] {a b c : R},
  AddLECancellable (b * c) → (a - b) * c = a * c - b * c
-- Mathlib.CategoryTheory.Generator.Basic
/-- Given `P : ObjectProperty C` and `X : C`, this is the product of
all the morphisms `X ⟶ Y` such that `P Y` holds.  -/
CategoryTheory.ObjectProperty.productTo : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    (P : CategoryTheory.ObjectProperty C) →
      (X : C) → [inst_1 : CategoryTheory.Limits.HasProduct (P.productToFamily X)] → X ⟶ ∏ᶜ P.productToFamily X
-- Std.Tactic.BVDecide.Normalize.BitVec
Std.Tactic.BVDecide.Normalize.BitVec.ult_max' : ∀ {w : ℕ} (a : BitVec w), a.ult (-1#w) = !a == -1#w
-- Mathlib.Data.Nat.PSub
/-- Partial predecessor operation. Returns `ppred n = some m`
if `n = m + 1`, otherwise `none`.  -/
Nat.ppred : ℕ → Option ℕ
-- Mathlib.Algebra.Polynomial.Taylor
Polynomial.exists_mul_sq_add_linear_part_eq_eval_add : ∀ {R : Type u_1} [inst : CommSemiring R] (p : Polynomial R) (x y : R),
  ∃ c, c * y ^ 2 + Polynomial.eval x (Polynomial.derivative p) * y + Polynomial.eval x p = Polynomial.eval (x + y) p
-- Init.Data.String.Lemmas.Pattern.TakeDrop.String
String.startsWith_slice_iff : ∀ {pat : String.Slice} {s : String}, s.startsWith pat = true ↔ pat.copy.toList <+: s.toList
-- Mathlib.Algebra.Module.Submodule.Lattice
Submodule.coe_finsetInf : ∀ {R : Type u_1} {M : Type u_3} [inst : Semiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M] {ι : Type u_4}
  (s : Finset ι) (p : ι → Submodule R M), ↑(s.inf p) = ⋂ i ∈ s, ↑(p i)
-- Mathlib.Combinatorics.Matroid.Closure
Matroid.Indep.mem_closure_iff' : ∀ {α : Type u_2} {M : Matroid α} {I : Set α} {x : α},
  M.Indep I → (x ∈ M.closure I ↔ x ∈ M.E ∧ (M.Indep (insert x I) → x ∈ I))
-- Mathlib.Analysis.SpecialFunctions.Integrability.LogMeromorphic
/-- **Alias** of `MeromorphicOn.intervalIntegrable_log_norm`.

---

If `f` is real-meromorphic on a compact interval, then `log ‖f ·‖` is interval integrable on this
interval.
 -/
intervalIntegrable_log_norm_meromorphicOn : ∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] {f : ℝ → E} {a b : ℝ},
  MeromorphicOn f (Set.uIcc a b) → IntervalIntegrable (fun x => Real.log ‖f x‖) MeasureTheory.volume a b
-- Mathlib.Topology.VectorBundle.Basic
VectorBundleCore.coordChange : {R : Type u_1} →
  {B : Type u_2} →
    {F : Type u_3} →
      [inst : NontriviallyNormedField R] →
        [inst_1 : NormedAddCommGroup F] →
          [inst_2 : NormedSpace R F] →
            [inst_3 : TopologicalSpace B] → {ι : Type u_5} → VectorBundleCore R B F ι → ι → ι → B → F →L[R] F
-- Mathlib.Data.List.Cycle
Cycle.length_nil : ∀ {α : Type u_1}, Cycle.nil.length = 0
-- Lean.Compiler.IR.Basic
Lean.IR.CtorInfo.mk.inj : ∀ {name : Lean.Name} {cidx size usize ssize : ℕ} {name_1 : Lean.Name} {cidx_1 size_1 usize_1 ssize_1 : ℕ},
  { name := name, cidx := cidx, size := size, usize := usize, ssize := ssize } =
      { name := name_1, cidx := cidx_1, size := size_1, usize := usize_1, ssize := ssize_1 } →
    name = name_1 ∧ cidx = cidx_1 ∧ size = size_1 ∧ usize = usize_1 ∧ ssize = ssize_1
-- Mathlib.GroupTheory.Coxeter.Length
CoxeterSystem.length_eq_one_iff : ∀ {B : Type u_1} {W : Type u_2} [inst : Group W] {M : CoxeterMatrix B} (cs : CoxeterSystem M W) {w : W},
  cs.length w = 1 ↔ ∃ i, w = cs.simple i
-- Std.Internal.Do.WP.Basic
/-- Weakest precondition monad: a monad `m` whose weakest precondition interpretation is sound for
`pure` and `bind`. The interpretation for every result type is carried as the `toWP` field; an
instance exposes it as a `WP (m α) …` interpretation.  -/
Std.Internal.Do.WPMonad : (m : Type u → Type v) →
  (Pred : outParam (Type w)) →
    (EPred : outParam (Type w')) →
      [Monad m] →
        [Std.Internal.Do.Assertion Pred] → [Std.Internal.Do.Assertion EPred] → Type (max (max (max (u + 1) v) w) w')
-- Mathlib.Algebra.Group.Action.Pretransitive
Multiplicative.mulAction_isPretransitive : ∀ {α : Type u_3} {β : Type u_4} [inst : AddMonoid α] [inst_1 : AddAction α β] [AddAction.IsPretransitive α β],
  MulAction.IsPretransitive (Multiplicative α) β
-- Init.Control.Lawful.MonadAttach.Lemmas
LawfulMonadAttach.eq_of_canReturn_pure : ∀ {m : Type u_1 → Type u_2} {α : Type u_1} [inst : Monad m] [inst_1 : MonadAttach m] [LawfulMonad m]
  [LawfulMonadAttach m] {a b : α}, MonadAttach.CanReturn (pure a) b → a = b
-- Mathlib.MeasureTheory.Integral.Prod
MeasureTheory.integral_prod_swap : ∀ {α : Type u_1} {β : Type u_2} {E : Type u_3} [inst : MeasurableSpace α] [inst_1 : MeasurableSpace β]
  {μ : MeasureTheory.Measure α} {ν : MeasureTheory.Measure β} [inst_2 : NormedAddCommGroup E] [MeasureTheory.SFinite ν]
  [inst_4 : NormedSpace ℝ E] [MeasureTheory.SFinite μ] (f : α × β → E),
  ∫ (z : β × α), f z.swap ∂ν.prod μ = ∫ (z : α × β), f z ∂μ.prod ν
-- Mathlib.Tactic.Linarith.Datatypes
/-- `c.scale n` scales the coefficients of `c` by `n`.  -/
Mathlib.Tactic.Linarith.Comp.scale : Mathlib.Tactic.Linarith.Comp → ℕ → Mathlib.Tactic.Linarith.Comp
-- Lean.ScopedEnvExtension
Lean.ScopedEnvExtension.ScopedEntries.mk.injEq : ∀ {β : Type} (map map_1 : Lean.SMap Lean.Name (Lean.PArray β)), ({ map := map } = { map := map_1 }) = (map = map_1)
-- Mathlib.Algebra.Order.Monoid.Unbundled.Basic
mul_le_of_mul_le_left : ∀ {α : Type u_1} [inst : Mul α] [inst_1 : Preorder α] [MulLeftMono α] {a b c d : α}, a * b ≤ c → d ≤ b → a * d ≤ c
-- Mathlib.AlgebraicTopology.SimplicialSet.AnodyneExtensions.PushoutProduct
SSet.anodyneExtensions.whiskerRight : ∀ {X Y : SSet} {f : X ⟶ Y},
  SSet.anodyneExtensions f →
    ∀ (Z : SSet), SSet.anodyneExtensions (CategoryTheory.MonoidalCategoryStruct.whiskerRight f Z)
-- Mathlib.CategoryTheory.Sites.Pullback
CategoryTheory.Functor.sheafPullbackConstruction.preservesFiniteLimits : ∀ {C : Type u₂} [inst : CategoryTheory.Category.{v₂, u₂} C] {D : Type u₃} [inst_1 : CategoryTheory.Category.{v₃, u₃} D]
  (G : CategoryTheory.Functor C D) (A : Type u₁) [inst_2 : CategoryTheory.Category.{v₁, u₁} A]
  (J : CategoryTheory.GrothendieckTopology C) (K : CategoryTheory.GrothendieckTopology D) [inst_3 : G.IsContinuous J K]
  [inst_4 : ∀ (F : CategoryTheory.Functor Cᵒᵖ A), G.op.HasLeftKanExtension F] [inst_5 : CategoryTheory.HasSheafify K A]
  [CategoryTheory.HasSheafify J A] [CategoryTheory.Limits.PreservesFiniteLimits G.op.lan],
  CategoryTheory.Limits.PreservesFiniteLimits (G.sheafPullback A J K)
-- Mathlib.Algebra.Group.Basic
div_div_eq_mul_div : ∀ {α : Type u_1} [inst : DivisionMonoid α] (a b c : α), a / (b / c) = a * c / b
-- Mathlib.Order.Hom.Basic
/-- An order isomorphism between the domains and codomains of two prosets of
order homomorphisms gives an order isomorphism between the two function prosets.  -/
OrderIso.arrowCongr : {α : Type u_6} →
  {β : Type u_7} →
    {γ : Type u_8} →
      {δ : Type u_9} →
        [inst : Preorder α] →
          [inst_1 : Preorder β] → [inst_2 : Preorder γ] → [inst_3 : Preorder δ] → α ≃o γ → β ≃o δ → (α →o β) ≃o (γ →o δ)
-- Mathlib.RingTheory.GradedAlgebra.Homogeneous.Subsemiring
HomogeneousSubsemiring.ext : ∀ {ι : Type u_1} {σ : Type u_2} {A : Type u_3} [inst : AddMonoid ι] [inst_1 : Semiring A] [inst_2 : SetLike σ A]
  [inst_3 : AddSubmonoidClass σ A] {𝒜 : ι → σ} [inst_4 : DecidableEq ι] [inst_5 : GradedRing 𝒜]
  {R S : HomogeneousSubsemiring 𝒜}, R.toSubsemiring = S.toSubsemiring → R = S
-- Mathlib.FieldTheory.PurelyInseparable.PerfectClosure
/-- If `E / F` is separable, then the perfect closure of `F` in `E` is equal to `F`. Note that
the converse is not necessarily true (see https://math.stackexchange.com/a/3009197)
even when `E / F` is algebraic.  -/
perfectClosure.eq_bot_of_isSeparable : ∀ (F : Type u) (E : Type v) [inst : Field F] [inst_1 : Field E] [inst_2 : Algebra F E] [Algebra.IsSeparable F E],
  perfectClosure F E = ⊥
-- Lean.Data.Lsp.LanguageFeatures
Lean.Lsp.instHashableInsertReplaceEdit.hash : Lean.Lsp.InsertReplaceEdit → UInt64
-- Aesop.RuleTac.Descr
Aesop.instInhabitedRuleTacDescr.default : Aesop.RuleTacDescr
-- Mathlib.Data.Int.Fib.Basic
Int.fib_neg_one : Int.fib (-1) = 1
-- Mathlib.NumberTheory.NumberField.InfinitePlace.TotallyRealComplex
NumberField.instIsAlgebraicSubtypeMemSubfield : ∀ {K : Type u_2} [inst : Field K] [inst_1 : CharZero K] [Algebra.IsAlgebraic ℚ K] (k : Subfield K),
  Algebra.IsAlgebraic (↥k) K
-- Mathlib.MeasureTheory.Measure.WithDensity
MeasureTheory.setLIntegral_withDensity_eq_lintegral_mul₀ : ∀ {α : Type u_1} {m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} {f : α → ENNReal},
  AEMeasurable f μ →
    ∀ {g : α → ENNReal},
      AEMeasurable g μ →
        ∀ {s : Set α}, MeasurableSet s → ∫⁻ (a : α) in s, g a ∂μ.withDensity f = ∫⁻ (a : α) in s, (f * g) a ∂μ
-- Mathlib.Data.Set.Prod
Set.graphOn_singleton : ∀ {α : Type u_1} {β : Type u_2} (f : α → β) (x : α), Set.graphOn f {x} = {(x, f x)}
-- Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.NonUnital
/-- The composition of `cfcₙHom` with the natural embedding `C(s, R)₀ → C(quasispectrum R a, R)₀`
whenever `quasispectrum R a ⊆ s`.

This is sometimes necessary in order to consider the same continuous functions applied to multiple
distinct elements, with the added constraint that `cfcₙ` does not suffice. This can occur, for
example, if it is necessary to use uniqueness of this continuous functional calculus. A practical
example can be found in the proof of `CFC.posPart_negPart_unique`.  -/
cfcₙHomSuperset : {R : Type u_1} →
  {A : Type u_2} →
    {p : A → Prop} →
      [inst : CommSemiring R] →
        [inst_1 : Nontrivial R] →
          [inst_2 : StarRing R] →
            [inst_3 : MetricSpace R] →
              [inst_4 : IsTopologicalSemiring R] →
                [inst_5 : ContinuousStar R] →
                  [inst_6 : NonUnitalRing A] →
                    [inst_7 : StarRing A] →
                      [inst_8 : TopologicalSpace A] →
                        [inst_9 : Module R A] →
                          [inst_10 : IsScalarTower R A A] →
                            [inst_11 : SMulCommClass R A A] →
                              [instCFCₙ : NonUnitalContinuousFunctionalCalculus R A p] →
                                {a : A} →
                                  p a → {s : Set R} → (hs : quasispectrum R a ⊆ s) → ContinuousMapZero (↑s) R →⋆ₙₐ[R] A
-- Init.Data.String.Lemmas.Splits
String.Slice.copy_slice_eq_iff_splits : ∀ {t : String} {s : String.Slice} {pos₁ pos₂ : s.Pos},
  (∃ (h : pos₁ ≤ pos₂), (s.slice pos₁ pos₂ h).copy = t) ↔ ∃ t₁ t₂, pos₁.Splits t₁ (t ++ t₂) ∧ pos₂.Splits (t₁ ++ t) t₂
-- Mathlib.Algebra.Ring.BooleanRing
instInhabitedAsBoolRing : {α : Type u_1} → [Inhabited α] → Inhabited (AsBoolRing α)
-- Mathlib.Algebra.BigOperators.Fin
Fin.partialProd.eq_1 : ∀ {M : Type u_2} [inst : Monoid M] {n : ℕ} (f : Fin n → M) (i : Fin (n + 1)),
  Fin.partialProd f i = (List.take (↑i) (List.ofFn f)).prod
-- Mathlib.Algebra.ContinuedFractions.ConvergentsEquiv
/-- The auxiliary continuants before the squashed position stay the same.  -/
GenContFract.contsAux_eq_contsAux_squashGCF_of_le : ∀ {K : Type u_1} {n : ℕ} {g : GenContFract K} [inst : DivisionRing K] {m : ℕ},
  m ≤ n → g.contsAux m = (g.squashGCF n).contsAux m
-- Init.Data.Nat.Internal.Linear
_private.Init.Data.Nat.Internal.Linear.0.Nat.Internal.Linear.Poly.isZero.match_1.eq_1 : ∀ (motive : Nat.Internal.Linear.Poly → Sort u_1) (h_1 : Unit → motive [])
  (h_2 : (x : Nat.Internal.Linear.Poly) → motive x),
  (match [] with
    | [] => h_1 ()
    | x => h_2 x) =
    h_1 ()
-- Mathlib.Analysis.InnerProductSpace.TensorProduct
/-- This is the natural linear isometric equivalence induced by `f : E ≃ₗᵢ F`.  -/
LinearIsometryEquiv.rTensor : {𝕜 : Type u_1} →
  {E : Type u_2} →
    {F : Type u_3} →
      (G : Type u_4) →
        [inst : RCLike 𝕜] →
          [inst_1 : NormedAddCommGroup E] →
            [inst_2 : InnerProductSpace 𝕜 E] →
              [inst_3 : NormedAddCommGroup F] →
                [inst_4 : InnerProductSpace 𝕜 F] →
                  [inst_5 : NormedAddCommGroup G] →
                    [inst_6 : InnerProductSpace 𝕜 G] → (E ≃ₗᵢ[𝕜] F) → TensorProduct 𝕜 E G ≃ₗᵢ[𝕜] TensorProduct 𝕜 F G
-- Mathlib.Order.Fin.Basic
Fin.rev_anti : ∀ {n : ℕ}, Antitone Fin.rev
-- Mathlib.LinearAlgebra.LinearIndependent.Lemmas
/-- **Alias** of `linearIndependent_finSucc`. -/
linearIndependent_fin_succ : ∀ {K : Type u_3} {V : Type u} [inst : DivisionRing K] [inst_1 : AddCommGroup V] [inst_2 : Module K V] {n : ℕ}
  {v : Fin (n + 1) → V},
  LinearIndependent K v ↔ LinearIndependent K (Fin.tail v) ∧ v 0 ∉ Submodule.span K (Set.range (Fin.tail v))
-- Lean.Meta.Tactic.Grind.Arith.ModelUtil
/-- If the given trace class is enabled, trace the model using the class.  -/
Lean.Meta.Grind.Arith.traceModel : Lean.Name → Array (Lean.Expr × ℚ) → Lean.MetaM Unit
-- Mathlib.NumberTheory.Height.Basic
/-- The "local" version of the height bound for arbitrary sums for general (possibly archimedean)
absolute values.  -/
Finset.max_abv_sum_one_le : ∀ {R : Type u_1} {S : Type u_2} [inst : Semiring R] [inst_1 : CommSemiring S] [inst_2 : LinearOrder S] [IsOrderedRing S]
  [CharZero S] (v : AbsoluteValue R S) {ι : Type u_3} {s : Finset ι},
  s.Nonempty → ∀ (x : ι → R), max (v (∑ i ∈ s, x i)) 1 ≤ ↑s.card * ∏ i ∈ s, max (v (x i)) 1
-- Mathlib.LinearAlgebra.AffineSpace.AffineSubspace.Defs
/-- A set is contained in its affine span.  -/
subset_affineSpan : ∀ (k : Type u_1) {V : Type u_2} {P : Type u_3} [inst : Ring k] [inst_1 : AddCommGroup V] [inst_2 : Module k V]
  [inst_3 : AddTorsor V P] (s : Set P), s ⊆ ↑(affineSpan k s)
-- Mathlib.Analysis.Convex.Basic
MonotoneOn.convex_le : ∀ {𝕜 : Type u_1} {E : Type u_2} {β : Type u_4} [inst : Semiring 𝕜] [inst_1 : PartialOrder 𝕜] [inst_2 : AddCommMonoid E]
  [inst_3 : LinearOrder E] [IsOrderedAddMonoid E] [inst_5 : PartialOrder β] [inst_6 : Module 𝕜 E] [PosSMulMono 𝕜 E]
  {s : Set E} {f : E → β}, MonotoneOn f s → Convex 𝕜 s → ∀ (r : β), Convex 𝕜 {x | x ∈ s ∧ f x ≤ r}
-- Lean.ScopedEnvExtension
Lean.ScopedEnvExtension.State.mk.injEq : ∀ {σ : Type} (state : σ) (activeScopes : Lean.NameSet) (delimitsLocal : Bool) (state_1 : σ)
  (activeScopes_1 : Lean.NameSet) (delimitsLocal_1 : Bool),
  ({ state := state, activeScopes := activeScopes, delimitsLocal := delimitsLocal } =
      { state := state_1, activeScopes := activeScopes_1, delimitsLocal := delimitsLocal_1 }) =
    (state = state_1 ∧ activeScopes = activeScopes_1 ∧ delimitsLocal = delimitsLocal_1)
-- Mathlib.CategoryTheory.LiftingProperties.Adjunction
/-- The liftings of a commutative are in bijection with the liftings of its (right)
adjoint square.  -/
CategoryTheory.CommSq.rightAdjointLiftStructEquiv : {C : Type u_1} →
  {D : Type u_2} →
    [inst : CategoryTheory.Category.{v_1, u_1} C] →
      [inst_1 : CategoryTheory.Category.{v_2, u_2} D] →
        {G : CategoryTheory.Functor C D} →
          {F : CategoryTheory.Functor D C} →
            {A B : C} →
              {X Y : D} →
                {i : A ⟶ B} →
                  {p : X ⟶ Y} →
                    {u : G.obj A ⟶ X} →
                      {v : G.obj B ⟶ Y} →
                        (sq : CategoryTheory.CommSq u (G.map i) p v) → (adj : G ⊣ F) → sq.LiftStruct ≃ ⋯.LiftStruct
-- Mathlib.CategoryTheory.Limits.Constructions.FiniteProductsOfBinaryProducts
/-- If `C` has an initial object and binary coproducts, then it has a coproduct for objects indexed by
`Fin n`.
This is a helper lemma for `hasFiniteCoproducts_of_has_binary_and_initial`, which is more general
than this.
 -/
_private.Mathlib.CategoryTheory.Limits.Constructions.FiniteProductsOfBinaryProducts.0.CategoryTheory.hasCoproduct_fin : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasBinaryCoproducts C]
  [CategoryTheory.Limits.HasInitial C] (n : ℕ) (f : Fin n → C), CategoryTheory.Limits.HasCoproduct f
-- Mathlib.CategoryTheory.Limits.FunctorCategory.Basic
CategoryTheory.Limits.limitObjIsoLimitCompEvaluation_inv_π_app : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {J : Type u₁} [inst_1 : CategoryTheory.Category.{v₁, u₁} J]
  {K : Type u₂} [inst_2 : CategoryTheory.Category.{v₂, u₂} K] [inst_3 : CategoryTheory.Limits.HasLimitsOfShape J C]
  (F : CategoryTheory.Functor J (CategoryTheory.Functor K C)) (j : J) (k : K),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.limitObjIsoLimitCompEvaluation F k).inv
      ((CategoryTheory.Limits.limit.π F j).app k) =
    CategoryTheory.Limits.limit.π (F.comp ((CategoryTheory.evaluation K C).obj k)) j
-- Lean.Parser.Command
Lean.Parser.Command.structExplicitBinder : Lean.Parser.Parser
-- Mathlib.MeasureTheory.Integral.Lebesgue.Basic
MeasureTheory.setLIntegral_measure_zero : ∀ {α : Type u_1} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} (s : Set α) (f : α → ENNReal),
  μ s = 0 → ∫⁻ (x : α) in s, f x ∂μ = 0
-- Std.Data.ExtTreeMap.Basic
/-- Tries to retrieve the smallest key that is greater than or equal to the
given key, returning `none` if no such key exists.
 -/
Std.ExtTreeMap.getKeyGE? : {α : Type u} → {β : Type v} → {cmp : α → α → Ordering} → [Std.TransCmp cmp] → Std.ExtTreeMap α β cmp → α → Option α
-- Lean.Meta.Tactic.Contradiction
/-- Check whether any of the hypotheses is an empty type.  -/
Lean.Meta.Contradiction.Config.emptyType : Lean.Meta.Contradiction.Config → Bool
-- Mathlib.GroupTheory.Coxeter.Length
CoxeterSystem.length_wordProd_le : ∀ {B : Type u_1} {W : Type u_2} [inst : Group W] {M : CoxeterMatrix B} (cs : CoxeterSystem M W) (ω : List B),
  cs.length (cs.wordProd ω) ≤ ω.length
-- Mathlib.Topology.Homotopy.Equiv
/-- If `X` is homotopy equivalent to `Y` and `Z` is homotopy equivalent to `Z'`, then `X × Z` is
homotopy equivalent to `Z × Z'`.  -/
ContinuousMap.HomotopyEquiv.prodCongr : {X : Type u} →
  {Y : Type v} →
    {Z : Type w} →
      {Z' : Type x} →
        [inst : TopologicalSpace X] →
          [inst_1 : TopologicalSpace Y] →
            [inst_2 : TopologicalSpace Z] →
              [inst_3 : TopologicalSpace Z'] →
                ContinuousMap.HomotopyEquiv X Y →
                  ContinuousMap.HomotopyEquiv Z Z' → ContinuousMap.HomotopyEquiv (X × Z) (Y × Z')
-- Mathlib.RingTheory.Morita.Basic
MoritaEquivalence.mk.injEq : ∀ {R : Type u₀} [inst : CommSemiring R] {A : Type u₁} [inst_1 : Ring A] [inst_2 : Algebra R A] {B : Type u₂}
  [inst_3 : Ring B] [inst_4 : Algebra R B] (eqv : ModuleCat A ≌ ModuleCat B)
  (linear : autoParam (CategoryTheory.Functor.Linear R eqv.functor) MoritaEquivalence.linear._autoParam)
  (eqv_1 : ModuleCat A ≌ ModuleCat B)
  (linear_1 : autoParam (CategoryTheory.Functor.Linear R eqv_1.functor) MoritaEquivalence.linear._autoParam),
  ({ eqv := eqv, linear := linear } = { eqv := eqv_1, linear := linear_1 }) = (eqv = eqv_1)