mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Topology.Closure
Filter.HasBasis.lift'_interior_eq_self : ∀ {X : Type u} [inst : TopologicalSpace X] {ι : Sort v} {l : Filter X} {p : ι → Prop} {s : ι → Set X},
  l.HasBasis p s → (∀ (i : ι), p i → IsOpen (s i)) → l.lift' interior = l
-- Mathlib.Topology.Algebra.Valued.WithVal
WithVal.ofVal_smul : ∀ {R : Type u_1} {Γ₀ : Type u_2} [inst : LinearOrderedCommGroupWithZero Γ₀] [inst_1 : Ring R] (v : Valuation R Γ₀)
  {S : Type u_3} [inst_2 : SMul S R] (s : S) (x : WithVal v), (s • x).ofVal = s • x.ofVal
-- Mathlib.Analysis.SpecialFunctions.Exponential
/-- The exponential map in `𝕂 = ℝ` or `𝕂 = ℂ` has derivative `NormedSpace.exp x`
at any point `x`.  -/
hasDerivAt_exp : ∀ {𝕂 : Type u_1} [inst : RCLike 𝕂] {x : 𝕂}, HasDerivAt NormedSpace.exp (NormedSpace.exp x) x
-- Mathlib.RingTheory.Ideal.Operations
Ideal.span_singleton_mul_le_span_singleton_mul : ∀ {R : Type u} [inst : CommSemiring R] {x y : R} {I J : Ideal R},
  Ideal.span {x} * I ≤ Ideal.span {y} * J ↔ ∀ zI ∈ I, ∃ zJ ∈ J, x * zI = y * zJ
-- Mathlib.Tactic.TermCongr
/-- Argument processing loop
- `i` is index into `lhsArgs`/`rhsArgs`.
- `finfo` is the funinfo of `f` applied to the first `finfoIdx` arguments
- `f` and `f'` are the current head functions, after the first `i` arguments have been applied.
 -/
_private.Mathlib.Tactic.TermCongr.0.Mathlib.Tactic.TermCongr.mkCongrOfApp.go : ℕ →
  ℕ →
    ℕ →
      Array Lean.Expr →
        Array Lean.Expr →
          ℕ →
            Lean.Meta.FunInfo →
              ℕ → Lean.Expr → Lean.Expr → Lean.Expr → Mathlib.Tactic.TermCongr.M Mathlib.Tactic.TermCongr.CongrResult
-- Std.Data.DTreeMap.Lemmas
Std.DTreeMap.Equiv.of_keys_unit_perm : ∀ {α : Type u} {cmp : α → α → Ordering} {t₁ t₂ : Std.DTreeMap α (fun x => Unit) cmp}, t₁.keys.Perm t₂.keys → t₁.Equiv t₂
-- Mathlib.GroupTheory.MonoidLocalization.Order
AddLocalization.le : {α : Type u_1} →
  [inst : AddCommMonoid α] →
    [inst_1 : PartialOrder α] → [IsOrderedCancelAddMonoid α] → {s : AddSubmonoid α} → LE (AddLocalization s)
-- Mathlib.Combinatorics.Enumerative.Pentagonal.PowerSeries
/-- **Pentagonal number theorem** for power series, expressed as the statement that the coefficients
of the product `∏ n, 1 - X ^ (n + 1)` are eventually constants as `(pentagonalSeries R).coeff`.  -/
PowerSeries.coeff_prod_one_sub_X_pow_eventually_eq : ∀ (R : Type u_1) [inst : CommRing R] (n : ℕ),
  ∀ᶠ (s : Finset ℕ) in Filter.atTop,
    (PowerSeries.coeff n) (∏ n ∈ s, (1 - PowerSeries.X ^ (n + 1))) =
      (PowerSeries.coeff n) (PowerSeries.pentagonalSeries R)
-- Mathlib.Algebra.Order.Monoid.Canonical.Defs
min_add_distrib' : ∀ {α : Type u} [inst : AddMonoid α] [inst_1 : LinearOrder α] [CanonicallyOrderedAdd α] (a b c : α),
  min (a + b) c = min (min a c + min b c) c
-- Mathlib.CategoryTheory.Sites.Sieves
CategoryTheory.Sieve.ofArrows_eq_ofObjects : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {X : C} (hX : CategoryTheory.Limits.IsTerminal X)
  {I : Type u_1} (Y : I → C) (f : (i : I) → Y i ⟶ X),
  CategoryTheory.Sieve.ofArrows Y f = CategoryTheory.Sieve.ofObjects Y X
