mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.RepresentationTheory.Homological.GroupHomology.LowDegree
groupHomology.isoCycles₁_hom_comp_i_apply : ∀ {k G : Type u} [inst : CommRing k] [inst_1 : Group G] (A : Rep.{u, u, u} k G) (x : ↑(groupHomology.cycles A 1)),
  (ModuleCat.Hom.hom (groupHomology.shortComplexH1 A).g).ker.subtype
      ((CategoryTheory.ConcreteCategory.hom (groupHomology.isoCycles₁ A).hom) x) =
    (CategoryTheory.ConcreteCategory.hom (groupHomology.chainsIso₁ A).hom)
      ((CategoryTheory.ConcreteCategory.hom (groupHomology.iCycles A 1)) x)
-- Std.Data.DTreeMap.Raw.Lemmas
Std.DTreeMap.Raw.getKey_insertIfNew : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t : Std.DTreeMap.Raw α β cmp} [inst : Std.TransCmp cmp]
  (h : t.WF) {k a : α} {v : β k} {h₁ : a ∈ t.insertIfNew k v},
  (t.insertIfNew k v).getKey a h₁ = if h₂ : cmp k a = Ordering.eq ∧ k ∉ t then k else t.getKey a ⋯
-- Mathlib.SetTheory.Ordinal.Veblen
Ordinal.invVeblen₁_le : ∀ (x : Ordinal.{u_1}), x.invVeblen₁ ≤ x
-- Std.Data.ExtTreeMap.Basic
Std.ExtTreeMap.instSingletonProdOfTransCmp : {α : Type u} → {β : Type v} → {cmp : α → α → Ordering} → [Std.TransCmp cmp] → Singleton (α × β) (Std.ExtTreeMap α β cmp)
-- Mathlib.AlgebraicGeometry.EllipticCurve.Affine.Point
WeierstrassCurve.Affine.CoordinateRing.XYIdeal_eq₁ : ∀ {R : Type r} [inst : CommRing R] {W' : WeierstrassCurve.Affine R} (x y ℓ : R),
  WeierstrassCurve.Affine.CoordinateRing.XYIdeal W' x (Polynomial.C y) =
    WeierstrassCurve.Affine.CoordinateRing.XYIdeal W' x (WeierstrassCurve.Affine.linePolynomial x y ℓ)
-- Mathlib.Computability.AkraBazzi.SumTransform
AkraBazziRecurrence.asympBound_def' : ∀ {g : ℝ → ℝ} {α : Type u_2} [inst : Fintype α] (a b : α → ℝ) {n : ℕ},
  AkraBazziRecurrence.asympBound g a b n =
    ↑n ^ AkraBazziRecurrence.p a b * (1 + ∑ u ∈ Finset.range n, g ↑u / ↑u ^ (AkraBazziRecurrence.p a b + 1))
-- Mathlib.CategoryTheory.LocallyCartesianClosed.Sections
/-- The adjunction between the toOver functor and the sections functor.  -/
CategoryTheory.Over.toOverSectionsAdj : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    [inst_1 : CategoryTheory.CartesianMonoidalCategory C] →
      (I : C) →
        [inst_2 : CategoryTheory.Closed I] →
          [inst_3 : CategoryTheory.ChosenPullbacksAlong (CategoryTheory.curryRightUnitorHom I)] →
            [CategoryTheory.BraidedCategory C] → CategoryTheory.toOver I ⊣ CategoryTheory.Over.sections I
-- Mathlib.Topology.Algebra.Group.Basic
Homeomorph.mulLeft_symm : ∀ {G : Type w} [inst : TopologicalSpace G] [inst_1 : Group G] [inst_2 : SeparatelyContinuousMul G] (a : G),
  (Homeomorph.mulLeft a).symm = Homeomorph.mulLeft a⁻¹
-- Mathlib.Topology.Algebra.Module.Alternating.Basic
ContinuousAlternatingMap.constOfIsEmpty_toContinuousMultilinearMap : ∀ (R : Type u_1) (M : Type u_2) {N : Type u_4} (ι : Type u_6) [inst : Semiring R] [inst_1 : AddCommMonoid M]
  [inst_2 : Module R M] [inst_3 : TopologicalSpace M] [inst_4 : AddCommMonoid N] [inst_5 : Module R N]
  [inst_6 : TopologicalSpace N] [inst_7 : IsEmpty ι] (m : N),
  (ContinuousAlternatingMap.constOfIsEmpty R M ι m).toContinuousMultilinearMap =
    ContinuousMultilinearMap.constOfIsEmpty R (fun x => M) m
-- Lean.Data.Lsp.Workspace
Lean.Lsp.instFromJsonFileEvent.fromJson : Lean.Json → Except String Lean.Lsp.FileEvent
-- Mathlib.Order.Bounds.OrderIso
OrderIso.isLUB_image : ∀ {α : Type u_1} {β : Type u_2} [inst : Preorder α] [inst_1 : Preorder β] (f : α ≃o β) {s : Set α} {x : β},
  IsLUB (⇑f '' s) x ↔ IsLUB s (f.symm x)
-- Mathlib.FieldTheory.IsRealClosed.Basic
IsRealClosed.exists_eq_zpow_of_nonneg : ∀ {R : Type u} [inst : Field R] [IsRealClosed R] [inst_2 : LinearOrder R] [IsStrictOrderedRing R] {x : R},
  0 ≤ x → ∀ {k : ℤ}, k ≠ 0 → ∃ r, x = r ^ k
-- Mathlib.Data.List.MinMax
List.maximum_of_length_pos.eq_1 : ∀ {α : Type u_1} [inst : LinearOrder α] {l : List α} (h : 0 < l.length),
  List.maximum_of_length_pos h = l.maximum.unbot ⋯
-- Init.Data.UInt.Lemmas
UInt32.ofNatLT_uSizeToNat : ∀ (n : USize) (h : n.toNat < UInt32.size), UInt32.ofNatLT n.toNat h = n.toUInt32
-- Mathlib.Data.Matrix.Block
Matrix.blockDiagonal_one : ∀ {m : Type u_2} {o : Type u_4} {α : Type u_12} [inst : DecidableEq o] [inst_1 : Zero α] [inst_2 : DecidableEq m]
  [inst_3 : One α], Matrix.blockDiagonal 1 = 1
-- Lean.Data.Iterators.Producers.PersistentHashMap
_private.Lean.Data.Iterators.Producers.PersistentHashMap.0.Lean.PersistentHashMap.Entry.measure.eq_3 : ∀ {α : Type u_1} {β : Type u_2} (node : Lean.PersistentHashMap.Node α β),
  (Lean.PersistentHashMap.Entry.ref node).measure = 2 + node.measure
-- Lean.Expr
Lean.instInhabitedMVarId.default : Lean.MVarId
-- Mathlib.Algebra.Vertex.VertexOperator
/-- The coefficient of a vertex operator under normalized indexing.  -/
VertexOperator.ncoeff : {R : Type u_1} →
  {V : Type u_2} →
    [inst : CommRing R] →
      [inst_1 : AddCommGroup V] → [inst_2 : Module R V] → VertexOperator R V →ₗ[R] ℤ → Module.End R V
-- Mathlib.CategoryTheory.Bicategory.Opposites
Bicategory.Opposite.op2_leftUnitor_inv : ∀ {B : Type u} [inst : CategoryTheory.Bicategory B] {a b : B} (f : a ⟶ b),
  Bicategory.Opposite.op2 (CategoryTheory.Bicategory.leftUnitor f).inv =
    (CategoryTheory.Bicategory.rightUnitor f.op).inv
-- Mathlib.NumberTheory.Pell
/-- If `(x, y)` is a solution with `x` positive, then all its powers with natural exponents
have positive `x`.  -/
Pell.Solution₁.x_pow_pos : ∀ {d : ℤ} {a : Pell.Solution₁ d}, 0 < a.x → ∀ (n : ℕ), 0 < (a ^ n).x
-- Init.Data.Iterators.Consumers.Monadic.Access
Std.IterM.not_isPlausibleNthOutputStep_yield : ∀ {α β : Type w} {m : Type w → Type w'} [inst : Std.Iterator α m β] {n : ℕ} {it it' : Std.IterM m β},
  ¬Std.IterM.IsPlausibleNthOutputStep n it (Std.IterStep.skip it')
-- Init.Data.Array.Monadic
Array.flatMapM_congr : ∀ {m : Type u_1 → Type u_2} {α : Type u_3} {β : Type u_1} [inst : Monad m] {as bs : Array α},
  as = bs → ∀ {f g : α → m (Array β)}, (∀ (a : α), f a = g a) → Array.flatMapM f as = Array.flatMapM g bs
-- Init.Data.String.Lemmas.Pattern.Char
String.Slice.Pattern.Model.Char.isMatch_iff_isMatch_beq : ∀ {c : Char} {s : String.Slice} {pos : s.Pos},
  String.Slice.Pattern.Model.IsMatch c pos ↔ String.Slice.Pattern.Model.IsMatch (fun x => x == c) pos
-- Lean.Data.PersistentArray
Lean.PersistentArray.all : {α : Type u} → Lean.PersistentArray α → (α → Bool) → Bool
-- Lean.Meta.Tactic.Grind.Cases
Lean.Meta.Grind.validateCasesAttr : Lean.Name → Bool → Lean.CoreM Unit
-- Batteries.Lean.Meta.Expr
Lean.Literal.instOrd_batteries : Ord Lean.Literal
-- Mathlib.Order.SupIndep
Finset.supIndep_univ_fin_two : ∀ {α : Type u_1} [inst : Lattice α] [inst_1 : OrderBot α] (f : Fin 2 → α), Finset.univ.SupIndep f ↔ Disjoint (f 0) (f 1)
-- Mathlib.Order.Category.HeytAlg
HeytAlg.hasForgetToLat_forget₂_map : ∀ {X Y : HeytAlg} (f : X ⟶ Y),
  CategoryTheory.HasForget₂.forget₂.map f =
    BddDistLat.ofHom
      (have __src := { toFun := ⇑(HeytAlg.Hom.hom f), map_sup' := ⋯, map_inf' := ⋯ };
      { toFun := ⇑(HeytAlg.Hom.hom f), map_sup' := ⋯, map_inf' := ⋯, map_top' := ⋯, map_bot' := ⋯ })
-- Mathlib.Topology.Category.TopCat.Basic
TopCat.homeoOfIso_apply : ∀ {X Y : TopCat} (f : X ≅ Y) (a : ↑X), (TopCat.homeoOfIso f) a = (CategoryTheory.ConcreteCategory.hom f.hom) a
-- Mathlib.Order.WellFoundedSet
Set.IsPWO.image_of_monotone : ∀ {α : Type u_2} {β : Type u_3} [inst : Preorder α] [inst_1 : Preorder β] {s : Set α},
  s.IsPWO → ∀ {f : α → β}, Monotone f → (f '' s).IsPWO
-- Std.Data.TreeMap.Raw.Lemmas
Std.TreeMap.Raw.maxKeyD_le_maxKeyD_insert : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Std.TreeMap.Raw α β cmp} [Std.TransCmp cmp],
  t.WF →
    t.isEmpty = false →
      ∀ {k : α} {v : β} {fallback : α}, (cmp (t.maxKeyD fallback) ((t.insert k v).maxKeyD fallback)).isLE = true
-- Mathlib.Algebra.Group.Embedding
mulLeftEmbedding_eq_mulRightEmbedding : ∀ {G : Type u_1} [inst : CommMagma G] [inst_1 : IsCancelMul G] (g : G), mulLeftEmbedding g = mulRightEmbedding g
-- Init.Data.Array.Lemmas
_private.Init.Data.Array.Lemmas.0.Array.filterMap_push.match_1.splitter : {β : Type u_1} →
  (motive : Option β → Sort u_2) → (x : Option β) → (Unit → motive none) → ((b : β) → motive (some b)) → motive x
-- Mathlib.Topology.NhdsWithin
nhdsWithin_empty : ∀ {α : Type u_1} [inst : TopologicalSpace α] (a : α), nhdsWithin a ∅ = ⊥
-- Mathlib.MeasureTheory.Function.AEEqFun
MeasureTheory.AEEqFun.instIsCentralScalar : ∀ {α : Type u_1} {γ : Type u_3} [inst : MeasurableSpace α] {μ : MeasureTheory.Measure α} [inst_1 : TopologicalSpace γ]
  {𝕜 : Type u_5} [inst_2 : SMul 𝕜 γ] [inst_3 : ContinuousConstSMul 𝕜 γ] [inst_4 : SMul 𝕜ᵐᵒᵖ γ]
  [inst_5 : IsCentralScalar 𝕜 γ], IsCentralScalar 𝕜 (α →ₘ[μ] γ)
-- Mathlib.Topology.Order
TopologicalSpace.indiscrete_or_nontrivial : ∀ (α : Type u_2) [inst : TopologicalSpace α], IndiscreteTopology α ∨ NontrivialTopology α
-- Mathlib.CategoryTheory.CommSq
CategoryTheory.CommSq.vert_inv : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] {W X Y Z : C} {f : W ⟶ X} {i : Y ⟶ Z} {g : W ≅ Y}
  {h : X ≅ Z}, CategoryTheory.CommSq f g.hom h.hom i → CategoryTheory.CommSq i g.inv h.inv f
