mathlib-initiative/mathlib-types huggingface dataset:
-- Init.SimpLemmas
not_decide_eq_true : ∀ {p : Prop} [h : Decidable p], ((!decide p) = true) = ¬p
-- Lean.Meta.Tactic.Grind.Parser
Lean.Parser.Command.GrindCnstr.genLt.parenthesizer : Lean.PrettyPrinter.Parenthesizer
-- Init.Data.Range.Polymorphic.PRange
Std.instDecidableEqRcc.decEq : {α : Type u_1} → [DecidableEq α] → (x x_1 : Std.Rcc α) → Decidable (x = x_1)
-- Init.Data.UInt.Lemmas
USize.toNat_zero : USize.toNat 0 = 0
-- Mathlib.Algebra.Lie.Weights.Killing
LieAlgebra.IsKilling.lie_eq_killingForm_smul_of_mem_rootSpace_of_mem_rootSpace_neg : ∀ {K : Type u_2} {L : Type u_3} [inst : LieRing L] [inst_1 : Field K] [inst_2 : LieAlgebra K L]
  [inst_3 : FiniteDimensional K L] {H : LieSubalgebra K L} [inst_4 : H.IsCartanSubalgebra]
  [inst_5 : LieAlgebra.IsKilling K L] [LieModule.IsTriangularizable K (↥H) L] [PerfectField K]
  {α : LieModule.Weight K (↥H) L} {e f : L},
  e ∈ LieAlgebra.rootSpace H ⇑α →
    f ∈ LieAlgebra.rootSpace H (-⇑α) →
      ⁅e, f⁆ =
        ((killingForm K L) e) f •
          ↑((LieAlgebra.IsKilling.cartanEquivDual H).symm (LieModule.Weight.toLinear K (↥H) L α))
-- Mathlib.LinearAlgebra.Matrix.Determinant.Basic
Matrix.det_diagonal : ∀ {n : Type u_2} [inst : DecidableEq n] [inst_1 : Fintype n] {R : Type v} [inst_2 : CommRing R] {d : n → R},
  (Matrix.diagonal d).det = ∏ i, d i
