mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Topology.Semicontinuity.Defs
/-- A real function `f` is lower semicontinuous at `x` if, for any `ε > 0`, for all `x'` close
enough to `x`, then `f x'` is at least `f x - ε`. We formulate this in a general preordered space,
using an arbitrary `y < f x` instead of `f x - ε`.  -/
LowerSemicontinuousAt : {α : Type u_1} → {β : Type u_2} → [TopologicalSpace α] → [Preorder β] → (α → β) → α → Prop
-- Mathlib.CategoryTheory.Limits.Shapes.WidePullbacks
/-- An aesop tactic for bulk cases on morphisms in `WidePushoutShape`  -/
CategoryTheory.Limits.WidePushoutShape.evalCasesBash' : Lean.Elab.Tactic.TacticM Unit
-- Mathlib.Analysis.Normed.Lp.ProdLp
WithLp.idemSnd_apply : ∀ {α : Type u_2} {β : Type u_3} [inst : SeminormedAddCommGroup α] [inst_1 : SeminormedAddCommGroup β] {p : ENNReal}
  (x : WithLp p (α × β)), WithLp.idemSnd x = WithLp.toLp p (0, x.snd)
-- Mathlib.Order.KrullDimension
/-- Another characterization of height, based on the supremum of the heights of elements below.  -/
Order.height_eq_iSup_lt_height : ∀ {α : Type u_1} [inst : Preorder α] (x : α), Order.height x = ⨆ y, ⨆ (_ : y < x), Order.height y + 1
-- Mathlib.CategoryTheory.Limits.Shapes.BinaryProducts
/-- Notation for the coproduct  -/
CategoryTheory.Limits.«term_⨿_» : Lean.TrailingParserDescr
-- Mathlib.MeasureTheory.Constructions.BorelSpace.Order
nullMeasurableSet_Iio : ∀ {α : Type u_1} [inst : TopologicalSpace α] {mα : MeasurableSpace α} [OpensMeasurableSpace α] [inst_2 : LinearOrder α]
  {a : α} {μ : MeasureTheory.Measure α} [ClosedIciTopology α], MeasureTheory.NullMeasurableSet (Set.Iio a) μ
-- Mathlib.Data.Seq.Basic
Stream'.Seq1.bind_ret : ∀ {α : Type u} {β : Type v} (f : α → β) (s : Stream'.Seq1 α), s.bind (Stream'.Seq1.ret ∘ f) = Stream'.Seq1.map f s
-- Mathlib.Algebra.Lie.CartanExists
LieAlgebra.exists_isCartanSubalgebra_engel_of_finrank_le_card : ∀ (K : Type u_1) (L : Type u_2) [inst : Field K] [inst_1 : LieRing L] [inst_2 : LieAlgebra K L] [Module.Finite K L],
  ↑(Module.finrank K L) ≤ Cardinal.mk K → ∃ x, (LieSubalgebra.engel K x).IsCartanSubalgebra
-- Lean.Data.Lsp.Internal
Lean.Lsp.instInhabitedLeanQueryModuleResponse.default : Lean.Lsp.LeanQueryModuleResponse
-- Mathlib.Topology.Algebra.OpenSubgroup
Subgroup.isOpen_of_mem_nhds : ∀ {G : Type u_1} [inst : Group G] [inst_1 : TopologicalSpace G] [SeparatelyContinuousMul G] (H : Subgroup G) {g : G},
  ↑H ∈ nhds g → IsOpen ↑H
-- Mathlib.MeasureTheory.Measure.GiryMonad
AEMeasurable.ae_of_bind : ∀ {α : Type u_1} {β : Type u_2} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} {γ : Type u_3} {x : MeasurableSpace γ}
  {m : MeasureTheory.Measure α} {f : α → MeasureTheory.Measure β} {g : β → γ},
  AEMeasurable f m → AEMeasurable g (m.bind f) → ∀ᵐ (a : α) ∂m, AEMeasurable g (f a)
-- Lean.Compiler.LCNF.Basic
Lean.Compiler.LCNF.CodeDecl.setTag : {pu : Lean.Compiler.LCNF.Purity} →
  Lean.FVarId →
    ℕ →
      autoParam (pu = Lean.Compiler.LCNF.Purity.impure) Lean.Compiler.LCNF.CodeDecl._auto_9 →
        Lean.Compiler.LCNF.CodeDecl pu