-- Mathlib.Combinatorics.Matroid.Rank.Cardinal
Matroid.cRk.eq_1 : ∀ {α : Type u} (M : Matroid α) (X : Set α), M.cRk X = (M.restrict X).cRank
-- Mathlib.Topology.Order.OrderClosed
closure_Iic : ∀ {α : Type u} [inst : TopologicalSpace α] [inst_1 : Preorder α] [ClosedIicTopology α] (a : α),
  closure (Set.Iic a) = Set.Iic a
-- Mathlib.CategoryTheory.Preadditive.Basic
CategoryTheory.Preadditive.instAddCommGroupEnd : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    [CategoryTheory.Preadditive C] → (X : C) → AddCommGroup (CategoryTheory.End X)
-- Mathlib.Algebra.Star.NonUnitalSubalgebra
NonUnitalStarAlgHom.coe_range : ∀ {F : Type v'} {R : Type u} {A : Type v} {B : Type w} [inst : CommSemiring R] [inst_1 : NonUnitalNonAssocSemiring A]
  [inst_2 : Module R A] [inst_3 : Star A] [inst_4 : NonUnitalNonAssocSemiring B] [inst_5 : Module R B] [inst_6 : Star B]
  [inst_7 : FunLike F A B] [inst_8 : NonUnitalAlgHomClass F R A B] [inst_9 : StarHomClass F A B] (φ : F),
  ↑(NonUnitalStarAlgHom.range φ) = Set.range ⇑φ
-- Mathlib.Algebra.Order.GroupWithZero.Basic
Monotone.const_mul : ∀ {α : Type u_1} {M₀ : Type u_2} [inst : MonoidWithZero M₀] [inst_1 : Preorder M₀] {a : M₀} [inst_2 : Preorder α]
  {f : α → M₀} [PosMulMono M₀], Monotone f → 0 ≤ a → Monotone fun x => a * f x
-- Aesop.Forward.State
/-- Modify the `InstMap` associated to variable `var`. If no such `InstMap`
exists, the function `f` is applied to the empty `InstMap` and the result is
associated with `var`. Returns the new variable map and the result of `f`.  -/
Aesop.VariableMap.modifyM : {m : Type u_1 → Type u_2} →
  {α : Type u_1} →
    [Monad m] →
      Aesop.VariableMap → Aesop.PremiseIndex → (Aesop.InstMap → m (Aesop.InstMap × α)) → m (Aesop.VariableMap × α)
-- Lean.Data.JsonRpc
Lean.JsonRpc.Message.notification.sizeOf_spec : ∀ (method : String) (params? : Option Lean.Json.Structured),
  sizeOf (Lean.JsonRpc.Message.notification method params?) = 1 + sizeOf method + sizeOf params?
-- Mathlib.CategoryTheory.Limits.Shapes.Multiequalizer
CategoryTheory.Limits.MulticospanIndex.multiforkEquivPiForkOfIsLimit_inverse : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {J : CategoryTheory.Limits.MulticospanShape}
  (I : CategoryTheory.Limits.MulticospanIndex J C) {c : CategoryTheory.Limits.Fan I.left}
  (hc : CategoryTheory.Limits.IsLimit c) {d : CategoryTheory.Limits.Fan I.right} (hd : CategoryTheory.Limits.IsLimit d),
  (I.multiforkEquivPiForkOfIsLimit hc hd).inverse = I.ofPiForkFunctor hd
-- Mathlib.Topology.Algebra.Group.Basic
Inseparable.inv : ∀ {G : Type w} [inst : TopologicalSpace G] [inst_1 : Inv G] [ContinuousInv G] {x y : G},
  Inseparable x y → Inseparable x⁻¹ y⁻¹
-- Mathlib.RingTheory.WittVector.DiscreteValuationRing
_private.Mathlib.RingTheory.WittVector.DiscreteValuationRing.0.WittVector.inverseCoeff.match_1.eq_1 : ∀ (motive : ℕ → Sort u_1) (h_1 : Unit → motive 0) (h_2 : (n : ℕ) → motive n.succ),
  (match 0 with
    | 0 => h_1 ()
    | n.succ => h_2 n) =
    h_1 ()
-- Mathlib.AlgebraicTopology.SimplicialSet.NonDegenerateSimplicesColimit
_private.Mathlib.AlgebraicTopology.SimplicialSet.NonDegenerateSimplicesColimit.0.SSet.isColimitCoconeN.multicoequalizerDiagram : ∀ (X : SSet), ⊤.MulticoequalizerDiagram (fun x => x.subcomplex) fun x y => x.subcomplex ⊓ y.subcomplex
-- Mathlib.RingTheory.Bialgebra.MonoidAlgebra
MonoidAlgebra.bialgHom_ext_iff : ∀ {R : Type u_1} {A : Type u_3} {B : Type u_4} {M : Type u_8} [inst : CommSemiring R] [inst_1 : Semiring A]
  [inst_2 : Semiring B] [inst_3 : Bialgebra R A] [inst_4 : Bialgebra R B] [inst_5 : Monoid M]
  {φ₁ φ₂ : MonoidAlgebra A M →ₐc[R] B},
  φ₁ = φ₂ ↔
    (∀ (m : M), φ₁ (MonoidAlgebra.single m 1) = φ₂ (MonoidAlgebra.single m 1)) ∧
      (↑φ₁).comp MonoidAlgebra.singleOneAlgHom = (↑φ₂).comp MonoidAlgebra.singleOneAlgHom
-- Std.Data.TreeSet.Lemmas
Std.TreeSet.max!_le : ∀ {α : Type u} {cmp : α → α → Ordering} {t : Std.TreeSet α cmp} [Std.TransCmp cmp] [inst : Inhabited α],
  t.isEmpty = false → ∀ {k : α}, (cmp t.max! k).isLE = true ↔ ∀ k' ∈ t, (cmp k' k).isLE = true