-- Std.Data.DHashMap.Internal.Model
/-- Internal implementation detail of the hash map  -/
Std.DHashMap.Internal.Raw₀.getEntry!ₘ : {α : Type u} →
  {β : α → Type v} →
    [BEq α] → [Hashable α] → [Inhabited ((a : α) × β a)] → Std.DHashMap.Internal.Raw₀ α β → α → (a : α) × β a
-- Mathlib.MeasureTheory.Measure.Typeclasses.Finite
MeasureTheory.isFiniteMeasureSMulOfNNRealTower : ∀ {α : Type u_1} {m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} {R : Type u_5} [inst : SMul R NNReal]
  [inst_1 : SMul R ENNReal] [IsScalarTower R NNReal ENNReal] [inst : IsScalarTower R ENNReal ENNReal]
  [MeasureTheory.IsFiniteMeasure μ] {r : R}, MeasureTheory.IsFiniteMeasure (r • μ)
-- Mathlib.Analysis.Convex.MetricSpace
/-- `dist(∑ tᵢ xᵢ, ∑ tᵢ yᵢ) ≤ ∑ tᵢ dist(xᵢ, yᵢ)`  -/
Convexity.dist_iConvexComb_le : ∀ {X : Type u_2} [inst : Convexity.ConvexSpace ℝ X] [inst_1 : MetricSpace X] [Convexity.IsConvexDist X] {ι : Type u_3}
  (f : Convexity.StdSimplex ℝ ι) (x y : ι → X),
  dist (Convexity.iConvexComb f x) (Convexity.iConvexComb f y) ≤ Convexity.iConvexComb f fun i => dist (x i) (y i)