-- Mathlib.Algebra.Ring.Rat
Rat.divInt_div_divInt_cancel_right : ∀ {x : ℤ}, x ≠ 0 → ∀ (n d : ℤ), Rat.divInt x n / Rat.divInt x d = Rat.divInt d n
-- Lean.Data.LOption
Lean.LOption.some.inj : ∀ {α : Type u} {a a_1 : α}, Lean.LOption.some a = Lean.LOption.some a_1 → a = a_1
-- Mathlib.CategoryTheory.Preadditive.Injective.Basic
CategoryTheory.Injective.ι_mono : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.EnoughInjectives C] (X : C),
  CategoryTheory.Mono (CategoryTheory.Injective.ι X)
-- Init.Data.BitVec.Bitblast
BitVec.neg_slt_zero : ∀ {w : ℕ}, 0 < w → ∀ {x : BitVec w}, (-x).slt 0#w = (x == BitVec.intMin w || (0#w).slt x)
-- Init.Core
DoResultPRBC.return.inj : ∀ {α β σ : Type u} {a : β} {a_1 : σ} {a_2 : β} {a_3 : σ},
  DoResultPRBC.return a a_1 = DoResultPRBC.return a_2 a_3 → a = a_2 ∧ a_1 = a_3
-- Mathlib.ModelTheory.Basic
FirstOrder.Language.Equiv.refl_toEmbedding : ∀ {L : FirstOrder.Language} {M : Type w} [inst : L.Structure M],
  (FirstOrder.Language.Equiv.refl L M).toEmbedding = FirstOrder.Language.Embedding.refl L M
-- Mathlib.NumberTheory.PellMatiyasevic
Pell.x_pos : ∀ {a : ℕ} (a1 : 1 < a) (n : ℕ), 0 < Pell.xn a1 n
-- Std.Data.TreeMap.Lemmas
Std.TreeMap.getKey_minKey? : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Std.TreeMap α β cmp} [inst : Std.TransCmp cmp] {km : α}
  {hc : t.contains km = true}, t.minKey?.get ⋯ = km → t.getKey km hc = km
-- Std.Data.DTreeMap.Raw.Lemmas
Std.DTreeMap.Raw.Const.maxKeyD_modify_eq_maxKeyD : ∀ {α : Type u} {cmp : α → α → Ordering} {β : Type v} {t : Std.DTreeMap.Raw α (fun x => β) cmp} [Std.TransCmp cmp]
  [Std.LawfulEqCmp cmp],
  t.WF →
    ∀ {k : α} {f : β → β} {fallback : α}, (Std.DTreeMap.Raw.Const.modify t k f).maxKeyD fallback = t.maxKeyD fallback
-- Mathlib.Algebra.Ring.Equiv
RingEquiv.toRingHom_eq_coe : ∀ {R : Type u_4} {S : Type u_5} [inst : NonAssocSemiring R] [inst_1 : NonAssocSemiring S] (f : R ≃+* S),
  f.toRingHom = ↑f