-- Mathlib.CategoryTheory.Monad.Algebra
CategoryTheory.Monad.Algebra.mk : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    {T : CategoryTheory.Monad C} →
      (A : C) →
        (a : T.obj A ⟶ A) →
          autoParam (CategoryTheory.CategoryStruct.comp (T.η.app A) a = CategoryTheory.CategoryStruct.id A)
              CategoryTheory.Monad.Algebra.unit._autoParam →
            autoParam
                (CategoryTheory.CategoryStruct.comp (T.μ.app A) a = CategoryTheory.CategoryStruct.comp (T.map a) a)
                CategoryTheory.Monad.Algebra.assoc._autoParam →
              T.Algebra
-- Mathlib.RingTheory.Ideal.Operations
Ideal.sup_multiset_prod_eq_top : ∀ {R : Type u} [inst : CommSemiring R] {I : Ideal R} {s : Multiset (Ideal R)}, (∀ p ∈ s, I ⊔ p = ⊤) → I ⊔ s.prod = ⊤
-- Mathlib.Analysis.Calculus.IteratedDeriv.Defs
iteratedDeriv_zero : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {F : Type u_2} [inst_1 : NormedAddCommGroup F]
  [inst_2 : NormedSpace 𝕜 F] {f : 𝕜 → F}, iteratedDeriv 0 f = f
-- Mathlib.Tactic.ComputeAsymptotics.Multiseries.Basic
Tactic.ComputeAsymptotics.MultiseriesExpansion.const.eq_1 : ∀ (c : ℝ),
  Tactic.ComputeAsymptotics.MultiseriesExpansion.const [] c = Tactic.ComputeAsymptotics.MultiseriesExpansion.ofReal c
-- Mathlib.Combinatorics.SimpleGraph.Coloring.EdgeLabeling
SimpleGraph.EdgeLabeling.labelGraph_le : ∀ {V : Type u_1} {G : SimpleGraph V} {K : Type u_3} (C : G.EdgeLabeling K) {k : K}, C.labelGraph k ≤ G
-- Std.Data.DTreeMap.Internal.Model
Std.DTreeMap.Internal.Impl.link2.eq_2 : ∀ {α : Type u} {β : α → Type v} (szr : ℕ) (k'' : α) (v'' : β k'') (l'' r'' : Std.DTreeMap.Internal.Impl α β)
  (hr_2 : (Std.DTreeMap.Internal.Impl.inner szr k'' v'' l'' r'').Balanced)
  (hr_4 : Std.DTreeMap.Internal.Impl.leaf.Balanced),
  (Std.DTreeMap.Internal.Impl.inner szr k'' v'' l'' r'').link2 Std.DTreeMap.Internal.Impl.leaf hr_2 hr_4 =
    { impl := Std.DTreeMap.Internal.Impl.inner szr k'' v'' l'' r'', balanced_impl := ⋯, size_impl := ⋯ }