-- Mathlib.CategoryTheory.Limits.Preserves.Over
CategoryTheory.Limits.instPreservesFilteredColimitsOfSizeUnderForget : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] {X : C},
  CategoryTheory.Limits.PreservesFilteredColimitsOfSize.{u_2, u_3, v_1, v_1, max u_1 v_1, u_1}
    (CategoryTheory.Under.forget X)
-- Mathlib.Topology.Algebra.Module.Spaces.UniformConvergenceCLM
UniformConvergenceCLM.instUniformSpace.congr_simp : ∀ {𝕜₁ : 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 : Module 𝕜₁ E] [inst_4 : TopologicalSpace E]
  [inst_5 : AddCommGroup F] [inst_6 : Module 𝕜₂ F] [inst_7 : UniformSpace F] [inst_8 : IsUniformAddGroup F]
  (𝔖 : Set (Set E)), UniformConvergenceCLM.instUniformSpace σ F 𝔖 = UniformConvergenceCLM.instUniformSpace σ F 𝔖
-- Mathlib.CategoryTheory.Comma.Arrow
CategoryTheory.Functor.mapArrowEquivalence_unitIso : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  (e : C ≌ D),
  (CategoryTheory.Functor.mapArrowEquivalence e).unitIso = (CategoryTheory.Functor.mapArrowFunctor C C).mapIso e.unitIso
