mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Analysis.Convex.Basic
convex_iInter₂ : ∀ {𝕜 : Type u_1} {E : Type u_2} [inst : Semiring 𝕜] [inst_1 : PartialOrder 𝕜] [inst_2 : AddCommMonoid E]
  [inst_3 : SMul 𝕜 E] {ι : Sort u_5} {κ : ι → Sort u_6} {s : (i : ι) → κ i → Set E},
  (∀ (i : ι) (j : κ i), Convex 𝕜 (s i j)) → Convex 𝕜 (⋂ i, ⋂ j, s i j)
-- Init.Data.Array.QSort.Basic
_private.Init.Data.Array.QSort.Basic.0.Array.qsort.match_8.splitter : {α : Type u_1} →
  {n : ℕ} →
    (lo hi : ℕ) →
      (motive : { m // lo ≤ m ∧ m ≤ hi } × Vector α n → Sort u_2) →
        (x : { m // lo ≤ m ∧ m ≤ hi } × Vector α n) →
          ((mid : ℕ) → (hmid : lo ≤ mid ∧ mid ≤ hi) → (as : Vector α n) → motive (⟨mid, hmid⟩, as)) → motive x
-- Init.Data.BitVec.Lemmas
BitVec.toInt_umod : ∀ {w : ℕ} {x y : BitVec w}, (x % y).toInt = (↑x.toNat % ↑y.toNat).bmod (2 ^ w)
-- Init.Data.Int.DivMod.Lemmas
Int.fdiv_neg : ∀ {a b : ℤ}, b ≠ 0 → a.fdiv (-b) = if b ∣ a then -a.fdiv b else -a.fdiv b - 1
-- Std.Data.DTreeMap.Lemmas
Std.DTreeMap.Const.equiv_iff_keys_unit_eq : ∀ {α : Type u} {cmp : α → α → Ordering} [Std.TransCmp cmp] {t₁ t₂ : Std.DTreeMap α (fun x => Unit) cmp},
  t₁.Equiv t₂ ↔ t₁.keys = t₂.keys
-- Init.Data.BitVec.Bitblast
/-- `shiftLeftRec x y n` shifts `x` to the left by the first `n` bits of `y`.
 -/
BitVec.shiftLeftRec_eq : ∀ {w₁ w₂ : ℕ} {x : BitVec w₁} {y : BitVec w₂} {n : ℕ},
  x.shiftLeftRec y n = x <<< BitVec.setWidth w₂ (BitVec.setWidth (n + 1) y)
-- Std.Data.TreeMap.Lemmas
Std.TreeMap.ofList_eq_insertMany_empty : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {l : List (α × β)}, Std.TreeMap.ofList l cmp = ∅.insertMany l
-- Init.Data.Ord.Array
List.compareLex_eq_compareLex_toArray : ∀ {α : Type u_1} {cmp : α → α → Ordering} {l₁ l₂ : List α},
  List.compareLex cmp l₁ l₂ = Array.compareLex cmp l₁.toArray l₂.toArray
-- Mathlib.RingTheory.Valuation.Integers
/-- The `v.integer`-submodule of `R` of elements whose valuation is less than or equal to a
certain value.  -/
Valuation.leSubmodule : {R : Type u} →
  {Γ₀ : Type v} →
    [inst : Ring R] →
      [inst_1 : LinearOrderedCommGroupWithZero Γ₀] → (v : Valuation R Γ₀) → Γ₀ → Submodule (↥v.integer) R
-- Lean.ToLevel
/-- A hack to avoid the "unused universe parameter" error.
We can remove this field pending issue https://github.com/leanprover/lean4/issues/2116  -/
Lean.ToLevel.univ : ∀ [self : Lean.ToLevel] (x : Sort u), True
-- Mathlib.Combinatorics.SimpleGraph.Basic
/-- A variant of the `aesop` tactic for use in the graph library. Changes relative
to standard `aesop`:

- We use the `SimpleGraph` rule set in addition to the default rule sets.
- We instruct Aesop's `intro` rule to unfold with `default` transparency.
- We instruct Aesop to fail if it can't fully solve the goal. This allows us to
  use `aesop_graph` for auto-params.
 -/
aesop_graph : Lean.ParserDescr
-- Batteries.Data.Fin.Lemmas
Fin.get_find?_minimal : ∀ {n : ℕ} {p : Fin n → Bool} (h : (Fin.find? p).isSome = true), ∀ j < (Fin.find? p).get h, p j = false
-- Mathlib.Algebra.Polynomial.Basic
Polynomial.ofFinsupp_one : ∀ {R : Type u} [inst : Semiring R], { toFinsupp := 1 } = 1
-- Mathlib.AlgebraicGeometry.EllipticCurve.Affine.Formula
WeierstrassCurve.Affine.negAddY.eq_1 : ∀ {R : Type r} [inst : CommRing R] (W' : WeierstrassCurve.Affine R) (x₁ x₂ y₁ ℓ : R),
  W'.negAddY x₁ x₂ y₁ ℓ = ℓ * (W'.addX x₁ x₂ ℓ - x₁) + y₁
-- Lean.Meta.LazyDiscrTree
Lean.Meta.LazyDiscrTree.PreDiscrTree.mk.sizeOf_spec : ∀ {α : Type} [inst : SizeOf α] (roots : Std.HashMap Lean.Meta.LazyDiscrTree.Key ℕ)
  (tries : Array (Array (Lean.Meta.LazyDiscrTree.LazyEntry α))),
  sizeOf { roots := roots, tries := tries } = 1 + sizeOf roots + sizeOf tries
-- Mathlib.Order.Concept
upperPolar_iUnion₂ : ∀ {ι : Sort u_1} {α : Type u_2} {β : Type u_3} {κ : ι → Sort u_5} (r : α → β → Prop) (f : (i : ι) → κ i → Set α),
  upperPolar r (⋃ i, ⋃ j, f i j) = ⋂ i, ⋂ j, upperPolar r (f i j)
-- Init.Data.Array.Count
Array.one_le_countP_iff : ∀ {α : Type u_1} {xs : Array α} {p : α → Bool}, 1 ≤ Array.countP p xs ↔ ∃ a ∈ xs, p a = true
-- Std.Data.TreeMap.Basic
/-- Tries to retrieve the largest key that is less than or equal to the
given key, returning `fallback` if no such key exists.
 -/
Std.TreeMap.getKeyLED : {α : Type u} → {β : Type v} → {cmp : α → α → Ordering} → Std.TreeMap α β cmp → α → α → α
-- Lean.Elab.ConfigEval.Basic
/-- Default `onErr` handler. If the `cfgItem` contains `.missing`, we assume an error has already been
reported by the parser and return `cfg`. Otherwise, we throw an unsupported syntax exception.

If `cfgType?` is present, then it adds completion info when the identifier is missing.
 -/
Lean.Elab.ConfigEval.EvalConfigItem.defaultOnErr : {α : Type} → α → Lean.Syntax → optParam (Option Lean.Expr) none → Lean.Elab.TermElabM α
-- Init.Core
ForInStep.done.injEq : ∀ {α : Type u} (a a_1 : α), (ForInStep.done a = ForInStep.done a_1) = (a = a_1)
-- Mathlib.Dynamics.BirkhoffSum.NormedSpace
/-- If `f` is a non-strictly contracting map (i.e., it is Lipschitz with constant `1`)
and `g` is a uniformly continuous, then the Birkhoff averages of `g` along orbits of `f`
is a uniformly equicontinuous family of functions.  -/
uniformEquicontinuous_birkhoffAverage : ∀ (𝕜 : Type u_1) {X : Type u_2} {E : Type u_3} [inst : PseudoEMetricSpace X] [inst_1 : RCLike 𝕜]
  [inst_2 : NormedAddCommGroup E] [inst_3 : NormedSpace 𝕜 E] {f : X → X} {g : X → E},
  LipschitzWith 1 f → UniformContinuous g → UniformEquicontinuous (birkhoffAverage 𝕜 f g)
-- Mathlib.RingTheory.DividedPowers.Basic
DividedPowers.dpow_linearCombination : ∀ {A : Type u_1} [inst : CommSemiring A] {ι : Type u_2} [inst_1 : DecidableEq ι] {S : Type u_3}
  [inst_2 : CommSemiring S] [inst_3 : Algebra A S] {J : Ideal S} (hJ : DividedPowers J) {b : ι → S} {x : ι →₀ A},
  (∀ i ∈ x.support, b i ∈ J) →
    ∀ {n : ℕ},
      hJ.dpow n (x.sum fun i r => r • b i) =
        ∑ k ∈ x.support.sym n, x.prod fun i r => r ^ Multiset.count i ↑k • hJ.dpow (Multiset.count i ↑k) (b i)
-- Mathlib.Analysis.Calculus.ContDiff.FaaDiBruno
/-- Bundled version of `compAlongOrderedFinpartition`, depending continuously linearly on `f`
and continuously multilinearly on `p`.  -/
OrderedFinpartition.compAlongOrderedFinpartitionL : (𝕜 : 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] →
                (G : Type u_4) →
                  [inst_5 : NormedAddCommGroup G] →
                    [inst_6 : NormedSpace 𝕜 G] →
                      {n : ℕ} →
                        (c : OrderedFinpartition n) →
                          (F [×c.length]→L[𝕜] G) →L[𝕜] (E [×c.partSize i]→L[𝕜] F) [×c.length]→L[𝕜] E [×n]→L[𝕜] G
-- Mathlib.GroupTheory.SpecificGroups.Cyclic.Basic
/-- Any non-identity element of a finite group of prime order generates the group.  -/
zmultiples_eq_top_of_prime_card : ∀ {G : Type u_2} [inst : AddGroup G] {p : ℕ} [hp : Fact (Nat.Prime p)],
  Nat.card G = p → ∀ {g : G}, g ≠ 0 → AddSubgroup.zmultiples g = ⊤
-- Aesop.RuleTac.Descr
Aesop.RuleTacDescr.forwardMatches.injEq : ∀ (ms ms_1 : Array Aesop.ForwardRuleMatch),
  (Aesop.RuleTacDescr.forwardMatches ms = Aesop.RuleTacDescr.forwardMatches ms_1) = (ms = ms_1)
-- Init.Data.List.Lemmas
List.getElem?_cons_zero : ∀ {α : Type u_1} {a : α} {l : List α}, (a :: l)[0]? = some a
-- Mathlib.Topology.MetricSpace.Closeds
/-- The range of `NonemptyCompacts.toCloseds` is closed in a complete space  -/
TopologicalSpace.NonemptyCompacts.isClosed_in_closeds : ∀ {α : Type u_1} [inst : EMetricSpace α] [CompleteSpace α],
  IsClosed (Set.range TopologicalSpace.NonemptyCompacts.toCloseds)
-- Mathlib.LinearAlgebra.Matrix.SchurComplement
Matrix.det_fromBlocks_one₂₂ : ∀ {m : Type u_2} {n : Type u_3} {α : Type u_4} [inst : Fintype m] [inst_1 : Fintype n] [inst_2 : DecidableEq m]
  [inst_3 : DecidableEq n] [inst_4 : CommRing α] (A : Matrix m m α) (B : Matrix m n α) (C : Matrix n m α),
  (Matrix.fromBlocks A B C 1).det = (A - B * C).det
-- Mathlib.Algebra.MvPolynomial.Division
MvPolynomial.X_divMonomial : ∀ {σ : Type u_1} {R : Type u_2} [inst : CommSemiring R] (i : σ), ((MvPolynomial.X i).divMonomial fun₀ | i => 1) = 1
-- Mathlib.Algebra.Group.Subgroup.Map
AddSubgroup.top_addSubgroupOf : ∀ {G : Type u_1} [inst : AddGroup G] (H : AddSubgroup G), ⊤.addSubgroupOf H = ⊤
-- Mathlib.Order.Bounds.Image
StrictMono.map_isLeast : ∀ {α : Type u} {β : Type v} [inst : LinearOrder α] [inst_1 : Preorder β] {f : α → β} {a : α} {s : Set α},
  StrictMono f → (IsLeast (f '' s) (f a) ↔ IsLeast s a)
-- Mathlib.LinearAlgebra.ExteriorAlgebra.OfAlternating
ExteriorAlgebra.liftAlternating_one : ∀ {R : Type u_1} {M : Type u_2} {N : Type u_3} [inst : CommRing R] [inst_1 : AddCommGroup M] [inst_2 : AddCommGroup N]
  [inst_3 : Module R M] [inst_4 : Module R N] (f : (i : ℕ) → M [⋀^Fin i]→ₗ[R] N),
  (ExteriorAlgebra.liftAlternating f) 1 = (f 0) 0
-- Lean.Meta.Tactic.Grind.EMatch
_private.Lean.Meta.Tactic.Grind.EMatch.0.Lean.Meta.Grind.EMatch.addNewInstance.go : Lean.Meta.Grind.EMatchTheorem →
  ℕ →
    List Lean.Meta.Grind.TheoremGuard →
      Lean.PHashSet Lean.Meta.Grind.EMatchDiagNode → Lean.Expr → Lean.Expr → Lean.Meta.Grind.EMatch.M Unit
-- Init.Data.String.Lemmas.Iterate
String.Model.mem_positionsFrom : ∀ {s : String} {p : s.Pos} {q : { q // q ≠ s.endPos }}, q ∈ String.Model.positionsFrom p ↔ p ≤ ↑q
-- Mathlib.RingTheory.Int.Basic
Int.sq_of_gcd_eq_one : ∀ {a b c : ℤ}, a.gcd b = 1 → a * b = c ^ 2 → ∃ a0, a = a0 ^ 2 ∨ a = -a0 ^ 2
-- Batteries.Data.BinomialHeap.Basic
Batteries.BinomialHeap.Imp.Heap.findMin.eq_2 : ∀ {α : Type u_1} (le : α → α → Bool) (k : Batteries.BinomialHeap.Imp.Heap α → Batteries.BinomialHeap.Imp.Heap α)
  (x : Batteries.BinomialHeap.Imp.FindMin α) (r : ℕ) (a : α) (c : Batteries.BinomialHeap.Imp.HeapNode α)
  (s : Batteries.BinomialHeap.Imp.Heap α),
  Batteries.BinomialHeap.Imp.Heap.findMin le k (Batteries.BinomialHeap.Imp.Heap.cons r a c s) x =
    Batteries.BinomialHeap.Imp.Heap.findMin le (k ∘ Batteries.BinomialHeap.Imp.Heap.cons r a c) s
      (if le x.val a = true then x else { before := k, val := a, node := c, next := s })
-- Mathlib.GroupTheory.FreeGroup.Basic
FreeGroup.instInhabited : {α : Type u} → Inhabited (FreeGroup α)
-- Mathlib.Algebra.Order.Nonneg.Basic
Nonneg.coe_zero : ∀ {α : Type u_1} [inst : Zero α] [inst_1 : Preorder α], ↑0 = 0
-- Lean.Data.PersistentHashMap
Lean.PersistentHashMap.Stats.numNull : Lean.PersistentHashMap.Stats → ℕ
-- Mathlib.Analysis.Complex.Periodic
Function.Periodic.im_invQParam : ∀ (h : ℝ) (q : ℂ), (Function.Periodic.invQParam h q).im = -h / (2 * Real.pi) * Real.log ‖q‖
-- Init.Data.List.Sort.Impl
_private.Init.Data.List.Sort.Impl.0.List.MergeSort.Internal.mergeSortTR₂.run' : {α : Type u_1} → (α → α → Bool) → {n : ℕ} → { l // l.length = n } → List α
-- ProofWidgets.Presentation.Expr
ProofWidgets.ExprPresentationData : Type
-- Mathlib.Analysis.ODE.Gronwall
hasDerivAt_gronwallBound : ∀ (δ K ε x : ℝ), HasDerivAt (gronwallBound δ K ε) (K * gronwallBound δ K ε x + ε) x
-- Mathlib.Geometry.Euclidean.Sphere.Power
/-- **Intersecting Secants Theorem**.  -/
EuclideanGeometry.mul_dist_eq_mul_dist_of_cospherical_of_angle_eq_zero : ∀ {V : Type u_1} [inst : NormedAddCommGroup V] [inst_1 : InnerProductSpace ℝ V] {P : Type u_2} [inst_2 : MetricSpace P]
  [inst_3 : NormedAddTorsor V P] {a b c d p : P},
  EuclideanGeometry.Cospherical {a, b, c, d} →
    a ≠ b →
      c ≠ d →
        EuclideanGeometry.angle a p b = 0 →
          EuclideanGeometry.angle c p d = 0 → dist a p * dist b p = dist c p * dist d p
-- Init.Data.UInt.BasicAux
Fin.ofNat.eq_1 : ∀ (n : ℕ) [inst : NeZero n] (a : ℕ), Fin.ofNat n a = ⟨a % n, ⋯⟩
-- Std.Data.ExtDTreeMap.Basic
/-- Tries to retrieve the key-value pair with the largest key in the tree map, returning `fallback` if
the tree map is empty.
 -/
Std.ExtDTreeMap.maxEntryD : {α : Type u} →
  {β : α → Type v} →
    {cmp : α → α → Ordering} → [Std.TransCmp cmp] → Std.ExtDTreeMap α β cmp → (a : α) × β a → (a : α) × β a
-- Lean.Meta.Tactic.LibrarySearch
/-- Process-global cache for star-indexed lemmas (see `ext`); used as a fallback when primary search
finds nothing for fvar-headed goals.  -/
_private.Lean.Meta.Tactic.LibrarySearch.0.Lean.Meta.LibrarySearch.starLemmasExt : IO.Ref (Option (Array (Lean.Name × Lean.Meta.LibrarySearch.DeclMod)))
-- Mathlib.Order.MinMax
/-- For elements `a` and `b` of a linear order, either `min a b = a` and `a ≤ b`,
or `min a b = b` and `b < a`.
Use cases on this lemma to automate linarith in inequalities  -/
min_cases : ∀ {α : Type u} [inst : LinearOrder α] (a b : α), min a b = a ∧ a ≤ b ∨ min a b = b ∧ b < a
-- Init.Data.List.Lemmas
List.getElem_insert : ∀ {α : Type u_1} [inst : BEq α] [inst_1 : LawfulBEq α] {l : List α} {a : α} {i : ℕ} (h : i < l.length),
  (List.insert a l)[i] = if a ∈ l then l[i] else if i = 0 then a else l[i - 1]
-- Mathlib.Topology.GDelta.Basic
/-- The empty set is meagre.  -/
IsMeagre.empty : ∀ {X : Type u_1} [inst : TopologicalSpace X], IsMeagre ∅
-- Mathlib.Topology.ContinuousMap.BoundedCompactlySupported
compactlySupported_eq_top : ∀ {α : Type u_1} {γ : Type u_2} [inst : TopologicalSpace α] [inst_1 : NonUnitalNormedRing γ] [CompactSpace α],
  compactlySupported α γ = ⊤
-- Mathlib.CategoryTheory.Abelian.Injective.Resolution
CategoryTheory.InjectiveResolution.ofCocomplex_exactAt_succ : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Abelian C]
  [inst_2 : CategoryTheory.EnoughInjectives C] (Z : C) (n : ℕ),
  HomologicalComplex.ExactAt (CategoryTheory.InjectiveResolution.ofCocomplex Z) (n + 1)
-- Mathlib.Algebra.Homology.TotalComplexShift
HomologicalComplex₂.totalShift₂Iso_hom_naturality : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Preadditive C]
  {K L : HomologicalComplex₂ C (ComplexShape.up ℤ) (ComplexShape.up ℤ)} (f : K ⟶ L) (y : ℤ)
  [inst_2 : K.HasTotal (ComplexShape.up ℤ)] [inst_3 : L.HasTotal (ComplexShape.up ℤ)],
  CategoryTheory.CategoryStruct.comp
      (HomologicalComplex₂.total.map ((HomologicalComplex₂.shiftFunctor₂ C y).map f) (ComplexShape.up ℤ))
      (L.totalShift₂Iso y).hom =
    CategoryTheory.CategoryStruct.comp (K.totalShift₂Iso y).hom
      ((CategoryTheory.shiftFunctor (HomologicalComplex C (ComplexShape.up ℤ)) y).map
        (HomologicalComplex₂.total.map f (ComplexShape.up ℤ)))
-- Init.Grind.Lemmas
Lean.Grind.Bool.and_eq_of_eq_true_right : ∀ {a b : Bool}, b = true → (a && b) = a
-- Mathlib.Topology.ContinuousMap.ContinuousMapZero
ContinuousMapZero.range_toContinuousMap : ∀ {X : Type u_1} {R : Type u_3} [inst : Zero X] [inst_1 : Zero R] [inst_2 : TopologicalSpace X]
  [inst_3 : TopologicalSpace R], Set.range toContinuousMap = {f | f 0 = 0}
-- Mathlib.Topology.Order.OrderClosed
/-- The set of antitone functions on a set is closed.  -/
isClosed_antitoneOn : ∀ {α : Type u} {β : Type v} [inst : TopologicalSpace α] [inst_1 : Preorder α] [t : OrderClosedTopology α]
  [inst_2 : Preorder β] {s : Set β}, IsClosed {f | AntitoneOn f s}
-- Mathlib.NumberTheory.EllipticDivisibilitySequence
preNormEDS'.eq_3 : ∀ {R : Type u_1} [inst : CommRing R] (b c d : R), preNormEDS' b c d 2 = 1
-- Init.Data.String.Slice
/-- Checks whether `s1 == s2` if ASCII upper/lowercase are ignored.
 -/
String.Slice.eqIgnoreAsciiCase : String.Slice → String.Slice → Bool
-- Lean.Data.Lsp.Window
Lean.Lsp.MessageType.log : Lean.Lsp.MessageType
-- Mathlib.RingTheory.DedekindDomain.Factorization
FractionalIdeal.divMod_zero_of_not_le : ∀ {R : Type u_1} [inst : CommRing R] {K : Type u_2} [inst_1 : Field K] [inst_2 : Algebra R K]
  [inst_3 : IsFractionRing R K] [inst_4 : IsDedekindDomain R] {a b c : FractionalIdeal (nonZeroDivisors R) K},
  ¬a ≤ c → c.divMod b a = 0
-- Mathlib.RingTheory.Nilpotent.Lemmas
RingHom.ker_isRadical_iff_reduced_of_surjective : ∀ {R : Type u_1} {S : Type u_3} {F : Type u_4} [inst : CommSemiring R] [inst_1 : Semiring S] [inst_2 : FunLike F R S]
  [inst_3 : RingHomClass F R S] {f : F}, Function.Surjective ⇑f → ((RingHom.ker f).IsRadical ↔ IsReduced S)
-- Mathlib.Topology.Connected.Basic
/-- A connected space is nonempty.  -/
ConnectedSpace.toNonempty : ∀ {α : Type u} {inst : TopologicalSpace α} [self : ConnectedSpace α], Nonempty α
-- Init.Data.SInt.Lemmas
Int64.ofNat_int32ToNatClampNeg : ∀ (x : Int32), 0 ≤ x → Int64.ofNat x.toNatClampNeg = x.toInt64
-- Batteries.Lean.Meta.SavedState
/-- Run the action `x` in state `s`. Returns the result of `x` and the state after
`x` was executed. The global state remains unchanged.
 -/
Lean.Meta.SavedState.runMetaM : {α : Type} → Lean.Meta.SavedState → Lean.MetaM α → Lean.MetaM (α × Lean.Meta.SavedState)
-- Mathlib.CategoryTheory.Subfunctor.Finite
/-- The condition that a presheaf of types `F : Cᵒᵖ ⥤ Type w` is generated by
a family of sections.  -/
CategoryTheory.PresheafIsGeneratedBy : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    (F : CategoryTheory.Functor Cᵒᵖ (Type w)) → {ι : Type w'} → {X : ι → Cᵒᵖ} → ((i : ι) → F.obj (X i)) → Prop
-- Mathlib.Data.Int.ModEq
Int.modEq_and_modEq_iff_modEq_lcm : ∀ {a b m n : ℤ}, a ≡ b [ZMOD m] ∧ a ≡ b [ZMOD n] ↔ a ≡ b [ZMOD ↑(m.lcm n)]
-- Mathlib.Topology.Constructions.SumProd
/-- If `Sum.elim f g` is an embedding, then so is `g`.  -/
Topology.IsEmbedding.sumElim_right : ∀ {X : Type u} {Y : Type v} {Z : Type u_2} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y]
  [inst_2 : TopologicalSpace Z] {f : X → Z} {g : Y → Z}, Topology.IsEmbedding (Sum.elim f g) → Topology.IsEmbedding g
-- Mathlib.Algebra.Ring.Subring.Basic
Subring.comap_map_eq : ∀ {R : Type u} {S : Type v} [inst : NonAssocRing R] [inst_1 : NonAssocRing S] (f : R →+* S) (s : Subring R),
  Subring.comap f (Subring.map f s) = s ⊔ Subring.closure (⇑f ⁻¹' {0})
-- Mathlib.CategoryTheory.Limits.Indization.ParallelPair
/-- The cocone on `F₁` with apex `A` is a colimit cocone.  -/
CategoryTheory.IndParallelPairPresentation.isColimit₁ : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    {A B : CategoryTheory.Functor Cᵒᵖ (Type v₁)} →
      {f g : A ⟶ B} →
        (self : CategoryTheory.IndParallelPairPresentation f g) →
          CategoryTheory.Limits.IsColimit { pt := A, ι := self.ι₁ }
-- Mathlib.ModelTheory.Syntax
FirstOrder.Language.BoundedFormula.imp.sizeOf_spec : ∀ {L : FirstOrder.Language} {α : Type u'} [inst : SizeOf α] {n : ℕ} (f₁ f₂ : L.BoundedFormula α n),
  sizeOf (f₁.imp f₂) = 1 + sizeOf n + sizeOf f₁ + sizeOf f₂
-- Mathlib.Algebra.Order.Ring.StandardPart
ArchimedeanClass.mk_sub_stdPart_pos : ∀ {K : Type u_1} [inst : LinearOrder K] [inst_1 : Field K] [inst_2 : IsOrderedRing K] {x : K} (f : ℝ →+*o K),
  0 ≤ ArchimedeanClass.mk x → 0 < ArchimedeanClass.mk (x - f (ArchimedeanClass.stdPart x))
-- Mathlib.Algebra.Group.TypeTags.Basic
Multiplicative.ext_iff : ∀ {α : Type u} {a b : Multiplicative α}, a = b ↔ Multiplicative.toAdd a = Multiplicative.toAdd b
-- Mathlib.RingTheory.Regular.RegularSequence
RingTheory.Sequence.IsWeaklyRegular.regular_mod_prev : ∀ {R : Type u_1} {M : Type u_3} [inst : CommRing R] [inst_1 : AddCommGroup M] [inst_2 : Module R M] {rs : List R},
  RingTheory.Sequence.IsWeaklyRegular M rs →
    ∀ (i : ℕ) (h : i < rs.length), IsSMulRegular (M ⧸ Ideal.ofList (List.take i rs) • ⊤) rs[i]
-- Mathlib.Algebra.Lie.TransferInstance
/-- An equivalence `e : M ≃ₗ[R] L` gives a Lie algebra equivalence `M ≃ₗ⁅R⁆ L` where the Lie bracket
on `M` is the one obtained by transporting a Lie Bracket on `L` back along `e`.  -/
LinearEquiv.lieEquiv : (R : Type u_1) →
  {M : Type u_2} →
    {L : Type u_3} →
      [inst : CommRing R] →
        [inst_1 : AddCommGroup M] →
          [inst_2 : Module R M] → [inst_3 : LieRing L] → [inst_4 : LieAlgebra R L] → (e : M ≃ₗ[R] L) → M ≃ₗ⁅R⁆ L
-- Mathlib.Algebra.Homology.HomotopyCategory.KInjective
CochainComplex.IsKInjective.eq_δ_of_cocycle : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Abelian C]
  {K L : CochainComplex C ℤ} {n : ℤ} (z : CochainComplex.HomComplex.Cocycle K L n) [L.IsKInjective],
  HomologicalComplex.Acyclic K → ∀ (m : ℤ), m + 1 = n → ∃ α, CochainComplex.HomComplex.δ m n α = ↑z
-- Batteries.Recycling.RBTree.Lemmas
/-- A cut is like a homomorphism of orderings: it is a monotonic predicate with respect to `cmp`,
but it can make things that are distinguished by `cmp` equal.
This is sufficient for `find?` to locate an element on which `cut` returns `.eq`,
but there may be other elements, not returned by `find?`, on which `cut` also returns `.eq`.
 -/
RBTree.RBNode.IsCut : {α : Type u_1} → (α → α → Ordering) → (α → Ordering) → Prop
-- Mathlib.Algebra.Homology.TotalComplexShift
/-- Auxiliary definition for `totalShift₁Iso`.  -/
HomologicalComplex₂.totalShift₁XIso : {C : Type u_1} →
  [inst : CategoryTheory.Category.{v_1, u_1} C] →
    [inst_1 : CategoryTheory.Preadditive C] →
      (K : HomologicalComplex₂ C (ComplexShape.up ℤ) (ComplexShape.up ℤ)) →
        (x : ℤ) →
          [inst_2 : K.HasTotal (ComplexShape.up ℤ)] →
            (n n' : ℤ) →
              n + x = n' →
                ((((HomologicalComplex₂.shiftFunctor₁ C x).obj K).total (ComplexShape.up ℤ)).X n ≅
                  (K.total (ComplexShape.up ℤ)).X n')
-- Mathlib.CategoryTheory.Sites.CoverLifting
CategoryTheory.RanIsSheafOfIsCocontinuous.fac : ∀ {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} {A : Type w}
  [inst_2 : CategoryTheory.Category.{w', w} A] {J : CategoryTheory.GrothendieckTopology C}
  {K : CategoryTheory.GrothendieckTopology D} [inst_3 : G.IsCocontinuous J K] {F : CategoryTheory.Functor Cᵒᵖ A}
  (hF : CategoryTheory.Presheaf.IsSheaf J F) {R : CategoryTheory.Functor Dᵒᵖ A} {α : G.op.comp R ⟶ F}
  (hR : (CategoryTheory.Functor.RightExtension.mk R α).IsPointwiseRightKanExtension) {X : D} {S : K.Cover X}
  (s : CategoryTheory.Limits.Multifork (S.index R)) (i : S.Arrow),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.RanIsSheafOfIsCocontinuous.lift hF hR s) (R.map i.f.op) = s.ι i
-- Mathlib.MeasureTheory.Function.ConditionalExpectation.CondJensen
ConcaveOn.condExp_map_le_of_finiteDimensional : ∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] [CompleteSpace E] {α : Type u_2} {f : α → E}
  {φ : E → ℝ} {m mα : MeasurableSpace α} {μ : MeasureTheory.Measure α} [FiniteDimensional ℝ E] (hm : m ≤ mα)
  [MeasureTheory.SigmaFinite (μ.trim hm)],
  ConcaveOn ℝ Set.univ φ →
    MeasureTheory.Integrable f μ → MeasureTheory.Integrable (φ ∘ f) μ → μ[φ ∘ f | m] ≤ᵐ[μ] φ ∘ μ[f | m]
-- Mathlib.Algebra.Order.Ring.IsNonarchimedean
IsNonarchimedean.multiset_powerset_image_add : ∀ {R : Type u_1} [inst : Semiring R] [inst_1 : LinearOrder R] [IsStrictOrderedRing R] {F : Type u_2} {α : Type u_3}
  [inst_3 : CommRing α] [inst_4 : FunLike F α R] [AddGroupSeminormClass F α R] {f : F},
  IsNonarchimedean ⇑f →
    ∀ (s : Multiset α) (m : ℕ),
      ∃ t,
        t.card = s.card - m ∧
          (∀ x ∈ t, x ∈ s) ∧ f (Multiset.map Multiset.prod (Multiset.powersetCard (s.card - m) s)).sum ≤ f t.prod
-- Mathlib.SetTheory.Ordinal.Family
Ordinal.iSup'_eq_bsup : ∀ {o : Ordinal.{u_3}} {ι : Type u_3} (r : ι → ι → Prop) [inst : IsWellOrder ι r] (ho : Ordinal.type r = o)
  (f : (a : Ordinal.{u_3}) → a < o → Ordinal.{max u_3 u_4}), iSup (Ordinal.familyOfBFamily' r ho f) = o.bsup f
-- Mathlib.CategoryTheory.Adjunction.Mates
/-- A component of a transposed version of the inverse mates correspondence.  -/
CategoryTheory.mateEquiv_counit_symm : ∀ {C : Type u₁} {D : Type u₂} {E : Type u₃} {F : Type u₄} [inst : CategoryTheory.Category.{v₁, u₁} C]
  [inst_1 : CategoryTheory.Category.{v₂, u₂} D] [inst_2 : CategoryTheory.Category.{v₃, u₃} E]
  [inst_3 : CategoryTheory.Category.{v₄, u₄} F] {G : CategoryTheory.Functor C E} {H : CategoryTheory.Functor D F}
  {L₁ : CategoryTheory.Functor C D} {R₁ : CategoryTheory.Functor D C} {L₂ : CategoryTheory.Functor E F}
  {R₂ : CategoryTheory.Functor F E} (adj₁ : L₁ ⊣ R₁) (adj₂ : L₂ ⊣ R₂) (α : CategoryTheory.TwoSquare R₁ H G R₂) (d : D),
  CategoryTheory.CategoryStruct.comp (L₂.map (α.app d)) (adj₂.counit.app (H.obj d)) =
    CategoryTheory.CategoryStruct.comp (((CategoryTheory.mateEquiv adj₁ adj₂).symm α).app (R₁.obj d))
      (H.map (adj₁.counit.app d))
-- Mathlib.Order.Category.LinOrd
linOrd_dual_comp_forget_to_Lat : LinOrd.dual.comp (CategoryTheory.forget₂ LinOrd Lat) = (CategoryTheory.forget₂ LinOrd Lat).comp Lat.dual