-- Mathlib.Algebra.QuadraticAlgebra.Basic
QuadraticAlgebra.omega_mul_omega_eq_add : ∀ {R : Type u_2} {a b : R} [inst : CommSemiring R],
  QuadraticAlgebra.omega * QuadraticAlgebra.omega = a • 1 + b • QuadraticAlgebra.omega
-- Mathlib.RepresentationTheory.Homological.GroupCohomology.LowDegree
groupCohomology.isMulCoboundary₁_of_mem_coboundaries₁ : ∀ {G M : Type} [inst : Group G] [inst_1 : CommGroup M] [inst_2 : MulDistribMulAction G M],
  ∀ f ∈ groupCohomology.coboundaries₁ (Rep.ofMulDistribMulAction G M),
    groupCohomology.IsMulCoboundary₁ (⇑Additive.ofMul ∘ f)
-- Mathlib.CategoryTheory.Bicategory.Adjunction.Basic
CategoryTheory.Bicategory.right_triangle_of_left_triangle : ∀ {B : Type u₁} [inst : CategoryTheory.Bicategory B] {a b : B} {f : a ⟶ b} {g : b ⟶ a}
  (η : CategoryTheory.CategoryStruct.id a ≅ CategoryTheory.CategoryStruct.comp f g)
  (ε : CategoryTheory.CategoryStruct.comp g f ≅ CategoryTheory.CategoryStruct.id b),
  CategoryTheory.Bicategory.leftZigzag η.hom ε.hom =
      CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.leftUnitor f).hom
        (CategoryTheory.Bicategory.rightUnitor f).inv →
    CategoryTheory.Bicategory.rightZigzag η.hom ε.hom =
      CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.rightUnitor g).hom
        (CategoryTheory.Bicategory.leftUnitor g).inv
-- Mathlib.GroupTheory.Perm.Cycle.Factors
Equiv.Perm.Disjoint.cycleFactorsFinset_mul_eq_union : ∀ {α : Type u_2} [inst : DecidableEq α] [inst_1 : Fintype α] {f g : Equiv.Perm α},
  f.Disjoint g → (f * g).cycleFactorsFinset = f.cycleFactorsFinset ∪ g.cycleFactorsFinset
-- Mathlib.CategoryTheory.Limits.Shapes.Pullback.HasPullback
CategoryTheory.Limits.walkingCospanOpEquiv_functor_obj : ∀ (X : (CategoryTheory.Limits.WidePullbackShape CategoryTheory.Limits.WalkingPair)ᵒᵖ),
  CategoryTheory.Limits.walkingCospanOpEquiv.functor.obj X = Opposite.unop X
-- Mathlib.SetTheory.Cardinal.Basic
Cardinal.mk_univ : ∀ {α : Type u}, Cardinal.mk ↑Set.univ = Cardinal.mk α
-- Mathlib.GroupTheory.Coset.Basic
AddSubgroup.rightCosetEquivAddSubgroup.eq_1 : ∀ {α : Type u_1} [inst : AddGroup α] {s : AddSubgroup α} (g : α),
  AddSubgroup.rightCosetEquivAddSubgroup g =
    { toFun := fun x => ⟨↑x + -g, ⋯⟩, invFun := fun x => ⟨↑x + g, ⋯⟩, left_inv := ⋯, right_inv := ⋯ }
-- Mathlib.Data.Matrix.Basic
/-- Extracting entries from a matrix as an additive homomorphism.  -/
Matrix.entryAddHom : {m : Type u_2} → {n : Type u_3} → (α : Type u_11) → [inst : Add α] → m → n → Matrix m n α →ₙ+ α
-- Mathlib.CategoryTheory.Limits.HasLimits
CategoryTheory.Limits.coneOfAdj_π : ∀ {J : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} J] {C : Type u} [inst_1 : CategoryTheory.Category.{v, u} C]
  {L : CategoryTheory.Functor (CategoryTheory.Functor J C) C} (adj : CategoryTheory.Functor.const J ⊣ L)
  (F : CategoryTheory.Functor J C), (CategoryTheory.Limits.coneOfAdj adj F).π = adj.counit.app F