-- Std.Data.TreeMap.Lemmas
Std.TreeMap.Equiv.insertMany_list : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t₁ t₂ : Std.TreeMap α β cmp} [Std.TransCmp cmp],
  t₁.Equiv t₂ → ∀ (l : List (α × β)), (t₁.insertMany l).Equiv (t₂.insertMany l)
-- Mathlib.Topology.VectorBundle.Basic
Bundle.zeroSection_proj : ∀ {B : Type u_2} (F : Type u_3) (E : B → Type u_4) [inst : (x : B) → Zero (E x)] (x : B),
  (Bundle.zeroSection F E x).proj = x
-- Mathlib.GroupTheory.OrderOfElement
isAddTorsionFree_iff_not_isOfFinAddOrder : ∀ {G : Type u_1} [inst : AddCommGroup G], IsAddTorsionFree G ↔ ∀ ⦃a : G⦄, a ≠ 0 → ¬IsOfFinAddOrder a
-- Mathlib.Algebra.Order.Hom.TypeTags
Multiplicative.instUniqueOrderdMonoidIso : {G : Type u_1} →
  {H : Type u_2} →
    [inst : AddCommMonoid G] →
      [inst_1 : PartialOrder G] →
        [inst_2 : AddCommMonoid H] →
          [inst_3 : PartialOrder H] → [Unique (G ≃+o H)] → Unique (Multiplicative G ≃*o Multiplicative H)