-- Mathlib.Algebra.Category.ModuleCat.Sheaf.Free
SheafOfModules.ιFree_mapFreeIso_hom_assoc : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {J : CategoryTheory.GrothendieckTopology C}
  {R : CategoryTheory.Sheaf J RingCat} [inst_1 : CategoryTheory.HasWeakSheafify J AddCommGrpCat]
  [inst_2 : J.WEqualsLocallyBijective AddCommGrpCat] {C' : Type u₂} [inst_3 : CategoryTheory.Category.{v₂, u₂} C']
  {J' : CategoryTheory.GrothendieckTopology C'} {S : CategoryTheory.Sheaf J' RingCat}
  [inst_4 : CategoryTheory.HasSheafify J' AddCommGrpCat] [inst_5 : J'.WEqualsLocallyBijective AddCommGrpCat]
  (F : CategoryTheory.Functor (SheafOfModules R) (SheafOfModules S)) (I : Type u)
  [inst_6 : CategoryTheory.Limits.PreservesColimitsOfShape (CategoryTheory.Discrete I) F]
  (η : SheafOfModules.unit S ≅ F.obj (SheafOfModules.unit R)) (i : I) {Z : SheafOfModules S}
  (h : F.obj (SheafOfModules.free I) ⟶ Z),
  CategoryTheory.CategoryStruct.comp (SheafOfModules.ιFree i)
      (CategoryTheory.CategoryStruct.comp (SheafOfModules.mapFreeIso F I η).hom h) =
    CategoryTheory.CategoryStruct.comp η.hom (CategoryTheory.CategoryStruct.comp (F.map (SheafOfModules.ιFree i)) h)
-- Mathlib.NumberTheory.FLT.Three
_private.Mathlib.NumberTheory.FLT.Three.0.FermatLastTheoremForThreeGen.Solution.X.congr_simp : ∀ {K : Type u_1} [inst : Field K] {ζ : K} {hζ : IsPrimitiveRoot ζ 3}
  (S S_1 : FermatLastTheoremForThreeGen.Solution✝ hζ),
  S = S_1 →
    ∀ [inst_1 : NumberField K] [inst_2 : IsCyclotomicExtension {3} ℚ K],
      FermatLastTheoremForThreeGen.Solution.X✝ S = FermatLastTheoremForThreeGen.Solution.X✝ S_1
-- Mathlib.Algebra.Order.Monoid.Unbundled.Basic
le_mul_of_le_mul_left : ∀ {α : Type u_1} [inst : Mul α] [inst_1 : Preorder α] [MulLeftMono α] {a b c d : α}, a ≤ b * c → c ≤ d → a ≤ b * d
-- Lean.Elab.Tactic.Grind.Basic
Lean.Elab.Tactic.Grind.DSimpArgs.mk.injEq : ∀ (fvarIds : Array Lean.FVarId) (zetaDeltaAll : Bool) (fvarIds_1 : Array Lean.FVarId) (zetaDeltaAll_1 : Bool),
  ({ fvarIds := fvarIds, zetaDeltaAll := zetaDeltaAll } = { fvarIds := fvarIds_1, zetaDeltaAll := zetaDeltaAll_1 }) =
    (fvarIds = fvarIds_1 ∧ zetaDeltaAll = zetaDeltaAll_1)
-- Mathlib.Order.Max
noMaxOrder_iff : ∀ {α : Type u_1} [inst : Preorder α], NoMaxOrder α ↔ ∀ (x : α), ¬IsMax x
-- Mathlib.FieldTheory.IntermediateField.Basic
/-- The isomorphism from `L` to the field range of the `AlgHom` `f`, sending `x` to `f x`.  -/
AlgHom.equivFieldRange : {K : Type u_1} →
  {L : Type u_2} →
    {L' : Type u_3} →
      [inst : Field K] →
        [inst_1 : Field L] →
          [inst_2 : Field L'] →
            [inst_3 : Algebra K L] → [inst_4 : Algebra K L'] → (f : L →ₐ[K] L') → L ≃ₐ[K] ↥f.fieldRange
-- Lean.Meta.Tactic.Grind.AC.Types
Lean.Meta.Grind.AC.EqCnstr.mk.injEq : ∀ (lhs rhs : Lean.Grind.AC.Seq) (h : Lean.Meta.Grind.AC.EqCnstrProof) (id : ℕ) (lhs_1 rhs_1 : Lean.Grind.AC.Seq)
  (h_1 : Lean.Meta.Grind.AC.EqCnstrProof) (id_1 : ℕ),
  ({ lhs := lhs, rhs := rhs, h := h, id := id } = { lhs := lhs_1, rhs := rhs_1, h := h_1, id := id_1 }) =
    (lhs = lhs_1 ∧ rhs = rhs_1 ∧ h = h_1 ∧ id = id_1)
-- Init.Data.List.Lemmas
List.dropLast_cons_of_ne_nil : ∀ {α : Type u} {x : α} {l : List α}, l ≠ [] → (x :: l).dropLast = x :: l.dropLast
-- ProofWidgets.Data.Html
/-- A HTML tree which may contain widget components.  -/
ProofWidgets.Html : Type
-- Mathlib.Data.Fintype.Sum
Finset.toRight_eq_empty : ∀ {α : Type u_3} {β : Type u_4} [inst : Fintype α] {u : Finset (α ⊕ β)},
  u.toRight = ∅ ↔ u ⊆ Finset.map Function.Embedding.inl Finset.univ
-- Init.Data.Rat.Basic
Rat.instOfNat : {n : ℕ} → OfNat ℚ n
-- Init.Data.Int.Cooper
Int.Cooper.resolve_left_ineq : ∀ {b q : ℤ} (a c d p x : ℤ),
  0 < a → 0 < b → p ≤ a * x → b * x ≤ q → b * Int.Cooper.resolve_left a c d p x + b * p ≤ a * q
-- Mathlib.Data.Finsupp.Ext
Finsupp.mulHom_ext' : ∀ {α : Type u_1} {M : Type u_2} {N : Type u_3} [inst : AddZeroClass M] [inst_1 : MulOneClass N]
  {f g : Multiplicative (α →₀ M) →* N},
  (∀ (x : α),
      f.comp (AddMonoidHom.toMultiplicative (Finsupp.singleAddHom x)) =
        g.comp (AddMonoidHom.toMultiplicative (Finsupp.singleAddHom x))) →
    f = g
-- Mathlib.RingTheory.FractionalIdeal.Basic
FractionalIdeal.zero_mem : ∀ {R : Type u_1} [inst : CommRing R] {S : Submonoid R} {P : Type u_2} [inst_1 : CommRing P] [inst_2 : Algebra R P]
  (I : FractionalIdeal S P), 0 ∈ I
-- Init.Data.Vector.Lemmas
Vector.mem_map_of_mem : ∀ {α : Type u_1} {β : Type u_2} {n : ℕ} {xs : Vector α n} {a : α} {f : α → β}, a ∈ xs → f a ∈ Vector.map f xs
-- Aesop.RuleTac.Descr
Aesop.RuleTacDescr.forward.inj : ∀ {term : Aesop.RuleTerm} {immediate : Aesop.UnorderedArraySet Aesop.PremiseIndex} {isDestruct : Bool}
  {term_1 : Aesop.RuleTerm} {immediate_1 : Aesop.UnorderedArraySet Aesop.PremiseIndex} {isDestruct_1 : Bool},
  Aesop.RuleTacDescr.forward term immediate isDestruct = Aesop.RuleTacDescr.forward term_1 immediate_1 isDestruct_1 →
    term = term_1 ∧ immediate = immediate_1 ∧ isDestruct = isDestruct_1
-- Mathlib.LinearAlgebra.LinearDisjoint
/-- Linear disjointness is symmetric if elements in the module commute.  -/
Submodule.linearDisjoint_comm_of_commute : ∀ {R : Type u} {S : Type v} [inst : CommSemiring R] [inst_1 : Semiring S] [inst_2 : Algebra R S] {M N : Submodule R S},
  (∀ (m : ↥M) (n : ↥N), Commute ↑m ↑n) → (M.LinearDisjoint N ↔ N.LinearDisjoint M)
-- Mathlib.Analysis.Analytic.IsolatedZeros
/-- Preimages of codiscrete sets, local filter version: if `f` is analytic at `x` and not locally
constant, then the push-forward of the punctured neighbourhood filter `𝓝[≠] x` is less than or
equal to the punctured neighbourhood filter `𝓝[≠] f x`.  -/
AnalyticAt.map_nhdsNE : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {x : 𝕜} {f : 𝕜 → E},
  AnalyticAt 𝕜 f x → ¬Filter.EventuallyConst f (nhds x) → Filter.map f (nhdsWithin x {x}ᶜ) ≤ nhdsWithin (f x) {f x}ᶜ
-- Mathlib.Data.Fin.Fin2
/-- The unique field of `Fin2.IsLT`, a proof that `m < n`.  -/
Fin2.IsLT.h : ∀ {m n : ℕ} [self : Fin2.IsLT m n], m < n
-- Init.Data.Range.Polymorphic.PRange
/-- `a...=b` is the range of elements greater than or equal to `a` and less than or equal to
`b`. See also `Std.Rcc`.
 -/
Std.«term_...=_» : Lean.TrailingParserDescr
-- Mathlib.Topology.ContinuousMap.Bounded.Basic
BoundedContinuousFunction.mkOfCompact_one : ∀ {α : Type u} {β : Type v} [inst : TopologicalSpace α] [inst_1 : PseudoMetricSpace β] [inst_2 : One β]
  [inst_3 : CompactSpace α], BoundedContinuousFunction.mkOfCompact 1 = 1
-- Mathlib.CategoryTheory.Monoidal.Action.Basic
CategoryTheory.MonoidalCategory.selRightfAction_actionObj : ∀ (C : Type u_1) [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.MonoidalCategory C] (x y : C),
  CategoryTheory.MonoidalCategory.MonoidalRightActionStruct.actionObj x y =
    CategoryTheory.MonoidalCategoryStruct.tensorObj x y
-- Mathlib.Algebra.Polynomial.FieldDivision
Polynomial.mod_eq_of_dvd_sub : ∀ {R : Type u} [inst : Field R] {p₁ p₂ q : Polynomial R}, q ∣ p₁ - p₂ → p₁ % q = p₂ % q
-- Mathlib.Analysis.Calculus.MeanValue
/-- If `f : 𝕜 → G`, `𝕜 = R` or `𝕜 = ℂ`, is differentiable everywhere and its derivative equal zero,
then it is a constant function.  -/
is_const_of_deriv_eq_zero : ∀ {𝕜 : Type u_3} {G : Type u_4} [inst : RCLike 𝕜] [inst_1 : NormedAddCommGroup G] [inst_2 : NormedSpace 𝕜 G]
  {f : 𝕜 → G}, Differentiable 𝕜 f → (∀ (x : 𝕜), deriv f x = 0) → ∀ (x y : 𝕜), f x = f y
-- Std.Data.Internal.List.Associative
Std.Internal.List.getValue?_insertListConst_of_mem : ∀ {α : Type u} {β : Type v} [inst : BEq α] [EquivBEq α] {l : List ((_ : α) × β)} {toInsert : List (α × β)},
  Std.Internal.List.DistinctKeys l →
    ∀ {k k' : α},
      (k == k') = true →
        ∀ {v : β},
          List.Pairwise (fun a b => (a.1 == b.1) = false) toInsert →
            (k, v) ∈ toInsert → Std.Internal.List.getValue? k' (Std.Internal.List.insertListConst l toInsert) = some v
-- Mathlib.Order.Disjoint
isCompl_top_bot : ∀ {α : Type u_1} [inst : Lattice α] [inst_1 : BoundedOrder α], IsCompl ⊤ ⊥
-- Mathlib.Algebra.FiniteSupport.Basic
Function.HasFiniteMulSupport.pow : ∀ {α : Type u_1} {M : Type u_3} [inst : Monoid M] {f : α → M},
  Function.HasFiniteMulSupport f → ∀ (n : ℕ), Function.HasFiniteMulSupport (f ^ n)
-- Mathlib.GroupTheory.GroupExtension.Defs
GroupExtension.conjAct.eq_1 : ∀ {N : Type u_1} {E : Type u_2} {G : Type u_3} [inst : Group N] [inst_1 : Group E] [inst_2 : Group G]
  (S : GroupExtension N E G),
  S.conjAct =
    {
      toFun := fun e =>
        (MonoidHom.ofInjective ⋯).trans (MulEquiv.trans (MulAut.conjNormal e) (MonoidHom.ofInjective ⋯).symm),
      map_one' := ⋯, map_mul' := ⋯ }
-- Mathlib.RingTheory.Localization.FractionRing
IsFractionRing.injective : ∀ (R : Type u_1) [inst : CommRing R] (K : Type u_5) [inst_1 : CommRing K] [inst_2 : Algebra R K] [IsFractionRing R K],
  Function.Injective ⇑(algebraMap R K)
-- Mathlib.CategoryTheory.Comma.StructuredArrow.CommaMap
CategoryTheory.StructuredArrow.commaMapEquivalenceFunctor_map_left : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  {T : Type u₃} [inst_2 : CategoryTheory.Category.{v₃, u₃} T] {L : CategoryTheory.Functor C T}
  {R : CategoryTheory.Functor D T} {C' : Type u₄} [inst_3 : CategoryTheory.Category.{v₄, u₄} C'] {D' : Type u₅}
  [inst_4 : CategoryTheory.Category.{v₅, u₅} D'] {T' : Type u₆} [inst_5 : CategoryTheory.Category.{v₆, u₆} T']
  {L' : CategoryTheory.Functor C' T'} {R' : CategoryTheory.Functor D' T'} {F₁ : CategoryTheory.Functor C C'}
  {F₂ : CategoryTheory.Functor D D'} {F : CategoryTheory.Functor T T'} (α : F₁.comp L' ⟶ L.comp F)
  (β : R.comp F ⟶ F₂.comp R') [inst_6 : CategoryTheory.IsIso β] (X : CategoryTheory.Comma L' R')
  {Y Z : CategoryTheory.StructuredArrow X (CategoryTheory.Comma.map α β)} (f : Y ⟶ Z),
  ((CategoryTheory.StructuredArrow.commaMapEquivalenceFunctor α β X).map f).left =
    CategoryTheory.StructuredArrow.homMk (CategoryTheory.StructuredArrow.Hom.right f).left ⋯
-- Mathlib.Combinatorics.Quiver.Covering
Quiver.starEquivCostar_apply_fst : ∀ {U : Type u_1} [inst : Quiver U] [inst_1 : Quiver.HasInvolutiveReverse U] (u : U) (e : Quiver.Star u),
  ((Quiver.starEquivCostar u) e).fst = e.fst
-- Mathlib.Algebra.Homology.EulerCharacteristic
ComplexShape.eulerCharSignsUpNat : (ComplexShape.up ℕ).EulerCharSigns
-- Mathlib.CategoryTheory.Presentable.LocallyPresentable
CategoryTheory.IsCardinalAccessibleCategory.mk : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {κ : Cardinal.{w}} [inst_1 : Fact κ.IsRegular]
  [toHasCardinalFilteredGenerator : CategoryTheory.HasCardinalFilteredGenerator C κ]
  [toHasCardinalFilteredColimits : CategoryTheory.HasCardinalFilteredColimits C κ],
  CategoryTheory.IsCardinalAccessibleCategory C κ
-- Mathlib.Topology.MetricSpace.HausdorffDistance
/-- **Alias** of `Metric.hausdorffEDist_self`.

---

The Hausdorff edistance of a set to itself vanishes.  -/
EMetric.hausdorffEdist_self : ∀ {α : Type u} [inst : PseudoEMetricSpace α] {s : Set α}, Metric.hausdorffEDist s s = 0
-- Mathlib.Order.SymmDiff
symmDiff_eq_left : ∀ {α : Type u_2} [inst : GeneralizedBooleanAlgebra α] {a b : α}, symmDiff a b = a ↔ b = ⊥
-- Mathlib.Order.Filter.Defs
/-- A filter `F` on a type `α` is a collection of sets of `α` which contains the whole `α`,
is upwards-closed, and is stable under intersection. We do not forbid this collection to be
all sets of `α`.  -/
Filter : Type u_1 → Type u_1
-- Std.Data.TreeSet.Lemmas
Std.TreeSet.getD_union_of_not_mem_right : ∀ {α : Type u} {cmp : α → α → Ordering} {t₁ t₂ : Std.TreeSet α cmp} [Std.TransCmp cmp] {k fallback : α},
  k ∉ t₂ → (t₁ ∪ t₂).getD k fallback = t₁.getD k fallback
-- Mathlib.CategoryTheory.Limits.Types.Limits
CategoryTheory.Limits.Types.isLimit_iff : ∀ {J : Type v} [inst : CategoryTheory.Category.{w, v} J] {F : CategoryTheory.Functor J (Type u)}
  (c : CategoryTheory.Limits.Cone F),
  Nonempty (CategoryTheory.Limits.IsLimit c) ↔
    ∀ s ∈ F.sections, ∃! x, ∀ (j : J), (CategoryTheory.ConcreteCategory.hom (c.π.app j)) x = s j
-- Mathlib.Tactic.CategoryTheory.Coherence.Datatypes
Mathlib.Tactic.BicategoryLike.Mor₁.of.inj : ∀ {a a_1 : Mathlib.Tactic.BicategoryLike.Atom₁},
  Mathlib.Tactic.BicategoryLike.Mor₁.of a = Mathlib.Tactic.BicategoryLike.Mor₁.of a_1 → a = a_1
-- Mathlib.Computability.AkraBazzi.GrowsPolynomially
AkraBazziRecurrence.GrowsPolynomially.eventually_atTop_le_nat : ∀ {f : ℝ → ℝ} {b : ℝ},
  b ∈ Set.Ioo 0 1 →
    AkraBazziRecurrence.GrowsPolynomially f →
      ∃ c > 0, ∀ᶠ (n : ℕ) in Filter.atTop, ∀ u ∈ Set.Icc (b * ↑n) ↑n, f u ≤ c * f ↑n
-- Mathlib.RingTheory.Perfection
ModP.preVal_zero : ∀ {K : Type u₁} [inst : Field K] {v : Valuation K NNReal} {O : Type u₂} [inst_1 : CommRing O] [inst_2 : Algebra O K]
  {p : ℕ}, ModP.preVal K v O p 0 = 0
-- Mathlib.RingTheory.Ideal.Norm.RelNorm
/-- This condition `eq_bot_or_top` is equivalent to being a field.
However, `Ideal.spanNorm_mul_of_field` is harder to apply since we'd need to upgrade a `CommRing R`
instance to a `Field R` instance.  -/
Ideal.spanNorm_mul_of_bot_or_top : ∀ (R : Type u_1) [inst : CommRing R] [inst_1 : IsDomain R] {S : Type u_3} [inst_2 : CommRing S] [inst_3 : IsDomain S]
  [inst_4 : IsIntegrallyClosed R] [inst_5 : IsIntegrallyClosed S] [inst_6 : Algebra R S] [inst_7 : Module.Finite R S]
  [inst_8 : Module.IsTorsionFree R S],
  (∀ (I : Ideal R), I = ⊥ ∨ I = ⊤) →
    ∀ (I J : Ideal S), Ideal.spanNorm R (I * J) = Ideal.spanNorm R I * Ideal.spanNorm R J
-- Mathlib.CategoryTheory.Abelian.Injective.Dimension
CategoryTheory.hasInjectiveDimensionLT_iff : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Abelian C] (X : C) (n : ℕ)
  [inst_2 : CategoryTheory.HasExt C],
  CategoryTheory.HasInjectiveDimensionLT X n ↔
    ∀ (i : ℕ), n ≤ i → ∀ ⦃Y : C⦄ (e : CategoryTheory.Abelian.Ext Y X i), e = 0
-- Lean.Elab.Tactic.Try
Lean.Elab.Tactic.Try.tryTacticElabAttribute : Lean.KeyedDeclsAttribute Lean.Elab.Tactic.Try.TryTactic
-- Std.Data.DHashMap.Lemmas
Std.DHashMap.get_inter : ∀ {α : Type u} {β : α → Type v} {x : BEq α} {x_1 : Hashable α} {m₁ m₂ : Std.DHashMap α β} [inst : LawfulBEq α] {k : α}
  {h_mem : k ∈ m₁ ∩ m₂}, (m₁ ∩ m₂).get k h_mem = m₁.get k ⋯
-- Init.Data.Option.Attach
Option.toArray_pbind : ∀ {α : Type u_1} {β : Type u_2} {o : Option α} {f : (a : α) → o = some a → Option β},
  (o.pbind f).toArray =
    Array.flatMap
      (fun x =>
        match x with
        | ⟨x, h⟩ => (f x h).toArray)
      o.attach.toArray
-- Mathlib.RingTheory.Ideal.Oka
Ideal.IsOka.oka : ∀ {R : Type u_1} [inst : CommSemiring R] {P : Ideal R → Prop},
  Ideal.IsOka P → ∀ {I : Ideal R} {a : R}, P (I ⊔ Ideal.span {a}) → P (Submodule.colon I ↑(Ideal.span {a})) → P I
-- Mathlib.Lean.Meta.RefinedDiscrTree.Encode
/-- Check whether the expression is represented by `Key.star` and has `arg` as an argument.  -/
_private.Mathlib.Lean.Meta.RefinedDiscrTree.Encode.0.Lean.Meta.RefinedDiscrTree.etaPossibilities.isStarWithArg : Lean.Expr → Lean.Expr → Bool
-- Mathlib.CategoryTheory.Sites.Coverage
CategoryTheory.Coverage.ext_iff : ∀ {C : Type u_1} {inst : CategoryTheory.Category.{v_1, u_1} C} {x y : CategoryTheory.Coverage C},
  x = y ↔ x.coverings = y.coverings
-- Mathlib.AlgebraicTopology.FundamentalGroupoid.Basic
FundamentalGroupoid.isEmpty_iff : ∀ (X : Type u_3), IsEmpty (FundamentalGroupoid X) ↔ IsEmpty X
-- Mathlib.Order.Defs.LinearOrder
min_le_left : ∀ {α : Type u_1} [inst : LinearOrder α] (a b : α), min a b ≤ a
-- Lean.DocString.Add
/-- Elaborates already-parsed Verso `blocks` for the specified declaration with interactive features
disabled, reporting any elaboration messages at the current reference. When `fileMap?` is provided,
message positions are interpreted against it.
 -/
_private.Lean.DocString.Add.0.Lean.execVersoBlocks : Lean.Name → Lean.Syntax → Array Lean.Syntax → Option Lean.FileMap → Lean.Elab.TermElabM Lean.VersoDocResult
-- Std.Data.HashMap.Lemmas
Std.HashMap.size_le_size_insertMany_list : ∀ {α : Type u} {β : Type v} {x : BEq α} {x_1 : Hashable α} {m : Std.HashMap α β} [EquivBEq α] [LawfulHashable α]
  {l : List (α × β)}, m.size ≤ (m.insertMany l).size
-- Batteries.Data.Fin.Coding
Fin.decodeSum.eq_1 : ∀ {n m : ℕ} (x : Fin (n + m)), Fin.decodeSum x = Fin.addCases Sum.inl Sum.inr x
-- Mathlib.Analysis.Normed.Group.Defs
ESeminormedAddCommMonoid.mk : {E : Type u_8} →
  [inst : TopologicalSpace E] →
    [toESeminormedAddMonoid : ESeminormedAddMonoid E] → (∀ (a b : E), a + b = b + a) → ESeminormedAddCommMonoid E
-- Mathlib.Topology.ContinuousMap.ContinuousMapZero
ContinuousMapZero.instNonUnitalCommSemiring : {X : Type u_1} →
  {R : Type u_2} →
    [inst : Zero X] →
      [inst_1 : TopologicalSpace X] →
        [inst_2 : TopologicalSpace R] →
          [inst_3 : CommSemiring R] → [IsTopologicalSemiring R] → NonUnitalCommSemiring (ContinuousMapZero X R)
-- Mathlib.CategoryTheory.Bicategory.CatEnriched
/-- The horizontal composition on 2-morphisms is defined using the action on arrows of the
composition bifunctor from the enriched category structure.  -/
CategoryTheory.CatEnrichedOrdinary.hComp : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    [inst_1 : CategoryTheory.EnrichedOrdinaryCategory CategoryTheory.Cat C] →
      {a b c : CategoryTheory.CatEnrichedOrdinary C} →
        {f f' : a ⟶ b} →
          {g g' : b ⟶ c} →
            (f ⟶ f') → (g ⟶ g') → (CategoryTheory.CategoryStruct.comp f g ⟶ CategoryTheory.CategoryStruct.comp f' g')
-- Mathlib.AlgebraicTopology.SimplicialSet.AnodyneExtensions.Pairing
SSet.Subcomplex.N.orderIsoOfIso.congr_simp : ∀ {X : SSet} {A : X.Subcomplex} {Y : SSet} {B : Y.Subcomplex} (e e_1 : X ≅ Y) (e_e : e = e_1)
  (hA : B.preimage e.hom = A), SSet.Subcomplex.N.orderIsoOfIso e hA = SSet.Subcomplex.N.orderIsoOfIso e_1 ⋯
-- Mathlib.Probability.Process.Filtration
MeasureTheory.Filtration.mk.sizeOf_spec : ∀ {Ω : Type u_1} {ι : Type u_2} [inst : Preorder ι] {m : MeasurableSpace Ω} [inst_1 : SizeOf Ω] [inst_2 : SizeOf ι]
  (seq : ι → MeasurableSpace Ω) (mono' : Monotone seq) (le' : ∀ (i : ι), seq i ≤ m),
  sizeOf { seq := seq, mono' := mono', le' := le' } = 1
-- Mathlib.Data.Finite.Prod
Set.Finite.offDiag : ∀ {α : Type u_1} {s : Set α}, s.Finite → s.offDiag.Finite
-- Std.Data.DTreeMap.Internal.Queries
_private.Std.Data.DTreeMap.Internal.Queries.0.Std.DTreeMap.Internal.Impl.maxEntry.match_1.eq_2 : ∀ {α : Type u_1} {β : α → Type u_2} (motive : (x : Std.DTreeMap.Internal.Impl α β) → x.isEmpty = false → Sort u_3)
  (size : ℕ) (k : α) (v : β k) (l : Std.DTreeMap.Internal.Impl α β) (size_1 : ℕ) (k_1 : α) (v_1 : β k_1)
  (l_1 r : Std.DTreeMap.Internal.Impl α β)
  (h :
    (Std.DTreeMap.Internal.Impl.inner size k v l (Std.DTreeMap.Internal.Impl.inner size_1 k_1 v_1 l_1 r)).isEmpty =
      false)
  (h_1 :
    (size : ℕ) →
      (k : α) →
        (v : β k) →
          (l : Std.DTreeMap.Internal.Impl α β) →
            (x : (Std.DTreeMap.Internal.Impl.inner size k v l Std.DTreeMap.Internal.Impl.leaf).isEmpty = false) →
              motive (Std.DTreeMap.Internal.Impl.inner size k v l Std.DTreeMap.Internal.Impl.leaf) x)
  (h_2 :
    (size : ℕ) →
      (k : α) →
        (v : β k) →
          (l l_2 : Std.DTreeMap.Internal.Impl α β) →
            (size_2 : ℕ) →
              (k_2 : α) →
                (v_2 : β k_2) →
                  (l_3 r : Std.DTreeMap.Internal.Impl α β) →
                    l_2 = Std.DTreeMap.Internal.Impl.inner size_2 k_2 v_2 l_3 r →
                      (h :
                          (Std.DTreeMap.Internal.Impl.inner size k v l
                                (Std.DTreeMap.Internal.Impl.inner size_2 k_2 v_2 l_3 r)).isEmpty =
                            false) →
                        motive
                          (Std.DTreeMap.Internal.Impl.inner size k v l
                            (Std.DTreeMap.Internal.Impl.inner size_2 k_2 v_2 l_3 r))
                          h),
  (match Std.DTreeMap.Internal.Impl.inner size k v l (Std.DTreeMap.Internal.Impl.inner size_1 k_1 v_1 l_1 r), h with
    | Std.DTreeMap.Internal.Impl.inner size k v l Std.DTreeMap.Internal.Impl.leaf, x => h_1 size k v l x
    | Std.DTreeMap.Internal.Impl.inner size k v l l_2@h:(Std.DTreeMap.Internal.Impl.inner size_2 k_2 v_2 l_3 r), h_3 =>
      h_2 size k v l l_2 size_2 k_2 v_2 l_3 r h h_3) =
    h_2 size k v l (Std.DTreeMap.Internal.Impl.inner size_1 k_1 v_1 l_1 r) size_1 k_1 v_1 l_1 r ⋯ h
-- Mathlib.Geometry.RingedSpace.LocallyRingedSpace
AlgebraicGeometry.LocallyRingedSpace.restrictStalkIso_hom_eq_germ_assoc : ∀ {U : TopCat} (X : AlgebraicGeometry.LocallyRingedSpace) {f : U ⟶ X.toTopCat}
  (h : Topology.IsOpenEmbedding ⇑(CategoryTheory.ConcreteCategory.hom f)) (V : TopologicalSpace.Opens ↑U) (x : ↑U)
  (hx : x ∈ V) {Z : CommRingCat} (h_1 : X.presheaf.stalk ((CategoryTheory.ConcreteCategory.hom f) x) ⟶ Z),
  CategoryTheory.CategoryStruct.comp ((X.restrict h).presheaf.germ V x hx)
      (CategoryTheory.CategoryStruct.comp (X.restrictStalkIso h x).hom h_1) =
    CategoryTheory.CategoryStruct.comp (X.presheaf.germ (h.functor.obj V) ((CategoryTheory.ConcreteCategory.hom f) x) ⋯)
      h_1
-- Mathlib.Algebra.Category.Grp.Basic
GrpCat.ext : ∀ {X Y : GrpCat} {f g : X ⟶ Y},
  (∀ (x : ↑X), (CategoryTheory.ConcreteCategory.hom f) x = (CategoryTheory.ConcreteCategory.hom g) x) → f = g
-- Mathlib.Topology.MetricSpace.Congruence
/-- Congruence follows from preserved extended distance. Backward direction of
`congruent_iff_edist_eq`.  -/
Congruent.of_edist_eq : ∀ {ι : Type u_1} {P₁ : Type u_3} {P₂ : Type u_4} {v₁ : ι → P₁} {v₂ : ι → P₂} [inst : PseudoEMetricSpace P₁]
  [inst_1 : PseudoEMetricSpace P₂], (∀ (i₁ i₂ : ι), edist (v₁ i₁) (v₁ i₂) = edist (v₂ i₁) (v₂ i₂)) → Congruent v₁ v₂
-- Init.Internal.Order.Lemmas
Lean.Order.List.monotone_findM? : ∀ {γ : Type w} [inst : Lean.Order.PartialOrder γ] {m : Type → Type v} [inst_1 : Monad m]
  [inst_2 : (α : Type) → Lean.Order.PartialOrder (m α)] [Lean.Order.MonoBind m] {α : Type} (f : γ → α → m Bool)
  (xs : List α), Lean.Order.monotone f → Lean.Order.monotone fun x => List.findM? (f x) xs
-- Mathlib.Algebra.Homology.ShortComplex.Exact
CategoryTheory.ShortComplex.exact_and_epi_g_iff_of_iso : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  {S₁ S₂ : CategoryTheory.ShortComplex C} (e : S₁ ≅ S₂),
  S₁.Exact ∧ CategoryTheory.Epi S₁.g ↔ S₂.Exact ∧ CategoryTheory.Epi S₂.g
-- Mathlib.LinearAlgebra.GeneralLinearGroup.Basic
LinearMap.GeneralLinearGroup.congrLinearEquiv_apply : ∀ {R₁ : Type u_3} {R₂ : Type u_4} {M₁ : Type u_6} {M₂ : Type u_7} [inst : Semiring R₁] [inst_1 : Semiring R₂]
  [inst_2 : AddCommMonoid M₁] [inst_3 : AddCommMonoid M₂] [inst_4 : Module R₁ M₁] [inst_5 : Module R₂ M₂]
  {σ₁₂ : R₁ →+* R₂} {σ₂₁ : R₂ →+* R₁} [inst_6 : RingHomInvPair σ₁₂ σ₂₁] [inst_7 : RingHomInvPair σ₂₁ σ₁₂]
  (e₁₂ : M₁ ≃ₛₗ[σ₁₂] M₂) (g : LinearMap.GeneralLinearGroup R₁ M₁),
  (LinearMap.GeneralLinearGroup.congrLinearEquiv e₁₂) g =
    LinearMap.GeneralLinearGroup.ofLinearEquiv (e₁₂.symm.trans (g.toLinearEquiv.trans e₁₂))