-- Mathlib.CategoryTheory.Functor.KanExtension.Adjunction
CategoryTheory.Functor.leftKanExtensionUnit_leftKanExtensionObjIsoColimit_hom_assoc : ∀ {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] (F : CategoryTheory.Functor C H)
  [inst_3 : L.HasPointwiseLeftKanExtension F] (X : C) {Z : H}
  (h : CategoryTheory.Limits.colimit ((CategoryTheory.CostructuredArrow.proj L (L.obj X)).comp F) ⟶ Z),
  CategoryTheory.CategoryStruct.comp ((L.leftKanExtensionUnit F).app X)
      (CategoryTheory.CategoryStruct.comp (L.leftKanExtensionObjIsoColimit F (L.obj X)).hom h) =
    CategoryTheory.CategoryStruct.comp
      (CategoryTheory.Limits.colimit.ι ((CategoryTheory.CostructuredArrow.proj L (L.obj X)).comp F)
        (CategoryTheory.CostructuredArrow.mk (CategoryTheory.CategoryStruct.id (L.obj X))))
      h
-- Mathlib.CategoryTheory.Limits.Shapes.NormalMono.Basic
/-- In a category in which every monomorphism is normal, we can express every monomorphism as
a kernel. This is not an instance because it would create an instance loop.  -/
CategoryTheory.normalMonoOfMono : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    {X Y : C} →
      [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C] →
        [CategoryTheory.IsNormalMonoCategory C] → (f : X ⟶ Y) → [CategoryTheory.Mono f] → CategoryTheory.NormalMono f
-- Mathlib.Tactic.CategoryTheory.Coherence
Mathlib.Tactic.Coherence.LiftObj.lift : {C : Type u} → (X : C) → [self : Mathlib.Tactic.Coherence.LiftObj X] → CategoryTheory.FreeMonoidalCategory C
-- Mathlib.Data.Part
Part.not_none_dom : ∀ {α : Type u_1}, ¬Part.none.Dom
-- Mathlib.Algebra.Group.ULift
ULift.commGroup : {α : Type u} → [CommGroup α] → CommGroup (ULift.{u_1, u} α)
-- Mathlib.Logic.Equiv.Basic
Equiv.sigmaSubtype_symm_apply_coe_fst : ∀ {α : Type u_9} {β : α → Type u_10} (a : α) (b : β a), (↑((Equiv.sigmaSubtype a).symm b)).fst = a
-- Std.Tactic.BVDecide.Bitblast.BVExpr.Basic
Std.Tactic.BVDecide.BVLogicalExpr.eval_not : ∀ {assign : Std.Tactic.BVDecide.BVExpr.Assignment} {x : Std.Tactic.BVDecide.BoolExpr Std.Tactic.BVDecide.BVPred},
  Std.Tactic.BVDecide.BVLogicalExpr.eval assign x.not = !Std.Tactic.BVDecide.BVLogicalExpr.eval assign x
-- Mathlib.Algebra.Category.Ring.Colimits
CommRingCat.Colimits.Relation.below.neg_add_cancel : ∀ {J : Type v} [inst : CategoryTheory.SmallCategory J] {F : CategoryTheory.Functor J CommRingCat}
  {motive : (a a_1 : CommRingCat.Colimits.Prequotient F) → CommRingCat.Colimits.Relation F a a_1 → Prop}
  (x : CommRingCat.Colimits.Prequotient F), CommRingCat.Colimits.Relation.below ⋯
-- Init.Meta.Defs
/-- This function can be used to detect whether the compiler has support for
generating LLVM instead of C. It is used by lake instead of the --features
flag in order to avoid having to run a compiler for this every time on startup.
See #2572.
 -/
Lean.Internal.hasLLVMBackend : Unit → Bool
-- Std.Data.ExtTreeMap.Basic
Std.ExtTreeMap.instSDiffOfTransCmp : {α : Type u} → {β : Type v} → {cmp : α → α → Ordering} → [Std.TransCmp cmp] → SDiff (Std.ExtTreeMap α β cmp)
-- Mathlib.CategoryTheory.Limits.Cones
CategoryTheory.Limits.coneUnopOfCocone.eq_1 : ∀ {J : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} J] {C : Type u₃} [inst_1 : CategoryTheory.Category.{v₃, u₃} C]
  {F : CategoryTheory.Functor Jᵒᵖ Cᵒᵖ} (c : CategoryTheory.Limits.Cocone F),
  CategoryTheory.Limits.coneUnopOfCocone c = { pt := Opposite.unop c.pt, π := CategoryTheory.NatTrans.unop c.ι }