-- Lean.Parser.Types
Lean.Parser.ParserState.mkUnexpectedError : Lean.Parser.ParserState → String → optParam (List String) [] → optParam Bool true → Lean.Parser.ParserState
-- Mathlib.Algebra.GroupWithZero.Prod
Prod.instCommMonoidWithZero : {M₀ : Type u_1} → {N₀ : Type u_2} → [CommMonoidWithZero M₀] → [CommMonoidWithZero N₀] → CommMonoidWithZero (M₀ × N₀)
-- Mathlib.RingTheory.IsAdjoinRoot
/-- If `α` is primitive in `E/f`, then `E` is given by adjoining a root of `minpoly F α`.  -/
IsAdjoinRoot.mkOfPrimitiveElement : {F : Type u_1} →
  {E : Type u_2} →
    [inst : Field F] →
      [inst_1 : Field E] → [inst_2 : Algebra F E] → {α : E} → IsIntegral F α → F⟮α⟯ = ⊤ → IsAdjoinRoot E (minpoly F α)
-- Std.Tactic.BVDecide.Normalize.Bool
Std.Tactic.BVDecide.Normalize.BitVec.ite_else_not_ite'' : ∀ {w : ℕ} (c0 c1 : Bool) {a b : BitVec w},
  (bif c0 then a else ~~~bif c1 then b else ~~~a) = bif !c0 && c1 then ~~~b else a
-- Mathlib.LinearAlgebra.BilinearForm.Isometry
LinearMap.BilinForm.Isometry.comp_apply : ∀ {R : Type u_1} {M₁ : Type u_3} {M₂ : Type u_4} {M₃ : Type u_5} [inst : CommSemiring R] [inst_1 : AddCommMonoid M₁]
  [inst_2 : AddCommMonoid M₂] [inst_3 : AddCommMonoid M₃] [inst_4 : Module R M₁] [inst_5 : Module R M₂]
  [inst_6 : Module R M₃] {B₁ : LinearMap.BilinForm R M₁} {B₂ : LinearMap.BilinForm R M₂} {B₃ : LinearMap.BilinForm R M₃}
  (g : B₂ →bᵢ B₃) (f : B₁ →bᵢ B₂) (x : M₁), (g.comp f) x = g (f x)