-- Batteries.Data.String.Lemmas
String.atEnd_iff : ∀ (s : String) (p : String.Pos.Raw), String.Pos.Raw.atEnd s p = true ↔ s.rawEndPos ≤ p
-- Mathlib.Tactic.Relation.Rfl
/-- If `e` is the form `@R .. x y`, where `R` is a reflexive
relation, return `some (R, x, y)`.
As a special case, if `e` is `@HEq α a β b`, return ``some (`HEq, a, b)``.  -/
Lean.Expr.relSidesIfRefl? : Lean.Expr → Lean.MetaM (Option (Lean.Name × Lean.Expr × Lean.Expr))
-- Mathlib.Analysis.Calculus.FDeriv.Affine
ContinuousAffineMap.differentiable : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {F : Type u_3} [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F] (f : E →ᴬ[𝕜] F),
  Differentiable 𝕜 ⇑f
-- Lean.Meta.Tactic.Simp.Rewrite
Lean.Meta.Simp.simpArith : Lean.Expr → Lean.Meta.SimpM Lean.Meta.Simp.Step
-- Mathlib.Tactic.ComputeAsymptotics.Multiseries.Corecursion
/-- If `op` is friendly, then `op s` and `op t` have the same head if `s` and `t`
have the same head.  -/
Tactic.ComputeAsymptotics.Seq.FriendlyOperation.op_head_eq : ∀ {α : Type u_1} {op : Stream'.Seq α → Stream'.Seq α},
  Tactic.ComputeAsymptotics.Seq.FriendlyOperation op →
    ∀ {s t : Stream'.Seq α}, s.head = t.head → (op s).head = (op t).head
-- Mathlib.Analysis.Convex.Basic
Convex.smul : ∀ {𝕜 : Type u_1} {E : Type u_2} [inst : CommSemiring 𝕜] [inst_1 : PartialOrder 𝕜] [inst_2 : AddCommMonoid E]
  [inst_3 : Module 𝕜 E] {s : Set E}, Convex 𝕜 s → ∀ (c : 𝕜), Convex 𝕜 (c • s)
-- Mathlib.FieldTheory.IsPerfectClosure
IsPerfectClosure.equiv_toRingHom : ∀ {K : Type u_1} {L : Type u_2} {M : Type u_3} [inst : CommRing K] [inst_1 : CommRing L] [inst_2 : CommRing M]
  (i : K →+* L) (j : K →+* M) (p : ℕ) [inst_3 : ExpChar M p] [inst_4 : ExpChar K p] [inst_5 : ExpChar L p]
  [inst_6 : PerfectRing L p] [inst_7 : IsPerfectClosure i p] [inst_8 : PerfectRing M p] [inst_9 : IsPerfectClosure j p],
  (IsPerfectClosure.equiv i j p).toRingHom = PerfectRing.lift i j p
-- Mathlib.Algebra.Lie.SemiDirect
/-- The product of two Lie algebras realized through a semidirect sum with trivial `ψ`  -/
LieAlgebra.SemiDirectSum.prod_iso : (R : Type u_1) →
  [inst : CommRing R] →
    (K : Type u_2) →
      [inst_1 : LieRing K] →
        [inst_2 : LieAlgebra R K] →
          (L : Type u_3) → [inst_3 : LieRing L] → [inst_4 : LieAlgebra R L] → (K ⋊⁅0⁆ L) ≃ₗ⁅R⁆ K × L
-- Mathlib.RingTheory.Spectrum.Prime.Basic
nilradical.eq_1 : ∀ (R : Type u_3) [inst : CommSemiring R], nilradical R = Ideal.radical 0
-- Mathlib.RingTheory.GradedAlgebra.Homogeneous.Maps
HomogeneousIdeal.comap_comap : ∀ {A : Type u_1} {B : Type u_2} {C : Type u_3} {σ : Type u_4} {τ : Type u_5} {ω : Type u_6} {ι : Type u_7}
  [inst : Semiring A] [inst_1 : Semiring B] [inst_2 : Semiring C] [inst_3 : SetLike σ A] [inst_4 : SetLike τ B]
  [inst_5 : SetLike ω C] [inst_6 : AddSubmonoidClass σ A] [inst_7 : AddSubmonoidClass τ B]
  [inst_8 : AddSubmonoidClass ω C] [inst_9 : DecidableEq ι] [inst_10 : AddMonoid ι] {𝒜 : ι → σ} {ℬ : ι → τ} {𝒞 : ι → ω}
  [inst_11 : GradedRing 𝒜] [inst_12 : GradedRing ℬ] [inst_13 : GradedRing 𝒞] (f : 𝒜 →+*ᵍ ℬ) (g : ℬ →+*ᵍ 𝒞)
  {K : HomogeneousIdeal 𝒞}, HomogeneousIdeal.comap f (HomogeneousIdeal.comap g K) = HomogeneousIdeal.comap (g.comp f) K
-- Mathlib.Tactic.CategoryTheory.Coherence
/-- If set to `false`, the warning on the use of the deprecated coherence tactic is disabled.
 -/
Mathlib.Tactic.Coherence.warn.refl_coherence : Lean.Option Bool
-- Mathlib.Algebra.Polynomial.Basic
Polynomial.addHom_ext : ∀ {R : Type u} [inst : Semiring R] {M : Type u_1} [inst_1 : AddZeroClass M] {f g : Polynomial R →+ M},
  (∀ (n : ℕ) (a : R), f ((Polynomial.monomial n) a) = g ((Polynomial.monomial n) a)) → f = g
-- Mathlib.Algebra.Order.Monoid.Unbundled.Units
Units.inv_le_one : ∀ {M : Type u_1} [inst : Monoid M] [inst_1 : LE M] [MulLeftMono M] (u : Mˣ), ↑u⁻¹ ≤ 1 ↔ 1 ≤ ↑u
-- Mathlib.Algebra.DirectSum.Module
DirectSum.IsInternal.addSubgroup_iSupIndep : ∀ {ι : Type v} [dec_ι : DecidableEq ι] {G : Type u_2} [inst : AddCommGroup G] {A : ι → AddSubgroup G},
  DirectSum.IsInternal A → iSupIndep A
-- Mathlib.Algebra.Ring.Subring.Basic
/-- If all elements of `s : Set R` commute pairwise, then `closure s` is a commutative ring.  -/
Subring.isMulCommutative_closure : ∀ {R : Type u_1} [inst : Ring R] {s : Set R}, (∀ x ∈ s, ∀ y ∈ s, x * y = y * x) → IsMulCommutative ↥(Subring.closure s)
-- Std.Data.DTreeMap.Basic
Std.DTreeMap.empty_eq_emptyc : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering}, Std.DTreeMap.empty = ∅
-- Mathlib.SetTheory.Cardinal.Order
Cardinal.out_embedding : ∀ {c c' : Cardinal.{u_1}}, c ≤ c' ↔ Nonempty (Quotient.out c ↪ Quotient.out c')
-- Mathlib.CategoryTheory.Preadditive.Biproducts
CategoryTheory.Limits.biproduct.matrix_map_assoc : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Preadditive C] {J K : Type}
  [inst_2 : Finite J] [inst_3 : CategoryTheory.Limits.HasFiniteBiproducts C] [inst_4 : Finite K] {f : J → C}
  {g h : K → C} (m : (j : J) → (k : K) → f j ⟶ g k) (n : (k : K) → g k ⟶ h k) {Z : C} (h_1 : ⨁ h ⟶ Z),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.biproduct.matrix m)
      (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.biproduct.map n) h_1) =
    CategoryTheory.CategoryStruct.comp
      (CategoryTheory.Limits.biproduct.matrix fun j k => CategoryTheory.CategoryStruct.comp (m j k) (n k)) h_1
-- Init.Data.String.Lemmas.Pattern.Pred
String.Slice.Pos.revSkipWhile_prop_eq_revSkipWhile_decide : ∀ {p : Char → Prop} [inst : DecidablePred p] {s : String.Slice} (curr : s.Pos),
  curr.revSkipWhile p = curr.revSkipWhile fun x => decide (p x)
-- Mathlib.Tactic.CategoryTheory.Monoidal.Normalize
Mathlib.Tactic.Monoidal.evalWhiskerLeft_nil : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.MonoidalCategory C] (f : C) {g h : C}
  (α : g ≅ h),
  (CategoryTheory.MonoidalCategory.whiskerLeftIso f α).hom = (CategoryTheory.MonoidalCategory.whiskerLeftIso f α).hom
-- Lean.CoreM
Lean.Core.setMessageLog : Lean.MessageLog → Lean.CoreM Unit
-- Mathlib.ModelTheory.Substructures
FirstOrder.Language.Substructure.comap_iSup_map_of_injective : ∀ {L : FirstOrder.Language} {M : Type w} {N : Type u_1} [inst : L.Structure M] [inst_1 : L.Structure N] {ι : Type u_3}
  {f : L.Hom M N},
  Function.Injective ⇑f →
    ∀ (S : ι → L.Substructure M),
      FirstOrder.Language.Substructure.comap f (⨆ i, FirstOrder.Language.Substructure.map f (S i)) = ⨆ i, S i
-- Init.Data.String.Iterate
_private.Init.Data.String.Iterate.0.String.Slice.ByteIterator.finitenessRelation : {m : Type → Type u_1} → [inst : Pure m] → Std.Iterators.FinitenessRelation String.Slice.ByteIterator m
-- Mathlib.Order.Copy
Lattice.copy.congr_simp : ∀ {α : Type u} (c c_1 : Lattice α) (e_c : c = c_1) (le le_1 : α → α → Prop) (e_le : le = le_1) (eq_le : le = LE.le)
  (sup sup_1 : α → α → α) (e_sup : sup = sup_1) (eq_sup : sup = max) (inf inf_1 : α → α → α) (e_inf : inf = inf_1)
  (eq_inf : inf = min), c.copy le eq_le sup eq_sup inf eq_inf = c_1.copy le_1 ⋯ sup_1 ⋯ inf_1 ⋯
-- Mathlib.Data.PFun
PFun.mem_toSubtype_iff : ∀ {α : Type u_1} {β : Type u_2} {p : β → Prop} {f : α → β} {a : α} {b : Subtype p}, b ∈ PFun.toSubtype p f a ↔ ↑b = f a
-- Mathlib.Analysis.LocallyConvex.WeakOperatorTopology
ContinuousLinearMapWOT.instContinuousSMul : ∀ {𝕜₁ : Type u_1} {𝕜₂ : Type u_2} [inst : NormedField 𝕜₁] [inst_1 : NormedField 𝕜₂] {σ : 𝕜₁ →+* 𝕜₂} {E : Type u_3}
  {F : Type u_4} [inst_2 : AddCommGroup E] [inst_3 : TopologicalSpace E] [inst_4 : Module 𝕜₁ E]
  [inst_5 : AddCommGroup F] [inst_6 : TopologicalSpace F] [inst_7 : Module 𝕜₂ F] [inst_8 : IsTopologicalAddGroup F]
  [inst_9 : ContinuousConstSMul 𝕜₂ F] {S : Type u_5} [inst_10 : Semiring S] [inst_11 : Module S F]
  [inst_12 : SMulCommClass 𝕜₂ S F] [inst_13 : Module S 𝕜₂] [IsScalarTower S 𝕜₂ F] [IsScalarTower S 𝕜₂ 𝕜₂]
  [inst_16 : ContinuousConstSMul S F] [inst_17 : TopologicalSpace S] [ContinuousSMul S 𝕜₂],
  ContinuousSMul S (E →SWOT[σ] F)
-- Mathlib.Algebra.Ring.Periodic
Function.Antiperiodic.funext : ∀ {α : Type u_1} {β : Type u_2} {f : α → β} {c : α} [inst : Add α] [inst_1 : Neg β],
  Function.Antiperiodic f c → (fun x => f (x + c)) = -f
-- Mathlib.Analysis.Meromorphic.LogDeriv
/-- Eta-expanded form of `MeromorphicOn.logDeriv_mul_eventuallyEq`

---

The logarithmic derivative converts products into sums: away from a codiscrete subset of `U`, the
logarithmic derivative of a product of two meromorphic functions is the sum of the logarithmic
derivatives.
 -/
MeromorphicOn.logDeriv_fun_mul_eventuallyEq : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {𝕜' : Type u_2} [inst_1 : NontriviallyNormedField 𝕜']
  [inst_2 : NormedAlgebra 𝕜 𝕜'] {f g : 𝕜 → 𝕜'} {U : Set 𝕜},
  MeromorphicOn f U →
    MeromorphicOn g U →
      (∀ x ∈ U, meromorphicOrderAt f x ≠ ⊤) →
        (∀ x ∈ U, meromorphicOrderAt g x ≠ ⊤) →
          (logDeriv fun i => f i * g i) =ᶠ[Filter.codiscreteWithin U] fun i => logDeriv f i + logDeriv g i
-- Mathlib.Order.Filter.Pointwise
Filter.top_add_of_nonneg : ∀ {α : Type u_2} [inst : AddMonoid α] {f : Filter α}, 0 ≤ f → ⊤ + f = ⊤
-- Mathlib.Algebra.BigOperators.Fin
/-- A sum of a function `f : Fin 0 → M` is `0` because `Fin 0` is empty  -/
Fin.sum_univ_zero : ∀ {M : Type u_2} [inst : AddCommMonoid M] (f : Fin 0 → M), ∑ i, f i = 0
-- Mathlib.MeasureTheory.Integral.IntegralEqImproper
MeasureTheory.integrableOn_comp_exp_Ioi : ∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] (g : ℝ → E) (a : ℝ),
  MeasureTheory.IntegrableOn (fun x => Real.exp x • g (Real.exp x)) (Set.Ioi a) MeasureTheory.volume ↔
    MeasureTheory.IntegrableOn g (Set.Ioi (Real.exp a)) MeasureTheory.volume
-- Mathlib.Algebra.Quaternion
Quaternion.imI_one : ∀ {R : Type u_3} [inst : CommRing R], QuaternionAlgebra.imI 1 = 0
-- Mathlib.Logic.Equiv.Basic
Equiv.Perm.extendDomain_refl : ∀ {α' : Type u_9} {β' : Type u_10} {p : β' → Prop} [inst : DecidablePred p] (f : α' ≃ Subtype p),
  Equiv.Perm.extendDomain (Equiv.refl α') f = Equiv.refl β'
-- Batteries.Data.List.Basic
List.Forall₂.below : {α : Type u_1} →
  {β : Type u_2} →
    {R : α → β → Prop} →
      {motive : (a : List α) → (a_1 : List β) → List.Forall₂ R a a_1 → Prop} →
        {a : List α} → {a_1 : List β} → List.Forall₂ R a a_1 → Prop
-- Mathlib.CategoryTheory.Groupoid
/-- A `Groupoid` is a category such that all morphisms are isomorphisms.  -/
CategoryTheory.Groupoid : Type u → Type (max u (v + 1))
-- Mathlib.Logic.Encodable.Basic
_private.Mathlib.Logic.Encodable.Basic.0.Encodable.good.match_1.eq_2 : ∀ {α : Type u_1} (motive : Option α → Sort u_2) (h_1 : (a : α) → motive (some a)) (h_2 : Unit → motive none),
  (match none with
    | some a => h_1 a
    | none => h_2 ()) =
    h_2 ()
-- Mathlib.Computability.TuringMachine.Tape
Turing.BlankExtends.refl : ∀ {Γ : Type u_1} [inst : Inhabited Γ] (l : List Γ), Turing.BlankExtends l l
-- Mathlib.Algebra.Category.ModuleCat.Semi
SemimoduleCat.isZero_of_iff_subsingleton : ∀ {R : Type u} [inst : Semiring R] {M : Type u_1} [inst_1 : AddCommMonoid M] [inst_2 : Module R M],
  CategoryTheory.Limits.IsZero (SemimoduleCat.of R M) ↔ Subsingleton M
-- Mathlib.CategoryTheory.Limits.Shapes.Images
/-- `image.preComp f g` is an isomorphism when `f` is an isomorphism
(we need `C` to have equalizers to prove this).
 -/
CategoryTheory.Limits.image.isIso_precomp_iso : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {X Y Z : C} (g : Y ⟶ Z) [CategoryTheory.Limits.HasEqualizers C]
  (f : X ⟶ Y) [inst_2 : CategoryTheory.IsIso f] [inst_3 : CategoryTheory.Limits.HasImage g],
  CategoryTheory.IsIso (CategoryTheory.Limits.image.preComp f g)
-- Mathlib.Order.WithBot
WithTop.coe_lt_coe : ∀ {α : Type u_1} {a b : α} [inst : LT α], ↑b < ↑a ↔ b < a
-- Init.Data.Array.Lemmas
Array.findSomeRev?_eq_findSome?_reverse : ∀ {α : Type u_1} {β : Type u_2} {f : α → Option β} {xs : Array α},
  Array.findSomeRev? f xs = Array.findSome? f xs.reverse
-- Mathlib.Analysis.Real.Hyperreal
Hyperreal.neg_lt_of_tendsto_zero_of_pos : ∀ {f : ℕ → ℝ}, Filter.Tendsto f Filter.atTop (nhds 0) → ∀ {r : ℝ}, 0 < r → -↑r < Hyperreal.ofSeq f
-- Mathlib.Order.Interval.Set.Basic
Set.Ico_sdiff_Ioo_same : ∀ {α : Type u_1} [inst : PartialOrder α] {a b : α}, a < b → Set.Ico a b \ Set.Ioo a b = {a}
-- Mathlib.CategoryTheory.MorphismProperty.Representable
CategoryTheory.Functor.relativelyRepresentable.lift'_fst_assoc : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  {F : CategoryTheory.Functor C D} {Y : D} {b : C} {f' : F.obj b ⟶ Y} (hf' : F.relativelyRepresentable f') {a : C}
  {g : F.obj a ⟶ Y} {c : C} (i : c ⟶ b) (h : c ⟶ a)
  (hi : CategoryTheory.CategoryStruct.comp (F.map i) f' = CategoryTheory.CategoryStruct.comp (F.map h) g)
  [inst_2 : F.Full] [F.Faithful] {Z : C} (h_1 : b ⟶ Z),
  CategoryTheory.CategoryStruct.comp (hf'.lift' i h hi) (CategoryTheory.CategoryStruct.comp (hf'.fst' g) h_1) =
    CategoryTheory.CategoryStruct.comp i h_1
-- Mathlib.LinearAlgebra.Matrix.Determinant.TotallyUnimodular
Matrix.fromRows_replicateRow0_isTotallyUnimodular_iff : ∀ {m : Type u_1} {m' : Type u_2} {n : Type u_3} {R : Type u_5} [inst : CommRing R] (A : Matrix m n R),
  (A.fromRows (Matrix.replicateRow m' 0)).IsTotallyUnimodular ↔ A.IsTotallyUnimodular
-- Mathlib.Data.Fin.Tuple.Take
/-- Version of `take_addCases_right` that specializes `addCases` to `append`.  -/
Fin.take_append_right : ∀ {n n' : ℕ} {α : Sort u_2} (m : ℕ) (h : m ≤ n') (u : Fin n → α) (v : Fin n' → α),
  Fin.take (n + m) ⋯ (Fin.append u v) = Fin.append u (Fin.take m h v)
-- Init.Grind.Ring.CommSolver
Lean.Grind.CommRing.Mon.denote'_eq_denote : ∀ {α : Type u_1} [inst : Lean.Grind.Semiring α] (ctx : Lean.Grind.CommRing.Context α) (m : Lean.Grind.CommRing.Mon),
  Lean.Grind.CommRing.Mon.denote' ctx m = Lean.Grind.CommRing.Mon.denote ctx m
-- Lean.Parser.Basic
/-- The `atomic(p)` parser parses `p`, returns the same result as `p` and fails iff `p` fails,
but if `p` fails after consuming some tokens `atomic(p)` will fail without consuming tokens.
This is important for the `p <|> q` combinator, because it is not backtracking, and will fail if
`p` fails after consuming some tokens. To get backtracking behavior, use `atomic(p) <|> q` instead.

This parser has the same arity as `p` - it produces the same result as `p`.  -/
Lean.Parser.atomic : Lean.Parser.Parser → Lean.Parser.Parser
-- Init.Data.UInt.Bitwise
UInt8.toUInt16_and : ∀ (a b : UInt8), (a &&& b).toUInt16 = a.toUInt16 &&& b.toUInt16
-- Mathlib.Algebra.Group.Subgroup.Map
AddSubgroup.comap_id : ∀ {N : Type u_5} [inst : AddGroup N] (K : AddSubgroup N), AddSubgroup.comap (AddMonoidHom.id N) K = K
-- Lean.Server.References
Lean.Server.instToJsonIlean : Lean.ToJson Lean.Server.Ilean
-- Mathlib.Topology.MetricSpace.GromovHausdorffRealized
/-- We will then choose the candidate minimizing the Hausdorff distance. Except that we are not
in a metric space setting, so we need to define our custom version of Hausdorff distance,
called `HD`, and prove its basic properties.  -/
GromovHausdorff.HD : {X : Type u} → {Y : Type v} → [inst : MetricSpace X] → [inst_1 : MetricSpace Y] → GromovHausdorff.Cb✝ X Y → ℝ
-- Std.Internal.Do.Order.Basic
Lean.Order.instCompleteLatticeProp_std : Lean.Order.CompleteLattice Prop
-- Mathlib.CategoryTheory.FinCategory.AsType
/-- The "identity" functor from `AsType α` to `ObjAsType α`.  -/
CategoryTheory.FinCategory.asTypeToObjAsType : (α : Type u_1) →
  [inst : Fintype α] →
    [inst_1 : CategoryTheory.SmallCategory α] →
      [inst_2 : CategoryTheory.FinCategory α] →
        CategoryTheory.Functor (CategoryTheory.FinCategory.AsType α) (CategoryTheory.FinCategory.ObjAsType α)
-- Mathlib.SetTheory.Ordinal.Notation
/-- Compare ordinal notations  -/
NONote.cmp : NONote → NONote → Ordering
-- Mathlib.Algebra.Category.ModuleCat.Adjunctions
ModuleCat.instIsRightAdjointForgetLinearMapIdCarrier : ∀ (R : Type u) [inst : Ring R], (CategoryTheory.forget (ModuleCat R)).IsRightAdjoint
-- Mathlib.GroupTheory.Nilpotent
Subgroup.upperCentralSeries_mono : ∀ (G : Type u_1) [inst : Group G], Monotone (Subgroup.upperCentralSeries G)
-- Lean.Parser.Command
Lean.Parser.Command.computedField : Lean.Parser.Parser
-- Mathlib.SetTheory.Lists
Lists.isList_of_mem : ∀ {α : Type u_1} {a l : Lists α}, a ∈ l → l.IsList
-- Lean.Meta.Match.Basic
Lean.Meta.Match.Pattern.var.sizeOf_spec : ∀ (fvarId : Lean.FVarId), sizeOf (Lean.Meta.Match.Pattern.var fvarId) = 1 + sizeOf fvarId
-- Mathlib.RingTheory.Polynomial.Bernstein
bernsteinPolynomial.iterate_derivative_at_0 : ∀ (R : Type u_1) [inst : CommRing R] (n ν : ℕ),
  Polynomial.eval 0 ((⇑Polynomial.derivative)^[ν] (bernsteinPolynomial R n ν)) =
    Polynomial.eval (↑(n - (ν - 1))) (ascPochhammer R ν)
-- Mathlib.Algebra.Module.Presentation.DirectSum
Module.Relations.Solution.directSum_var : ∀ {A : Type u} [inst : Ring A] {ι : Type w} [inst_1 : DecidableEq ι] {relations : ι → Module.Relations A}
  {M : ι → Type v} [inst_2 : (i : ι) → AddCommGroup (M i)] [inst_3 : (i : ι) → Module A (M i)]
  (solution : (i : ι) → (relations i).Solution (M i)) (i : ι) (g : (relations i).G),
  (Module.Relations.Solution.directSum solution).var ⟨i, g⟩ = (DirectSum.lof A ι M i) ((solution i).var g)
-- Batteries.CodeAction.Match
/-- Computes for a constructor, if it makes sense to use `@constr` in a match, by determining
if it has any non-parameter implicit arguments.  -/
Batteries.CodeAction.hasImplicitNonparArg : Lean.Name → Lean.Environment → Bool
-- Mathlib.Data.Num.Prime
PosNum.minFac.eq_2 : ∀ (a : PosNum), a.bit0.minFac = 2
-- Mathlib.MeasureTheory.Measure.Prod
/-- The Lebesgue integral is measurable. This shows that the integrand of (the right-hand-side of)
the symmetric version of Tonelli's theorem is measurable.
This version has the argument `f` in curried form.  -/
Measurable.lintegral_prod_left : ∀ {α : Type u_1} {β : Type u_2} [inst : MeasurableSpace α] [inst_1 : MeasurableSpace β] {μ : MeasureTheory.Measure α}
  [MeasureTheory.SFinite μ] {f : α → β → ENNReal},
  Measurable (Function.uncurry f) → Measurable fun y => ∫⁻ (x : α), f x y ∂μ
-- Mathlib.CategoryTheory.Localization.SmallHom
/-- The action of a localizer morphism on `SmallHom`.  -/
CategoryTheory.LocalizerMorphism.smallHomMap : {C₁ : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C₁] →
    {W₁ : CategoryTheory.MorphismProperty C₁} →
      {C₂ : Type u₂} →
        [inst_1 : CategoryTheory.Category.{v₂, u₂} C₂] →
          {W₂ : CategoryTheory.MorphismProperty C₂} →
            (Φ : CategoryTheory.LocalizerMorphism W₁ W₂) →
              {X Y : C₁} →
                [inst_2 : CategoryTheory.Localization.HasSmallLocalizedHom W₁ X Y] →
                  [inst_3 : CategoryTheory.Localization.HasSmallLocalizedHom W₂ (Φ.functor.obj X) (Φ.functor.obj Y)] →
                    CategoryTheory.Localization.SmallHom W₁ X Y →
                      CategoryTheory.Localization.SmallHom W₂ (Φ.functor.obj X) (Φ.functor.obj Y)
-- Mathlib.Algebra.Lie.SkewAdjoint
LieEquiv.ofSubalgebras.congr_simp : ∀ {R : Type u} {L₁ : Type v} {L₂ : Type w} [inst : CommRing R] [inst_1 : LieRing L₁] [inst_2 : LieRing L₂]
  [inst_3 : LieAlgebra R L₁] [inst_4 : LieAlgebra R L₂] (L₁' : LieSubalgebra R L₁) (L₂' : LieSubalgebra R L₂)
  (e e_1 : L₁ ≃ₗ⁅R⁆ L₂) (e_e : e = e_1) (h : LieSubalgebra.map e.toLieHom L₁' = L₂'),
  LieEquiv.ofSubalgebras L₁' L₂' e h = LieEquiv.ofSubalgebras L₁' L₂' e_1 ⋯