-- Std.Time.Date.Basic
/-- Convert `Day.Offset` into `Millisecond.Offset`.
 -/
Std.Time.Millisecond.Offset.ofDays : Std.Time.Day.Offset → Std.Time.Millisecond.Offset
-- Mathlib.Analysis.Normed.Unbundled.SpectralNorm
/-- The function `ℕ → ℝ` sending `n` to `‖ p.coeff n ‖^(1/(p.natDegree - n : ℝ))`, if
`n < p.natDegree`, or to `0` otherwise.  -/
spectralValueTerms : {R : Type u_1} → [inst : SeminormedRing R] → Polynomial R → ℕ → ℝ
-- Mathlib.NumberTheory.Cyclotomic.CyclotomicCharacter
/-- Suppose `L` is a domain containing all `pⁱ`-th primitive roots with `p` a (rational) prime.
If `g` is a ring automorphism of `L`, then `cyclotomicCharacter L p g` is the unique `j : ℤₚ` such
that `g(ζ) = ζ ^ (j mod pⁱ)` for all `pⁱ`-th roots of unity `ζ`.

Note: This is the trivial character when `L` does not contain all `pⁱ`-th primitive roots.
 -/
cyclotomicCharacter : (L : Type u) → [inst : CommRing L] → [IsDomain L] → (p : ℕ) → [inst_2 : Fact (Nat.Prime p)] → (L ≃+* L) →* ℤ_[p]ˣ
-- Mathlib.Order.CountableSupClosed
CountableSupClosed.of_iSup_mem : ∀ {α : Type u_2} {s : Set α} [inst : CompleteLattice α],
  (∀ (A : ℕ → α), (∀ (n : ℕ), A n ∈ s) → ⨆ n, A n ∈ s) → CountableSupClosed s
-- Mathlib.Tactic.ClickSuggestions.Util
/-- Get the syntax of the variable whose type the user selected.  -/
Mathlib.Tactic.ClickSuggestions.getHypIdent? : Mathlib.Tactic.ClickSuggestions.ClickSuggestionsM (Option Lean.Ident)
-- Mathlib.Analysis.SpecialFunctions.Complex.Log
Complex.exp_eq_exp_iff_exists_int : ∀ {x y : ℂ}, Complex.exp x = Complex.exp y ↔ ∃ n, x = y + ↑n * (2 * ↑Real.pi * Complex.I)
-- Mathlib.Algebra.Polynomial.Basic
Polynomial.instMul : {R : Type u} → [inst : Semiring R] → Mul (Polynomial R)
-- Mathlib.Analysis.InnerProductSpace.GramSchmidtOrtho
InnerProductSpace.gramSchmidtOrthonormalBasis.congr_simp : ∀ {𝕜 : Type u_1} {E : Type u_2} [inst : RCLike 𝕜] [inst_1 : NormedAddCommGroup E] [inst_2 : InnerProductSpace 𝕜 E]
  {ι : Type u_3} [inst_3 : LinearOrder ι] [inst_4 : LocallyFiniteOrderBot ι] [inst_5 : WellFoundedLT ι]
  [inst_6 : Fintype ι] [inst_7 : FiniteDimensional 𝕜 E] (h : Module.finrank 𝕜 E = Fintype.card ι) (f f_1 : ι → E),
  f = f_1 → InnerProductSpace.gramSchmidtOrthonormalBasis h f = InnerProductSpace.gramSchmidtOrthonormalBasis h f_1
-- Lean.Elab.ConfigEval.DeriveEvalConfigItem
/-- Constant to use for terminfo. The root of the trie does not have this set.
Collected from `EvalConfigItemHandler.projFn?`.  -/
_private.Lean.Elab.ConfigEval.DeriveEvalConfigItem.0.Lean.Elab.ConfigEval.HandlerTrie.projFn? : Lean.Elab.ConfigEval.HandlerTrie✝ → Option Lean.Name
-- Std.Data.ExtTreeMap.Lemmas
Std.ExtTreeMap.size_alter : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Std.ExtTreeMap α β cmp} [inst : Std.TransCmp cmp] {k : α}
  {f : Option β → Option β},
  (t.alter k f).size =
    if k ∈ t ∧ (f t[k]?).isNone = true then t.size - 1
    else if k ∉ t ∧ (f t[k]?).isSome = true then t.size + 1 else t.size