-- Mathlib.Analysis.Calculus.FDeriv.Congr
HasFDerivAtFilter.congr_of_eventuallyEq : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : AddCommGroup E] [inst_2 : Module 𝕜 E]
  [inst_3 : TopologicalSpace E] {F : Type u_3} [inst_4 : AddCommGroup F] [inst_5 : Module 𝕜 F]
  [inst_6 : TopologicalSpace F] {f f₁ : E → F} {f' : E →L[𝕜] F} {L : Filter (E × E)},
  HasFDerivAtFilter f f' L → Prod.map f₁ f₁ =ᶠ[L] Prod.map f f → HasFDerivAtFilter f₁ f' L
-- Mathlib.Topology.Algebra.Group.Basic
discreteTopology_of_isOpen_singleton_one : ∀ {G : Type w} [inst : TopologicalSpace G] [inst_1 : Group G] [SeparatelyContinuousMul G],
  IsOpen {1} → DiscreteTopology G
-- Mathlib.Algebra.Group.Pointwise.Set.Lattice
Set.add_iUnion : ∀ {α : Type u_2} {ι : Sort u_5} [inst : Add α] (s : Set α) (t : ι → Set α), s + ⋃ i, t i = ⋃ i, s + t i
-- Mathlib.Data.Subtype
exists_eq_subtype_mk_iff : ∀ {α : Sort u_1} {p : α → Prop} {a : Subtype p} {b : α}, (∃ (h : p b), a = ⟨b, h⟩) ↔ ↑a = b
-- Mathlib.Tactic.Linter.TextBased
/-- Produce style error output aimed at humans: no error code, clickable file name  -/
Mathlib.Linter.TextBased.ErrorFormat.humanReadable : Mathlib.Linter.TextBased.ErrorFormat
-- Mathlib.ModelTheory.Substructures
FirstOrder.Language.Substructure.closure_union : ∀ {L : FirstOrder.Language} {M : Type w} [inst : L.Structure M] (s t : Set M),
  (FirstOrder.Language.Substructure.closure L).toFun (s ∪ t) =
    (FirstOrder.Language.Substructure.closure L).toFun s ⊔ (FirstOrder.Language.Substructure.closure L).toFun t
-- Mathlib.CategoryTheory.Sums.Associator
CategoryTheory.sum.inrCompAssociator.eq_1 : ∀ (C : Type u₁) [inst : CategoryTheory.Category.{v₁, u₁} C] (D : Type u₂) [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  (E : Type u₃) [inst_2 : CategoryTheory.Category.{v₃, u₃} E],
  CategoryTheory.sum.inrCompAssociator C D E =
    ((CategoryTheory.Sum.inl_ C (D ⊕ E)).sum'
          ((CategoryTheory.Sum.inl_ D E).comp (CategoryTheory.Sum.inr_ C (D ⊕ E)))).inrCompSum'
      ((CategoryTheory.Sum.inr_ D E).comp (CategoryTheory.Sum.inr_ C (D ⊕ E)))
-- Mathlib.CategoryTheory.MorphismProperty.Basic
/-- If `W j` are morphism properties on categories `C j` for all `j`, this is the
induced morphism property on the category `∀ j, C j`.  -/
CategoryTheory.MorphismProperty.pi : {J : Type w} →
  {C : J → Type u} →
    [inst : (j : J) → CategoryTheory.Category.{v, u} (C j)] →
      ((j : J) → CategoryTheory.MorphismProperty (C j)) → CategoryTheory.MorphismProperty ((j : J) → C j)
-- Mathlib.Topology.FiberBundle.Trivialization
Bundle.Pretrivialization.symm_proj_apply : ∀ {B : Type u_1} {F : Type u_2} {E : B → Type u_3} [inst : TopologicalSpace B] [inst_1 : TopologicalSpace F]
  [inst_2 : ∀ (x : B), Nonempty (E x)] (e : Bundle.Pretrivialization F Bundle.TotalSpace.proj)
  (z : Bundle.TotalSpace F E), z.proj ∈ e.baseSet → e.symm z.proj (↑e z).2 = z.snd
-- Mathlib.AlgebraicGeometry.Morphisms.FinitePresentation
AlgebraicGeometry.locallyOfFinitePresentation_isStableUnderBaseChange : CategoryTheory.MorphismProperty.IsStableUnderBaseChange @AlgebraicGeometry.LocallyOfFinitePresentation
-- Init.Internal.Order.Lemmas
Lean.Order.List.monotone_filterRevM : ∀ {γ : 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.filterRevM (f x) xs
-- Mathlib.Analysis.BoxIntegral.Box.Basic
BoxIntegral.Box.lower_mem_Icc : ∀ {ι : Type u_1} (I : BoxIntegral.Box ι), I.lower ∈ BoxIntegral.Box.Icc I
-- Std.Data.DTreeMap.Lemmas
Std.DTreeMap.getKey?_diff : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t₁ t₂ : Std.DTreeMap α β cmp} [Std.TransCmp cmp] {k : α},
  (t₁ \ t₂).getKey? k = if k ∈ t₂ then none else t₁.getKey? k
-- Mathlib.Algebra.Module.Submodule.Lattice
Submodule.instNontrivial : ∀ {R : Type u_1} {M : Type u_3} [inst : Semiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M] [Nontrivial M],
  Nontrivial (Submodule R M)
-- Mathlib.GroupTheory.MonoidLocalization.Maps
Submonoid.LocalizationMap.map_eq : ∀ {M : Type u_1} [inst : CommMonoid M] {S : Submonoid M} {N : Type u_2} [inst_1 : CommMonoid N] {P : Type u_3}
  [inst_2 : CommMonoid P] (f : S.LocalizationMap N) {g : M →* P} {T : Submonoid P} (hy : ∀ (y : ↥S), g ↑y ∈ T)
  {Q : Type u_4} [inst_3 : CommMonoid Q] {k : T.LocalizationMap Q} (x : M), (f.map hy k) (f x) = k (g x)
-- Mathlib.SetTheory.ZFC.Basic
ZFSet.inter_eq_left_of_subset : ∀ {x y : ZFSet.{u}}, x ⊆ y → x ∩ y = x
-- Mathlib.Algebra.Polynomial.Derivative
Polynomial.iterate_derivative_derivative_mul_X : ∀ {R : Type u} [inst : CommSemiring R] {n : ℕ} (p : Polynomial R),
  (⇑Polynomial.derivative)^[n] (Polynomial.derivative p * Polynomial.X) =
    (⇑Polynomial.derivative)^[n + 1] p * Polynomial.X + n • (⇑Polynomial.derivative)^[n] p
-- Mathlib.Algebra.Order.Monoid.Unbundled.Basic
Contravariant.AddLECancellable : ∀ {α : Type u_1} [inst : Add α] [inst_1 : LE α] [AddLeftReflectLE α] {a : α}, AddLECancellable a
-- Mathlib.Data.Finset.Range
Finset.range_add_one : ∀ {n : ℕ}, Finset.range (n + 1) = insert n (Finset.range n)
-- Mathlib.Algebra.Group.Subgroup.Map
AddSubgroup.mem_comap : ∀ {G : Type u_1} [inst : AddGroup G] {N : Type u_5} [inst_1 : AddGroup N] {K : AddSubgroup N} {f : G →+ N} {x : G},
  x ∈ AddSubgroup.comap f K ↔ f x ∈ K
-- Mathlib.CategoryTheory.Limits.Shapes.Biproducts
CategoryTheory.Limits.instHasCokernelι : ∀ {J : Type w} {C : Type u} [inst : CategoryTheory.Category.{v, u} C]
  [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C] (f : J → C) (i : J)
  [inst_2 : CategoryTheory.Limits.HasBiproduct f]
  [CategoryTheory.Limits.HasBiproduct (Subtype.restrict (fun j => j ≠ i) f)],
  CategoryTheory.Limits.HasCokernel (CategoryTheory.Limits.biproduct.ι f i)
-- Mathlib.Order.CompleteBooleanAlgebra
_private.Mathlib.Order.CompleteBooleanAlgebra.0.Order.Coframe.MinimalAxioms.iInf_sup_eq : ∀ {α : Type u} {ι : Sort w} [inst : CompleteLattice α],
  Order.Coframe.MinimalAxioms α → ∀ (f : ι → α) (a : α), (⨅ i, f i) ⊔ a = ⨅ i, f i ⊔ a
-- Init.Data.Array.DecidableEq
Array.instDecidableEqImpl : {α : Type u_1} → [DecidableEq α] → DecidableEq (Array α)
-- Std.Data.TreeMap.Raw.Lemmas
Std.TreeMap.Raw.forIn_eq_forIn_toArray : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Std.TreeMap.Raw α β cmp} {δ : Type w} {m : Type w → Type w'}
  [inst : Monad m] [LawfulMonad m] {f : α × β → δ → m (ForInStep δ)} {init : δ}, forIn t init f = forIn t.toArray init f
-- Batteries.Data.ByteArray
ByteArray.uset_eq_set : ∀ (a : ByteArray) {i : USize} (h : i.toNat < a.size) (v : UInt8), a.uset i v h = a.set i.toNat v h
-- Init.Data.SInt.Bitwise
Int32.ofBitVec_and : ∀ (a b : BitVec 32), Int32.ofBitVec (a &&& b) = Int32.ofBitVec a &&& Int32.ofBitVec b
-- Mathlib.CategoryTheory.GuitartExact.VerticalComposition
CategoryTheory.TwoSquare.vComp'.eq_1 : ∀ {C₁ : Type u_1} {C₂ : Type u_2} {C₃ : Type u_3} {D₁ : Type u_4} {D₂ : Type u_5} {D₃ : Type u_6}
  [inst : CategoryTheory.Category.{v_1, u_1} C₁] [inst_1 : CategoryTheory.Category.{v_2, u_2} C₂]
  [inst_2 : CategoryTheory.Category.{v_3, u_3} C₃] [inst_3 : CategoryTheory.Category.{v_4, u_4} D₁]
  [inst_4 : CategoryTheory.Category.{v_5, u_5} D₂] [inst_5 : CategoryTheory.Category.{v_6, u_6} D₃]
  {H₁ : CategoryTheory.Functor C₁ D₁} {L₁ : CategoryTheory.Functor C₁ C₂} {R₁ : CategoryTheory.Functor D₁ D₂}
  {H₂ : CategoryTheory.Functor C₂ D₂} (w : CategoryTheory.TwoSquare H₁ L₁ R₁ H₂) {L₂ : CategoryTheory.Functor C₂ C₃}
  {R₂ : CategoryTheory.Functor D₂ D₃} {H₃ : CategoryTheory.Functor C₃ D₃} (w' : CategoryTheory.TwoSquare H₂ L₂ R₂ H₃)
  {L₁₂ : CategoryTheory.Functor C₁ C₃} {R₁₂ : CategoryTheory.Functor D₁ D₃} (eL : L₁.comp L₂ ≅ L₁₂)
  (eR : R₁.comp R₂ ≅ R₁₂), w.vComp' w' eL eR = (w.vComp w').whiskerVertical eL.hom eR.inv
-- Mathlib.Topology.Sion
/-- The Sion-von Neumann minimax theorem (saddle point form)  -/
Sion.exists_isSaddlePointOn' : ∀ {E : Type u_1} {F : Type u_2} {β : Type u_3} [inst : LinearOrder β] {X : Set E} {Y : Set F} {f : E → F → β}
  [inst_1 : TopologicalSpace E] [inst_2 : AddCommGroup E] [inst_3 : Module ℝ E] [IsTopologicalAddGroup E]
  [ContinuousSMul ℝ E],
  X.Nonempty →
    IsCompact X →
      (∀ y ∈ Y, LowerSemicontinuousOn (fun x => f x y) X) →
        (∀ y ∈ Y, QuasiconvexOn ℝ X fun x => f x y) →
          ∀ [inst_6 : TopologicalSpace F] [inst_7 : AddCommGroup F] [inst_8 : Module ℝ F],
            Convex ℝ Y →
              IsCompact Y →
                (∀ x ∈ X, UpperSemicontinuousOn (fun y => f x y) Y) →
                  (∀ x ∈ X, QuasiconcaveOn ℝ Y fun y => f x y) →
                    ∀ [DenselyOrdered β] [IsTopologicalAddGroup F] [ContinuousSMul ℝ F],
                      Convex ℝ X → Y.Nonempty → ∃ a ∈ X, ∃ b ∈ Y, IsSaddlePointOn X Y f a b
-- Init.Data.SInt.Lemmas
Int32.ofBitVec_neg : ∀ (a : BitVec 32), Int32.ofBitVec (-a) = -Int32.ofBitVec a
-- Std.Data.DTreeMap.Internal.Model
/-- Model implementation of the `getKeyD` function.
Internal implementation detail of the tree map
 -/
Std.DTreeMap.Internal.Impl.getKeyDₘ : {α : Type u} → {β : α → Type v} → [Ord α] → α → Std.DTreeMap.Internal.Impl α β → α → α
-- Mathlib.Algebra.Homology.HomologicalBicomplex
/-- Given a category `C` and two complex shapes `c₁` and `c₂` on types `I₁` and `I₂`,
the associated type of bicomplexes `HomologicalComplex₂ C c₁ c₂` is
`K : HomologicalComplex (HomologicalComplex C c₂) c₁`. Then, the object in
position `⟨i₁, i₂⟩` can be obtained as `(K.X i₁).X i₂`.  -/
HomologicalComplex₂ : (C : Type u_1) →
  [inst : CategoryTheory.Category.{v_1, u_1} C] →
    [CategoryTheory.Limits.HasZeroMorphisms C] →
      {I₁ : Type u_2} →
        {I₂ : Type u_3} → ComplexShape I₁ → ComplexShape I₂ → Type (max (max (max (max u_3 u_1) v_1) u_2) u_3 v_1)
-- Mathlib.Algebra.Group.Equiv.Opposite
/-- The function `MulOpposite.op` is an additive equivalence.  -/
MulOpposite.opAddEquiv : {α : Type u_2} → [inst : Add α] → α ≃+ αᵐᵒᵖ
-- Mathlib.Algebra.Group.Subgroup.Order
/-- In a group that satisfies the normalizer condition, every maximal subgroup is normal  -/
Subgroup.NormalizerCondition.normal_of_coatom : ∀ {G : Type u_1} [inst : Group G] (H : Subgroup G), NormalizerCondition G → IsCoatom H → H.Normal
-- Mathlib.AlgebraicGeometry.Birational.RationalMap
/-- The domain of definition of a rational map.  -/
AlgebraicGeometry.Scheme.RationalMap.domain : {X Y : AlgebraicGeometry.Scheme} → X.RationalMap Y → X.Opens
-- Mathlib.Order.Filter.CountableInter
Filter.CountableGenerateSets.superset : ∀ {α : Type u_2} {g : Set (Set α)} {s t : Set α},
  Filter.CountableGenerateSets g s → s ⊆ t → Filter.CountableGenerateSets g t