mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Topology.Order.IsLUB
/-- A closed interval in a conditionally complete linear order is compact.
Also see general API on `CompactIccSpace`.  -/
ConditionallyCompleteLinearOrder.isCompact_Icc : ∀ {α : Type u_3} [inst : ConditionallyCompleteLinearOrder α] [inst_1 : TopologicalSpace α] [OrderTopology α] (a b : α),
  IsCompact (Set.Icc a b)
-- Mathlib.Data.Finset.Option
Finset.forall_mem_eraseNone : ∀ {α : Type u_1} {s : Finset (Option α)} {p : Option α → Prop},
  (∀ a ∈ Finset.eraseNone s, p (some a)) ↔ ∀ (a : α), some a ∈ s → p (some a)
-- Lean.Elab.Tactic.Simp
_private.Lean.Elab.Tactic.Simp.0.Lean.Elab.Tactic.resolveSimpIdTheorem?.isSimproc? : Lean.Expr → Lean.MetaM (Option Lean.Name)
-- Std.Data.DTreeMap.Internal.WF.Lemmas
_private.Std.Data.DTreeMap.Internal.WF.Lemmas.0.Std.Internal.List.getKey?.eq_1 : ∀ {α : Type u} {β : α → Type v} [inst : BEq α] (a : α), Std.Internal.List.getKey? a [] = none
-- Mathlib.Algebra.Order.Hom.Monoid
OrderMonoidIso.coe_mulEquiv : ∀ {α : Type u_2} {β : Type u_3} [inst : Preorder α] [inst_1 : Preorder β] [inst_2 : Mul α] [inst_3 : Mul β]
  (f : α ≃*o β), ⇑↑f = ⇑f
-- Lean.Expr
_private.Lean.Expr.0.Lean.Expr.getAppArgsAux : Lean.Expr → Array Lean.Expr → ℕ → Array Lean.Expr
-- Mathlib.FieldTheory.Galois.IsGaloisGroup
IsGaloisGroup.of_mulEquiv_algEquiv : ∀ {G : Type u_1} {K : Type u_3} {L : Type u_4} [inst : Group G] [inst_1 : Field K] [inst_2 : Field L]
  [inst_3 : Algebra K L] [inst_4 : MulSemiringAction G L] [IsGalois K L] (e : G ≃* Gal(L/K)),
  (∀ (g : G) (x : L), (e g) x = g • x) → IsGaloisGroup G K L
-- Mathlib.LinearAlgebra.Matrix.PosDef
Matrix.PosSemidef.zpow : ∀ {n : Type u_2} {R' : Type u_4} [inst : CommRing R'] [inst_1 : PartialOrder R'] [inst_2 : StarRing R']
  [inst_3 : Fintype n] [StarOrderedRing R'] [inst_5 : DecidableEq n] {M : Matrix n n R'},
  M.PosSemidef → ∀ (z : ℤ), (M ^ z).PosSemidef