-- Mathlib.Geometry.Euclidean.Volume.Measure
/-- A measurable equivalence between an affine space and its orthogonal decomposition by a base
point and a direction. We show that this is measure preserving between `μHE[finrank ℝ V]` and
`volume` at `Submodule.measurePreserving_measurableEquivProd`.

This is similar to `Submodule.orthogonalDecomposition` as a `MeasurableEquiv`, but as the right-hand
side is not with L²-norm, this is not an isometry.
 -/
Submodule.measurableEquivProd : {V : Type u_3} →
  {P : Type u_4} →
    [inst : NormedAddCommGroup V] →
      [inst_1 : InnerProductSpace ℝ V] →
        [inst_2 : MeasurableSpace V] →
          [BorelSpace V] →
            [FiniteDimensional ℝ V] →
              [inst_5 : MetricSpace P] →
                [inst_6 : MeasurableSpace P] →
                  [BorelSpace P] → [NormedAddTorsor V P] → (s : Submodule ℝ V) → P → P ≃ᵐ ↥s × ↥sᗮ
-- Lean.Environment
Lean.Kernel.Exception.alreadyDeclared.injEq : ∀ (env : Lean.Kernel.Environment) (name : Lean.Name) (env_1 : Lean.Kernel.Environment) (name_1 : Lean.Name),
  (Lean.Kernel.Exception.alreadyDeclared env name = Lean.Kernel.Exception.alreadyDeclared env_1 name_1) =
    (env = env_1 ∧ name = name_1)
-- Mathlib.Order.Filter.IsBounded
Filter.isCobounded_principal : ∀ {α : Type u_1} {r : α → α → Prop} (s : Set α),
  Filter.IsCobounded r (Filter.principal s) ↔ ∃ b, ∀ (a : α), (∀ x ∈ s, r x a) → r b a
-- Lean.Elab.DeprecatedArg
Lean.Elab.instInhabitedDeprecatedArgEntry : Inhabited Lean.Elab.DeprecatedArgEntry
-- Mathlib.Combinatorics.Additive.AP.Three.Behrend
Behrend.mem_box : ∀ {n d : ℕ} {x : Fin n → ℕ}, x ∈ Behrend.box n d ↔ ∀ (i : Fin n), x i < d
-- Mathlib.RingTheory.Kaehler.TensorProduct
KaehlerDifferential.tensorKaehlerEquiv_tmul_D : ∀ (R : Type u_1) (S : Type u_2) (A : Type u_3) (B : Type u_4) [inst : CommRing R] [inst_1 : CommRing S]
  [inst_2 : Algebra R S] [inst_3 : CommRing A] [inst_4 : CommRing B] [inst_5 : Algebra R A] [inst_6 : Algebra R B]
  [inst_7 : Algebra A B] [inst_8 : Algebra S B] [inst_9 : IsScalarTower R A B] [inst_10 : IsScalarTower R S B]
  [inst_11 : Algebra.IsPushout R S A B] (b : B) (a : A),
  (KaehlerDifferential.tensorKaehlerEquiv R S A B) (b ⊗ₜ[A] (KaehlerDifferential.D R A) a) =
    b • (KaehlerDifferential.D S B) ((algebraMap A B) a)
-- Mathlib.Order.Filter.Defs
/-- A variant on `bind` using a function `g` taking a set instead of a member of `α`.
This is essentially a push-forward along a function mapping each set to a filter.  -/
Filter.lift : {α : Type u_1} → {β : Type u_2} → Filter α → (Set α → Filter β) → Filter β
-- Init.Data.List.Find
List.findIdx?_eq_guard_findIdx_lt : ∀ {α : Type u_1} {xs : List α} {p : α → Bool},
  List.findIdx? p xs = Option.guard (fun i => decide (i < xs.length)) (List.findIdx p xs)
-- Init.Data.UInt.Lemmas
UInt32.le_antisymm_iff : ∀ {a b : UInt32}, a = b ↔ a ≤ b ∧ b ≤ a
-- Mathlib.RingTheory.HahnSeries.Basic
HahnSeries.support_mk : ∀ {Γ : Type u_1} {R : Type u_3} [inst : PartialOrder Γ] [inst_1 : Zero R] (f : Γ → R) (h : (Function.support f).IsPWO),
  { coeff := f, isPWO_support' := h }.support = Function.support f
-- Mathlib.Order.Preorder.Chain
subset_succChain : ∀ {α : Type u_1} {r : α → α → Prop} {s : Set α}, s ⊆ SuccChain r s
-- Mathlib.Algebra.Group.Submonoid.Basic
Submonoid.mem_iInf : ∀ {M : Type u_1} [inst : MulOneClass M] {ι : Sort u_4} {S : ι → Submonoid M} {x : M}, x ∈ ⨅ i, S i ↔ ∀ (i : ι), x ∈ S i
-- Mathlib.Algebra.Homology.HomotopyCategory.Pretriangulated
CochainComplex.mappingCone.triangleMapOfHomotopy_comm₂_assoc : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Preadditive C]
  [inst_2 : CategoryTheory.Limits.HasBinaryBiproducts C] {K₁ L₁ K₂ L₂ : CochainComplex C ℤ} {φ₁ : K₁ ⟶ L₁}
  {φ₂ : K₂ ⟶ L₂} {a : K₁ ⟶ K₂} {b : L₁ ⟶ L₂}
  (H : Homotopy (CategoryTheory.CategoryStruct.comp φ₁ b) (CategoryTheory.CategoryStruct.comp a φ₂))
  {Z : CochainComplex C ℤ} (h : CochainComplex.mappingCone φ₂ ⟶ Z),
  CategoryTheory.CategoryStruct.comp (CochainComplex.mappingCone.inr φ₁)
      (CategoryTheory.CategoryStruct.comp (CochainComplex.mappingCone.mapOfHomotopy H) h) =
    CategoryTheory.CategoryStruct.comp b (CategoryTheory.CategoryStruct.comp (CochainComplex.mappingCone.inr φ₂) h)
-- Mathlib.Tactic.ComputeAsymptotics.Multiseries.Corecursion
Tactic.ComputeAsymptotics.Seq.dist_cons_cons : ∀ {α : Type u_1} (x : α) (s t : Stream'.Seq α), dist (Stream'.Seq.cons x s) (Stream'.Seq.cons x t) = 2⁻¹ * dist s t
-- Mathlib.NumberTheory.LSeries.Convolution
/-- We turn any function `ℕ → R` into an `ArithmeticFunction R` by setting its value at `0`
to be zero.  -/
toArithmeticFunction : {R : Type u_1} → [inst : Zero R] → (ℕ → R) → ArithmeticFunction R
-- Mathlib.Analysis.Complex.UpperHalfPlane.Topology
UpperHalfPlane.comp_ofComplex_of_im_pos : ∀ (f : UpperHalfPlane → ℂ) (z : ℂ) (hz : 0 < z.im), (f ∘ ↑UpperHalfPlane.ofComplex) z = f { coe := z, coe_im_pos := hz }
-- Mathlib.CategoryTheory.Limits.Shapes.WidePullbacks
_private.Mathlib.CategoryTheory.Limits.Shapes.WidePullbacks.0.CategoryTheory.Limits.WidePullbackShape.mkCone.match_1.eq_2 : ∀ {J : Type u_1} (motive : CategoryTheory.Limits.WidePullbackShape J → Sort u_2) (j : J) (h_1 : Unit → motive none)
  (h_2 : (j : J) → motive (some j)),
  (match some j with
    | none => h_1 ()
    | some j => h_2 j) =
    h_2 j
-- Mathlib.LinearAlgebra.LinearPMap
LinearPMap.ext_iff : ∀ {R : Type u_1} {S : Type u_2} [inst : Ring R] [inst_1 : Ring S] {σ : R →+* S} {E : Type u_4} [inst_2 : AddCommGroup E]
  [inst_3 : Module R E] {F : Type u_5} [inst_4 : AddCommGroup F] [inst_5 : Module S F] {f g : E →ₛₗ.[σ] F},
  f = g ↔ f.domain = g.domain ∧ ∀ ⦃x : E⦄ ⦃hf : x ∈ f.domain⦄ ⦃hg : x ∈ g.domain⦄, ↑f ⟨x, hf⟩ = ↑g ⟨x, hg⟩
-- Init.Internal.Order.MonadTail
Lean.Order.instMonadTailIO : Lean.Order.MonadTail IO