-- Mathlib.MeasureTheory.MeasurableSpace.Constructions
ENat.measurable_iff : ∀ {α : Type u_6} [inst : MeasurableSpace α] {f : α → ℕ∞}, Measurable f ↔ ∀ (n : ℕ), MeasurableSet (f ⁻¹' {↑n})
-- Mathlib.NumberTheory.Harmonic.ZetaAsymp
riemannZeta₀_one : riemannZeta₀ 1 = ↑Real.eulerMascheroniConstant
-- Std.Data.DTreeMap.Basic
/-- Carries out a monadic action on each mapping in the tree map in ascending order.  -/
Std.DTreeMap.Const.forMUncurried : {α : Type u} →
  {cmp : α → α → Ordering} →
    {m : Type w → Type w₂} →
      [Monad m] → {β : Type v} → (α × β → m PUnit.{w + 1}) → Std.DTreeMap α (fun x => β) cmp → m PUnit.{w + 1}
-- Mathlib.AlgebraicTopology.SimplexCategory.Truncated
SimplexCategory.Truncated.δ₂_zero_comp_σ₂_zero : ∀ {n : ℕ} (hn : autoParam ({ len := n }.len ≤ 2) SimplexCategory.Truncated.δ₂_zero_comp_σ₂_zero._auto_1)
  (hn' : autoParam ({ len := n + 1 }.len ≤ 2) SimplexCategory.Truncated.δ₂_zero_comp_σ₂_zero._auto_3),
  CategoryTheory.CategoryStruct.comp (SimplexCategory.Truncated.δ₂ 0 hn hn') (SimplexCategory.Truncated.σ₂ 0 hn' hn) =
    CategoryTheory.CategoryStruct.id { obj := { len := n }, property := hn }
-- Mathlib.RepresentationTheory.Homological.GroupCohomology.LowDegree
groupCohomology.cocycles₂.eq_1 : ∀ {k G : Type u} [inst : CommRing k] [inst_1 : Group G] (A : Rep.{u_1, u, u} k G),
  groupCohomology.cocycles₂ A = (ModuleCat.Hom.hom (groupCohomology.d₂₃ A)).ker
-- Mathlib.RingTheory.Polynomial.Chebyshev
Polynomial.Chebyshev.T_eval_neg_one : ∀ (R : Type u_1) [inst : CommRing R] (n : ℤ), Polynomial.eval (-1) (Polynomial.Chebyshev.T R n) = ↑↑n.negOnePow
-- Mathlib.CategoryTheory.Functor.KanExtension.Adjunction
/-- Composing the left Kan extension of `L : C ⥤ D` with `colim` on shapes `D` is isomorphic
to `colim` on shapes `C`.  -/
CategoryTheory.Functor.lanCompColimIso : {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] →
        (L : CategoryTheory.Functor C D) →
          {H : Type u_3} →
            [inst_2 : CategoryTheory.Category.{v_3, u_3} H] →
              [inst_3 : ∀ (F : CategoryTheory.Functor C H), L.HasLeftKanExtension F] →
                [inst_4 : CategoryTheory.Limits.HasColimitsOfShape C H] →
                  [inst_5 : CategoryTheory.Limits.HasColimitsOfShape D H] →
                    L.lan.comp CategoryTheory.Limits.colim ≅ CategoryTheory.Limits.colim
-- Mathlib.GroupTheory.GroupAction.SubMulAction.Combination
Set.powersetCard.coe_mulActionHom_compl : ∀ (G : Type u_1) [inst : Group G] (α : Type u_2) [inst_1 : MulAction G α] {n : ℕ} [inst_2 : DecidableEq α]
  [inst_3 : Fintype α] {m : ℕ} {hm : m + n = Fintype.card α} {s : ↑(Set.powersetCard α n)},
  ↑((Set.powersetCard.mulActionHom_compl G α hm) s) = (↑s)ᶜ
-- Mathlib.Data.Num.Bitwise
/-- The `tail` of a `NzsNum` is the `SNum` obtained by removing the LSB.
Edge cases: `tail 1 = 0` and `tail (-2) = -1`.  -/
NzsNum.tail : NzsNum → SNum
-- Mathlib.Algebra.Group.TransferInstance
Equiv.semigroup.eq_1 : ∀ {α : Type u_2} {β : Type u_3} (e : α ≃ β) [inst : Semigroup β], e.semigroup = Function.Injective.semigroup ⇑e ⋯ ⋯
-- Mathlib.AlgebraicGeometry.EllipticCurve.Affine.Formula
_private.Mathlib.AlgebraicGeometry.EllipticCurve.Affine.Formula.0.tacticC_simp : Lean.ParserDescr
-- Batteries.Data.UnionFind.Lemmas
Batteries.UnionFind.rank_push : ∀ {a : ℕ} {m : Batteries.UnionFind}, m.push.rank a = m.rank a
-- Mathlib.CategoryTheory.Comma.Presheaf.Basic
CategoryTheory.OverPresheafAux.OverArrows.map₁.congr_simp : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {A F G : CategoryTheory.Functor Cᵒᵖ (Type v)} {η : F ⟶ A}
  {μ : G ⟶ A} {X : C} {s : CategoryTheory.yoneda.obj X ⟶ A} (u u_1 : CategoryTheory.OverPresheafAux.OverArrows η s),
  u = u_1 →
    ∀ (ε ε_1 : F ⟶ G) (e_ε : ε = ε_1) (hε : CategoryTheory.CategoryStruct.comp ε μ = η), u.map₁ ε hε = u_1.map₁ ε_1 ⋯
-- Std.Tactic.BVDecide.Normalize.BitVec
Std.Tactic.BVDecide.Normalize.BitVec.and_const_right : ∀ {w a : ℕ} {b : BitVec w} {c : ℕ},
  BitVec.ofNat w a &&& (b &&& BitVec.ofNat w c) = BitVec.ofNat w a &&& BitVec.ofNat w c &&& b
-- Mathlib.Order.CompleteLattice.Lemmas
iSup_ge_eq_iSup_nat_add : ∀ {α : Type u_1} [inst : CompleteLattice α] (u : ℕ → α) (n : ℕ), ⨆ i, ⨆ (_ : i ≥ n), u i = ⨆ i, u (i + n)
-- Mathlib.MeasureTheory.Integral.IntervalIntegral.IntegrationByParts
intervalIntegral.integrable_comp_mul_deriv_iff_of_deriv_nonneg : ∀ {a b : ℝ} {f f' g : ℝ → ℝ},
  ContinuousOn f (Set.uIcc a b) →
    (∀ x ∈ Set.Ioo (min a b) (max a b), HasDerivAt f (f' x) x) →
      (∀ x ∈ Set.Ioo (min a b) (max a b), 0 ≤ f' x) →
        (IntervalIntegrable (fun x => (g ∘ f) x * f' x) MeasureTheory.volume a b ↔
          IntervalIntegrable g MeasureTheory.volume (f a) (f b))
-- Mathlib.Algebra.Module.Submodule.Lattice
Submodule.coe_sInf : ∀ {R : Type u_1} {M : Type u_3} [inst : Semiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M]
  (P : Set (Submodule R M)), ↑(sInf P) = ⋂ p ∈ P, ↑p
-- Mathlib.Analysis.InnerProductSpace.Dual
_private.Mathlib.Analysis.InnerProductSpace.Dual.0.InnerProductSpace.«term⟪_,_⟫_1» : Lean.ParserDescr
-- Lean.Data.Lsp.LanguageFeatures
Lean.Lsp.CallHierarchyOutgoingCall.mk : Lean.Lsp.CallHierarchyItem → Array Lean.Lsp.Range → Lean.Lsp.CallHierarchyOutgoingCall
-- Init.Core
instNonemptyTask : ∀ {α : Type u_1} [Nonempty α], Nonempty (Task α)
-- Mathlib.Topology.Category.TopCommRingCat
/-- The forgetful functors to `Type` do not reflect isomorphisms,
but the forgetful functor from `TopCommRingCat` to `TopCat` does.
 -/
TopCommRingCat.instReflectsIsomorphismsTopCatForget₂SubtypeRingHomαContinuousCoeContinuousMapCarrier : (CategoryTheory.forget₂ TopCommRingCat TopCat).ReflectsIsomorphisms
-- Mathlib.Algebra.Ring.Subsemiring.MulOpposite
Subsemiring.coe_unop : ∀ {R : Type u_2} [inst : NonAssocSemiring R] (S : Subsemiring Rᵐᵒᵖ), ↑S.unop = MulOpposite.op ⁻¹' ↑S
-- Mathlib.Combinatorics.SimpleGraph.Coloring.Vertex
SimpleGraph.IsClique.card_le_of_coloring : ∀ {V : Type u} {G : SimpleGraph V} {α : Type u_2} {s : Finset V},
  G.IsClique ↑s → ∀ [inst : Fintype α] (C : G.Coloring α), s.card ≤ Fintype.card α
-- Init.Data.Iterators.Basic
Std.IterM.IsPlausibleOutput.eq_1 : ∀ {α : Type w} {m : Type w → Type w'} {β : Type w} [inst : Std.Iterator α m β] (it : Std.IterM m β) (out : β),
  it.IsPlausibleOutput out = ∃ it', it.IsPlausibleStep (Std.IterStep.yield it' out)
-- Mathlib.FieldTheory.Normal.Closure
IntermediateField.normal_iff_forall_map_eq : ∀ {F : Type u_1} {L : Type u_3} [inst : Field F] [inst_1 : Field L] [inst_2 : Algebra F L] [Normal F L]
  {K : IntermediateField F L}, Normal F ↥K ↔ ∀ (σ : L →ₐ[F] L), IntermediateField.map σ K = K
-- Mathlib.CategoryTheory.Bicategory.Yoneda
CategoryTheory.Pseudofunctor.StrongTrans.isoMk.congr_simp : ∀ {B : Type u₁} [inst : CategoryTheory.Bicategory B] {C : Type u₂} [inst_1 : CategoryTheory.Bicategory C]
  {F G : CategoryTheory.Pseudofunctor B C} {η θ : F ⟶ G} (app app_1 : (a : B) → η.app a ≅ θ.app a) (e_app : app = app_1)
  (naturality :
    ∀ {a b : B} (f : a ⟶ b),
      CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.whiskerLeft (F.map f) (app b).hom)
          (θ.naturality f).hom =
        CategoryTheory.CategoryStruct.comp (η.naturality f).hom
          (CategoryTheory.Bicategory.whiskerRight (app a).hom (G.map f))),
  CategoryTheory.Pseudofunctor.StrongTrans.isoMk app naturality = CategoryTheory.Pseudofunctor.StrongTrans.isoMk app_1 ⋯
-- Mathlib.SetTheory.Cardinal.Arithmetic
Cardinal.mk_list_eq_mk : ∀ (α : Type u) [Infinite α], Cardinal.mk (List α) = Cardinal.mk α
-- Init.Data.Nat.Basic
Nat.ne_zero_of_lt : ∀ {b a : ℕ}, b < a → a ≠ 0
-- Init.Data.Range.Polymorphic.NatLemmas
Nat.map_add_toList_rio : ∀ {n k : ℕ}, List.map (fun x => x + k) (*...n).toList = (k...n + k).toList
-- Mathlib.Order.Interval.Finset.Nat
Nat.strong_decreasing_induction : ∀ {P : ℕ → Prop}, (∃ n, ∀ m > n, P m) → (∀ (n : ℕ), (∀ m > n, P m) → P n) → ∀ (n : ℕ), P n
-- Mathlib.Algebra.Homology.Factorizations.CM5a
_private.Mathlib.Algebra.Homology.Factorizations.CM5a.0.CochainComplex.Plus.modelCategoryQuillen.cm5a_cof.CofFibFactorizationQuasiIsoLE.exists_next : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Abelian C]
  {K L : CochainComplex C ℤ} {f : K ⟶ L} [CategoryTheory.EnoughInjectives C] {n₀ : ℤ}
  (F : CochainComplex.Plus.modelCategoryQuillen.cm5a_cof.CofFibFactorizationQuasiIsoLE✝ f n₀) (n₁ : ℤ),
  n₀ + 1 = n₁ → ∃ F' g, ∀ i ≤ n₀, CategoryTheory.IsIso (g.hom.h.f i)
-- Mathlib.MeasureTheory.Integral.Bochner.L1
MeasureTheory.L1.integralCLM.congr_simp : ∀ {α : Type u_1} {E : Type u_2} [inst : NormedAddCommGroup E] {m : MeasurableSpace α} {μ : MeasureTheory.Measure α}
  [inst_1 : NormedSpace ℝ E] [inst_2 : CompleteSpace E], MeasureTheory.L1.integralCLM = MeasureTheory.L1.integralCLM
-- Mathlib.CategoryTheory.Endofunctor.Algebra
CategoryTheory.Endofunctor.Coalgebra.forget_faithful : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {F : CategoryTheory.Functor C C},
  (CategoryTheory.Endofunctor.Coalgebra.forget F).Faithful
-- Init.Data.UInt.Lemmas
UInt8.mul_two : ∀ {a : UInt8}, a * 2 = a + a
-- Mathlib.Order.Filter.Pointwise
Filter.covariant_smul_filter : ∀ {α : Type u_2} {β : Type u_3} [inst : SMul α β],
  CovariantClass α (Filter β) (fun x1 x2 => x1 • x2) fun x1 x2 => x1 ≤ x2
-- Mathlib.Algebra.Lie.Ideal
LieHom.idealRange.eq_1 : ∀ {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] (f : L →ₗ⁅R⁆ L'),
  f.idealRange = LieSubmodule.lieSpan R L' ↑f.range
-- Std.Sync.Channel
_private.Std.Sync.Channel.0.Std.CloseableChannel.Zero.State.mk.injEq : ∀ {α : Type} (producers : Std.Queue (α × IO.Promise Bool)) (consumers : Std.Queue (Std.CloseableChannel.Consumer✝ α))
  (closed : Bool) (producers_1 : Std.Queue (α × IO.Promise Bool))
  (consumers_1 : Std.Queue (Std.CloseableChannel.Consumer✝ α)) (closed_1 : Bool),
  ({ producers := producers, consumers := consumers, closed := closed } =
      { producers := producers_1, consumers := consumers_1, closed := closed_1 }) =
    (producers = producers_1 ∧ consumers = consumers_1 ∧ closed = closed_1)
-- Mathlib.SetTheory.Ordinal.Veblen
Ordinal.veblen_zero_le_veblen_zero : ∀ {o₁ o₂ : Ordinal.{u}}, Ordinal.veblen o₁ 0 ≤ Ordinal.veblen o₂ 0 ↔ o₁ ≤ o₂
-- Init.Data.Range.Polymorphic.Nat
Std.PRange.instHasSizeNat_1 : Std.Rxo.HasSize ℕ
-- Mathlib.Algebra.Star.StarAlgHom
StarAlgHom.prod_fst_snd : ∀ {R : Type u_1} {A : Type u_2} {B : Type u_3} [inst : CommSemiring R] [inst_1 : Semiring A] [inst_2 : Algebra R A]
  [inst_3 : Star A] [inst_4 : Semiring B] [inst_5 : Algebra R B] [inst_6 : Star B],
  (StarAlgHom.fst R A B).prod (StarAlgHom.snd R A B) = 1
-- Std.Time.Duration
Std.Time.Duration.instHSubOffset : HSub Std.Time.Duration Std.Time.Day.Offset Std.Time.Duration
-- Mathlib.Data.Holor
Holor.cprankMax_nil : ∀ {α : Type} [inst : Mul α] [inst_1 : AddMonoid α] (x : Holor α []), Holor.CPRankMax 1 x
-- Mathlib.CategoryTheory.Limits.Shapes.Opposites.Products
CategoryTheory.Limits.hasFiniteCoproducts_opposite : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.Limits.HasFiniteProducts C],
  CategoryTheory.Limits.HasFiniteCoproducts Cᵒᵖ
-- Mathlib.Topology.Compactification.OnePoint.Basic
/-- The point at infinity  -/
OnePoint.«term∞» : Lean.ParserDescr
-- Lean.Message
Lean.MessageData.withNamingContext.injEq : ∀ (a : Lean.NamingContext) (a_1 : Lean.MessageData) (a_2 : Lean.NamingContext) (a_3 : Lean.MessageData),
  (Lean.MessageData.withNamingContext a a_1 = Lean.MessageData.withNamingContext a_2 a_3) = (a = a_2 ∧ a_1 = a_3)
-- Mathlib.Tactic.CategoryTheory.Coherence.Datatypes
/-- The expression for the right unitor `ρ_ f`.  -/
Mathlib.Tactic.BicategoryLike.MonadMor₂Iso.rightUnitorM' : {m : Type → Type} →
  [Monad m] →
    [Mathlib.Tactic.BicategoryLike.MonadMor₂Iso m] →
      Mathlib.Tactic.BicategoryLike.Mor₁ → m Mathlib.Tactic.BicategoryLike.Mor₂Iso
-- Mathlib.Algebra.Order.GroupWithZero.Basic
div_lt_div_of_pos_left : ∀ {G₀ : Type u_3} [inst : GroupWithZero G₀] [inst_1 : PartialOrder G₀] [PosMulReflectLT G₀] [MulPosReflectLT G₀]
  {a b c : G₀}, 0 < a → 0 < c → c < b → a / b < a / c
-- Mathlib.CategoryTheory.Quotient
/-- Hom-sets of the quotient category.  -/
CategoryTheory.Quotient.Hom : {C : Type u_1} →
  [inst : CategoryTheory.Category.{v_1, u_1} C] →
    (r : HomRel C) → CategoryTheory.Quotient r → CategoryTheory.Quotient r → Type v_1
-- Mathlib.FieldTheory.RatFunc.AsPolynomial
/-- If a valuation `v` is trivial on constants and `v RatFunc.X ≤ 1` then for every polynomial `p`,
`v p ≤ 1`.  -/
Polynomial.valuation_le_one_of_valuation_X_le_one : ∀ (K : Type u_1) [inst : Field K] {Γ : Type u_2} [inst_1 : LinearOrderedCommGroupWithZero Γ]
  {v : Valuation (RatFunc K) Γ} [hv : Valuation.IsTrivialOn K v], v RatFunc.X ≤ 1 → ∀ (p : Polynomial K), v ↑p ≤ 1
-- Mathlib.Order.Filter.Map
Filter.mem_comap_iff_compl : ∀ {α : Type u_1} {β : Type u_2} {f : α → β} {l : Filter β} {s : Set α}, s ∈ Filter.comap f l ↔ (f '' sᶜ)ᶜ ∈ l
-- Init.Data.Nat.Basic
Nat.pred_ne_self : ∀ {a : ℕ}, a ≠ 0 → a.pred ≠ a
-- Mathlib.RingTheory.Algebraic.Integral
IsAlgebraic.of_finite : ∀ (R : Type u_3) {A : Type u_4} [inst : CommRing R] [Nontrivial R] [inst_2 : Ring A] [inst_3 : Algebra R A] (e : A)
  [Module.Finite R A], IsAlgebraic R e
-- Std.Tactic.BVDecide.Bitblast.BVExpr.Circuit.Impl.Expr
Std.Tactic.BVDecide.BVExpr.Cache.get? : {aig : Std.Sat.AIG Std.Tactic.BVDecide.BVBit} →
  {w : ℕ} → Std.Tactic.BVDecide.BVExpr.Cache aig → Std.Tactic.BVDecide.BVExpr w → Option (aig.RefVec w)
-- Mathlib.Topology.PartialHomeomorph.Defs
PartialHomeomorph.rightInvOn : ∀ {X : Type u_1} {Y : Type u_3} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y] (e : PartialHomeomorph X Y),
  Set.RightInvOn (↑e.symm) (↑e) e.target
-- Mathlib.RingTheory.HopfAlgebra.Basic
/-- A Hopf algebra over a commutative (semi)ring `R` is a bialgebra over `R` equipped with an
`R`-linear endomorphism `antipode` satisfying the antipode axioms.  -/
HopfAlgebra : (R : Type u) → (A : Type v) → [CommSemiring R] → [Semiring A] → Type (max u v)
-- Mathlib.Algebra.Category.Grp.Basic
CommGrpCat.coe_id : ∀ {X : CommGrpCat}, ⇑(CategoryTheory.ConcreteCategory.hom (CategoryTheory.CategoryStruct.id X)) = id
-- Mathlib.Computability.Primrec.List
_private.Mathlib.Computability.Primrec.List.0.list_foldl' : ∀ {α : Type u_1} {β : Type u_2} {σ : Type u_3} [inst : Primcodable α] [inst_1 : Primcodable β] [inst_2 : Primcodable σ]
  (H : Nat.Primrec fun n => Encodable.encode (Encodable.decode n)) {f : α → List β} {g : α → σ} {h : α → σ × β → σ},
  Primrec f → Primrec g → Primrec₂ h → Primrec fun a => List.foldl (fun s b => h a (s, b)) (g a) (f a)
-- Mathlib.RingTheory.Algebraic.Basic
isAlgebraic_ringHom_iff_of_comp_eq : ∀ {R : Type u} {S : Type u_1} {A : Type v} [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : Ring A]
  [inst_3 : Algebra R A] {B : Type u_2} [inst_4 : Ring B] [inst_5 : Algebra S B] {FRS : Type u_3} {FAB : Type u_4}
  [inst_6 : EquivLike FRS R S] [inst_7 : RingEquivClass FRS R S] [inst_8 : FunLike FAB A B]
  [inst_9 : RingHomClass FAB A B] (f : FRS) (g : FAB),
  Function.Injective ⇑g →
    (algebraMap S B).comp ↑f = (↑g).comp (algebraMap R A) → ∀ {a : A}, IsAlgebraic S (g a) ↔ IsAlgebraic R a
-- Mathlib.Data.List.Basic
List.foldr_concat : ∀ {α : Type u} {β : Type v} (f : α → β → β) (b : β) (x : α) (xs : List α),
  List.foldr f b (xs ++ [x]) = List.foldr f (f x b) xs
-- Mathlib.RingTheory.Congruence.Hom
RingCon.quotientKerEquivOfRightInverse_apply : ∀ {M : Type u_1} {P : Type u_3} [inst : NonAssocSemiring M] [inst_1 : NonAssocSemiring P] (f : M →+* P) (g : P → M)
  (hf : Function.RightInverse g ⇑f) (x : (RingCon.ker f).Quotient),
  (RingCon.quotientKerEquivOfRightInverse f g hf) x = (RingCon.kerLift f) x
-- Mathlib.LinearAlgebra.AffineSpace.Basis
AffineBasis.ind' : ∀ {ι : Type u₁} {k : Type u₂} {V : Type u₃} {P : Type u₄} [inst : AddCommGroup V] [inst_1 : AddTorsor V P]
  [inst_2 : Ring k] [inst_3 : Module k V] (self : AffineBasis ι k P), AffineIndependent k self.toFun
-- Mathlib.Data.Set.Finite.Basic
/-- This is not an instance so that it does not conflict with the one
in `Mathlib/Order/Interval/Finset/Defs.lean`.  -/
Set.Nat.fintypeIio : (n : ℕ) → Fintype ↑(Set.Iio n)
-- Mathlib.CategoryTheory.ObjectProperty.CompleteLattice
CategoryTheory.ObjectProperty.prop_sup_iff : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] (P Q : CategoryTheory.ObjectProperty C) (X : C),
  (P ⊔ Q) X ↔ P X ∨ Q X
-- Mathlib.Data.List.Nodup
List.Nodup.eq_of_getLast_mem_of_prefix : ∀ {α : Type u} {l₁ l₂ : List α}, l₁ <+: l₂ → ∀ {hne : l₂ ≠ []}, l₂.getLast hne ∈ l₁ → l₂.Nodup → l₁ = l₂
-- Std.Data.HashSet.RawLemmas
Std.HashSet.Raw.mem_iff_isSome_get? : ∀ {α : Type u} {m : Std.HashSet.Raw α} [inst : BEq α] [inst_1 : Hashable α] [EquivBEq α] [LawfulHashable α],
  m.WF → ∀ {a : α}, a ∈ m ↔ (m.get? a).isSome = true
-- Mathlib.Tactic.Linter.OverlappingInstances
/-- Return the result of `getAbstractDataProjections`, using a global cache.
To ensure soundness, the cache is only used for imported declarations.  -/
_private.Mathlib.Tactic.Linter.OverlappingInstances.0.Mathlib.Linter.OverlappingInstances.getAbstractProjectionsCached : Lean.Name → Lean.CoreM (Array Lean.Expr)
-- Mathlib.Order.OrderDual
OrderDual.exists : ∀ {α : Type u_1} {p : αᵒᵈ → Prop}, (∃ a, p a) ↔ ∃ a, p (OrderDual.toDual a)
-- Std.Data.DHashMap.Internal.Model
Std.DHashMap.Internal.Raw₀.replaceₘ.eq_1 : ∀ {α : Type u} {β : α → Type v} [inst : BEq α] [inst_1 : Hashable α] (m : Std.DHashMap.Internal.Raw₀ α β) (a : α)
  (b : β a),
  m.replaceₘ a b =
    ⟨{ size := (↑m).size,
        buckets :=
          Std.DHashMap.Internal.updateBucket (↑m).buckets ⋯ a fun l => Std.DHashMap.Internal.AssocList.replace a b l },
      ⋯⟩
-- Mathlib.GroupTheory.Commensurable
Subgroup.Commensurable.symm : ∀ {G : Type u_1} [inst : Group G] {H K : Subgroup G}, H.Commensurable K → K.Commensurable H
-- Mathlib.Algebra.Group.Commute.Units
Units.ofPowEqOne.eq_1 : ∀ {M : Type u_1} [inst : Monoid M] (a : M) (n : ℕ) (ha : a ^ n = 1) (hn : n ≠ 0),
  Units.ofPowEqOne a n ha hn = Units.ofPow 1 a hn ha
-- Mathlib.Data.PNat.Find
/-- If `p` is a (decidable) predicate on `ℕ+` and `hp : ∃ (n : ℕ+), p n` is a proof that
there exists some positive natural number satisfying `p`, then `PNat.find hp` is the
smallest positive natural number satisfying `p`. Note that `PNat.find` is protected,
meaning that you can't just write `find`, even if the `PNat` namespace is open.

The API for `PNat.find` is:

* `PNat.find_spec` is the proof that `PNat.find hp` satisfies `p`.
* `PNat.find_min` is the proof that if `m < PNat.find hp` then `m` does not satisfy `p`.
* `PNat.find_min'` is the proof that if `m` does satisfy `p` then `PNat.find hp ≤ m`.
 -/
PNat.find : {p : ℕ+ → Prop} → [DecidablePred p] → (∃ n, p n) → ℕ+
-- Mathlib.RingTheory.Finiteness.Ideal
Ideal.exists_radical_pow_le_of_fg : ∀ {R : Type u_3} [inst : CommSemiring R] (I : Ideal R), I.radical.FG → ∃ n, I.radical ^ n ≤ I
-- Std.Data.ByteSlice
instSelfSliceByteSliceDataByteSlice : Std.Slice.Self (Std.Slice Std.Slice.Internal.ByteSliceData) ByteSlice
-- Mathlib.RingTheory.Ideal.AssociatedPrime.Finiteness
Submodule.isQuotientEquivQuotientPrime_iff : ∀ {A : Type u} [inst : CommRing A] {M : Type v} [inst_1 : AddCommGroup M] [inst_2 : Module A M] {N₁ N₂ : Submodule A M},
  N₁.IsQuotientEquivQuotientPrime N₂ ↔ ∃ x, (⊥.colon {N₁.mkQ x}).IsPrime ∧ N₂ = N₁ ⊔ A ∙ x
-- Mathlib.Probability.Distributions.Gaussian.Multivariate
ProbabilityTheory.covarianceBilin_multivariateGaussian : ∀ {ι : Type u_1} [inst : Fintype ι] [inst_1 : DecidableEq ι] {μ : EuclideanSpace ℝ ι} {S : Matrix ι ι ℝ},
  S.PosSemidef →
    ∀ (x y : EuclideanSpace ℝ ι),
      ((ProbabilityTheory.covarianceBilin (ProbabilityTheory.multivariateGaussian μ S)) x) y = x.ofLp ⬝ᵥ S.mulVec y.ofLp
-- Batteries.Util.LibraryNote
Batteries.Util.LibraryNote.instInhabitedLibraryNoteEntry : Inhabited Batteries.Util.LibraryNote.LibraryNoteEntry
-- Mathlib.Algebra.Group.Submonoid.Support
/-- The support of a submonoid is the largest subgroup it contains.  -/
AddSubgroup.gc_toAddSubmonoid_support : ∀ {G : Type u_1} [inst : AddGroup G], GaloisConnection AddSubgroup.toAddSubmonoid AddSubmonoid.support
-- Mathlib.Analysis.Normed.Operator.LinearIsometry
LinearIsometryEquiv.coe_trans : ∀ {R : Type u_1} {R₂ : Type u_2} {R₃ : Type u_3} {E : Type u_5} {E₂ : Type u_6} {E₃ : Type u_7} [inst : Semiring R]
  [inst_1 : Semiring R₂] [inst_2 : Semiring R₃] {σ₁₂ : R →+* R₂} {σ₂₁ : R₂ →+* R} {σ₁₃ : R →+* R₃} {σ₃₁ : R₃ →+* R}
  {σ₂₃ : R₂ →+* R₃} {σ₃₂ : R₃ →+* R₂} [inst_3 : RingHomInvPair σ₁₂ σ₂₁] [inst_4 : RingHomInvPair σ₂₁ σ₁₂]
  [inst_5 : RingHomInvPair σ₁₃ σ₃₁] [inst_6 : RingHomInvPair σ₃₁ σ₁₃] [inst_7 : RingHomInvPair σ₂₃ σ₃₂]
  [inst_8 : RingHomInvPair σ₃₂ σ₂₃] [inst_9 : RingHomCompTriple σ₁₂ σ₂₃ σ₁₃] [inst_10 : RingHomCompTriple σ₃₂ σ₂₁ σ₃₁]
  [inst_11 : SeminormedAddCommGroup E] [inst_12 : SeminormedAddCommGroup E₂] [inst_13 : SeminormedAddCommGroup E₃]
  [inst_14 : Module R E] [inst_15 : Module R₂ E₂] [inst_16 : Module R₃ E₃] (e₁ : E ≃ₛₗᵢ[σ₁₂] E₂) (e₂ : E₂ ≃ₛₗᵢ[σ₂₃] E₃),
  ⇑(e₁.trans e₂) = ⇑e₂ ∘ ⇑e₁
-- Mathlib.NumberTheory.NumberField.CanonicalEmbedding.PolarCoord
NumberField.mixedEmbedding.homeoRealMixedSpacePolarSpace_apply_fst_ofIsComplex : ∀ (K : Type u_1) [inst : Field K] (x : NumberField.mixedEmbedding.realMixedSpace K) (w : { w // w.IsComplex }),
  ((NumberField.mixedEmbedding.homeoRealMixedSpacePolarSpace K) x).1 ↑w = (x.2 w).1
-- Mathlib.Combinatorics.SimpleGraph.Ends.Defs
SimpleGraph.ComponentCompl.supp_injective : ∀ {V : Type u} {G : SimpleGraph V} {K : Set V}, Function.Injective SimpleGraph.ComponentCompl.supp
-- Mathlib.Algebra.Homology.ShortComplex.Exact
CategoryTheory.ShortComplex.Exact.rightHomologyDataOfIsColimitCokernelCofork_p : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Preadditive C]
  {S : CategoryTheory.ShortComplex C} (hS : S.Exact) [inst_2 : CategoryTheory.Limits.HasZeroObject C]
  (cc : CategoryTheory.Limits.CokernelCofork S.f) (hcc : CategoryTheory.Limits.IsColimit cc),
  (hS.rightHomologyDataOfIsColimitCokernelCofork cc hcc).p = CategoryTheory.Limits.Cofork.π cc
-- Mathlib.Data.Set.Card
Set.Finite.ncard_strictMonoOn : ∀ {α : Type u_1}, StrictMonoOn Set.ncard (Set.ofPred Set.Finite)