mathlib-initiative/mathlib-types huggingface dataset:
-- Batteries.Recycling.RBTree.WF
RBTree.RBNode.balLeft.match_1.congr_eq_3 : ∀ {α : Type u_1} (motive : RBTree.RBNode α → Sort u_2) (r : RBTree.RBNode α)
  (h_1 :
    (a : RBTree.RBNode α) → (y : α) → (b : RBTree.RBNode α) → motive (RBTree.RBNode.node RBTree.RBColor.black a y b))
  (h_2 :
    (a : RBTree.RBNode α) →
      (y : α) →
        (b : RBTree.RBNode α) →
          (z : α) →
            (c : RBTree.RBNode α) →
              motive (RBTree.RBNode.node RBTree.RBColor.red (RBTree.RBNode.node RBTree.RBColor.black a y b) z c))
  (h_3 : (r : RBTree.RBNode α) → motive r) (r_1 : RBTree.RBNode α),
  r = r_1 →
    (∀ (a : RBTree.RBNode α) (y : α) (b : RBTree.RBNode α),
        r_1 = RBTree.RBNode.node RBTree.RBColor.black a y b → False) →
      (∀ (a : RBTree.RBNode α) (y : α) (b : RBTree.RBNode α) (z : α) (c : RBTree.RBNode α),
          r_1 = RBTree.RBNode.node RBTree.RBColor.red (RBTree.RBNode.node RBTree.RBColor.black a y b) z c → False) →
        (match r with
          | RBTree.RBNode.node RBTree.RBColor.black a y b => h_1 a y b
          | RBTree.RBNode.node RBTree.RBColor.red (RBTree.RBNode.node RBTree.RBColor.black a y b) z c => h_2 a y b z c
          | r => h_3 r) ≍
          h_3 r_1
-- Mathlib.Analysis.Normed.Unbundled.SmoothingSeminorm
/-- If `μ 1 ≤ 1`, `μ` is nonarchimedean, and `∀ y : R, μ (x * y) = μ x * μ y`, then
`smoothingSeminorm μ x = μ x`.  -/
smoothingSeminorm_apply_of_map_mul_eq_mul : ∀ {R : Type u_1} [inst : CommRing R] (μ : RingSeminorm R) (hμ1 : μ 1 ≤ 1) (hna : IsNonarchimedean ⇑μ) {x : R},
  (∀ (y : R), μ (x * y) = μ x * μ y) → (smoothingSeminorm μ hμ1 hna) x = μ x
-- Mathlib.Topology.Order.OrderClosed
instFirstCountableTopologyOrderDual : ∀ {α : Type u} [inst : TopologicalSpace α] [h : FirstCountableTopology α], FirstCountableTopology αᵒᵈ
-- Mathlib.NumberTheory.NumberField.Completion.InfinitePlace
/-- Wrap an element of `v.1.Completion` into `v.Completion`.  -/
NumberField.InfinitePlace.Completion.ofCompletion : {K : Type u_1} → [inst : Field K] → {v : NumberField.InfinitePlace K} → (↑v).Completion → v.Completion
-- Mathlib.MeasureTheory.VectorMeasure.Integral
MeasureTheory.VectorMeasure.integral_congr_ae : ∀ {X : Type u_2} {E : Type u_4} {F : Type u_5} {G : Type u_6} {mX : MeasurableSpace X} [inst : NormedAddCommGroup E]
  [inst_1 : NormedSpace ℝ E] [inst_2 : NormedAddCommGroup F] [inst_3 : NormedSpace ℝ F] [inst_4 : NormedAddCommGroup G]
  [inst_5 : NormedSpace ℝ G] {f g : X → E} {μ : MeasureTheory.VectorMeasure X F} {B : E →L[ℝ] F →L[ℝ] G},
  f =ᵐ[μ.variation] g → ∫ᵛ (x : X), f x ∂[B; μ] = ∫ᵛ (x : X), g x ∂[B; μ]
-- Lean.Meta.Tactic.Generalize
/-- Extension of `generalize` to support generalizing within specified hypotheses.
The `hyps` array contains the list of hypotheses within which to look for occurrences
of the generalizing expressions.
 -/
Lean.MVarId.generalizeHyp : Lean.MVarId →
  Array Lean.Meta.GeneralizeArg →
    optParam (Array Lean.FVarId) #[] →
      optParam Lean.Meta.FVarSubst { } →
        optParam Lean.Meta.TransparencyMode Lean.Meta.TransparencyMode.instances →
          Lean.MetaM (Lean.Meta.FVarSubst × Array Lean.FVarId × Lean.MVarId)
-- Mathlib.AlgebraicGeometry.PullbackCarrier
AlgebraicGeometry.Scheme.Pullback.range_map : ∀ {X Y S : AlgebraicGeometry.Scheme} (f : X ⟶ S) (g : Y ⟶ S) {X' Y' S' : AlgebraicGeometry.Scheme} (f' : X' ⟶ S')
  (g' : Y' ⟶ S') (i₁ : X ⟶ X') (i₂ : Y ⟶ Y') (i₃ : S ⟶ S')
  (e₁ : CategoryTheory.CategoryStruct.comp f i₃ = CategoryTheory.CategoryStruct.comp i₁ f')
  (e₂ : CategoryTheory.CategoryStruct.comp g i₃ = CategoryTheory.CategoryStruct.comp i₂ g') [CategoryTheory.Mono i₃],
  Set.range ⇑(CategoryTheory.Limits.pullback.map f g f' g' i₁ i₂ i₃ e₁ e₂) =
    ⇑(CategoryTheory.Limits.pullback.fst f' g') ⁻¹' Set.range ⇑i₁ ∩
      ⇑(CategoryTheory.Limits.pullback.snd f' g') ⁻¹' Set.range ⇑i₂
-- Init.System.IO
/-- Returns the contents of the indicated directory. Throws an exception if the file does not exist or
is not a directory.
 -/
System.FilePath.readDir : System.FilePath → IO (Array IO.FS.DirEntry)
-- Mathlib.RingTheory.HahnSeries.PowerSeries
HahnSeries.toMvPowerSeries_apply : ∀ {R : Type u_2} [inst : Semiring R] {σ : Type u_3} [inst_1 : Finite σ] (f : HahnSeries (σ →₀ ℕ) R) (a : σ →₀ ℕ),
  HahnSeries.toMvPowerSeries f a = f.coeff a
-- Mathlib.MeasureTheory.Measure.MeasureSpaceDef
MeasureTheory.measure_biUnion_ne_top : ∀ {α : Type u_1} {β : Type u_2} [inst : MeasurableSpace α] {μ : MeasureTheory.Measure α} {s : Set β} {f : β → Set α},
  s.Finite → (∀ i ∈ s, μ (f i) ≠ ⊤) → μ (⋃ i ∈ s, f i) ≠ ⊤
-- Std.Data.TreeSet.Lemmas
Std.TreeSet.min?_insert_le_min? : ∀ {α : Type u} {cmp : α → α → Ordering} {t : Std.TreeSet α cmp} [inst : Std.TransCmp cmp] {k km kmi : α},
  t.min? = some km → (t.insert k).min?.get ⋯ = kmi → (cmp kmi km).isLE = true
-- Mathlib.RingTheory.Valuation.Quotient
/-- The quotient valuation on `R / J` has support `(supp v) / J` if `J ⊆ supp v`.  -/
AddValuation.supp_quot : ∀ {R : Type u_1} {Γ₀ : Type u_2} [inst : CommRing R] [inst_1 : LinearOrderedAddCommMonoidWithTop Γ₀]
  (v : AddValuation R Γ₀) {J : Ideal R} (hJ : J ≤ v.supp), (v.onQuot hJ).supp = Ideal.map (Ideal.Quotient.mk J) v.supp
-- Std.Data.String.ToNat
String.isNat_comp_toSlice : String.Slice.isNat ∘ String.toSlice = String.isNat
-- Mathlib.Order.Filter.AtTopBot.Defs
IsBot.atBot_eq : ∀ {α : Type u_3} [inst : Preorder α] {a : α}, IsBot a → Filter.atBot = Filter.principal (Set.Iic a)
-- Mathlib.Geometry.Manifold.Diffeomorph
ContinuousLinearEquiv.symm_toDiffeomorph : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {E' : Type u_3} [inst_3 : NormedAddCommGroup E'] [inst_4 : NormedSpace 𝕜 E']
  (e : E ≃L[𝕜] E'), e.symm.toDiffeomorph = e.toDiffeomorph.symm
-- Mathlib.Algebra.BigOperators.Fin
Fin.prod_Ioo_castLE : ∀ {M : Type u_2} [inst : CommMonoid M] {n m : ℕ} (h : n ≤ m) (f : Fin m → M) (a b : Fin n),
  ∏ i ∈ Finset.Ioo (Fin.castLE h a) (Fin.castLE h b), f i = ∏ i ∈ Finset.Ioo a b, f (Fin.castLE h i)
-- Mathlib.CategoryTheory.Monoidal.Mod
/-- If `C` acts monoidally on `D`, then every object of `D` is canonically a
module over the trivial monoid.  -/
CategoryTheory.ModObj.instTensorUnit : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    [inst_1 : CategoryTheory.MonoidalCategory C] →
      {D : Type u₂} →
        [inst_2 : CategoryTheory.Category.{v₂, u₂} D] →
          [inst_3 : CategoryTheory.MonoidalCategory.MonoidalLeftAction C D] →
            (X : D) → CategoryTheory.ModObj (CategoryTheory.MonoidalCategoryStruct.tensorUnit C) X
-- Mathlib.FieldTheory.IntermediateField.Adjoin.Defs
/-- Adjoining is idempotent: adjoining an adjoin is the same as a single adjoin.  -/
IntermediateField.adjoin_adjoin_right : ∀ (F : Type u_1) [inst : Field F] {E : Type u_2} [inst_1 : Field E] [inst_2 : Algebra F E] (S : Set E) {K : Type u_3}
  [inst_3 : Field K] [inst_4 : Algebra K F] [inst_5 : Algebra K E] [IsScalarTower K F E],
  IntermediateField.adjoin F ↑(IntermediateField.adjoin K S) = IntermediateField.adjoin F S
-- Mathlib.Topology.Algebra.Ring.Basic
ContinuousAddEquiv.mulRight_apply : ∀ {R : Type u_1} [inst : TopologicalSpace R] [inst_1 : Semiring R] [inst_2 : IsTopologicalSemiring R] (r : Rˣ) (x : R),
  (ContinuousAddEquiv.mulRight r) x = x * ↑r
-- Mathlib.Data.DFinsupp.NeLocus
DFinsupp.neLocus_neg_neg : ∀ {α : Type u_1} {N : α → Type u_2} [inst : DecidableEq α] [inst_1 : (a : α) → DecidableEq (N a)]
  [inst_2 : (a : α) → AddGroup (N a)] (f g : Π₀ (a : α), N a), (-f).neLocus (-g) = f.neLocus g
-- Mathlib.Algebra.MonoidAlgebra.Defs
/-- **Alias** of `MonoidAlgebra.coeff_mul_antidiag`. -/
MonoidAlgebra.mul_apply_antidiagonal : ∀ {R : Type u_1} {M : Type u_4} [inst : Semiring R] [inst_1 : Mul M] (x y : MonoidAlgebra R M) (m : M)
  (s : Finset (M × M)), (∀ {p : M × M}, p ∈ s ↔ p.1 * p.2 = m) → (x * y).coeff m = ∑ p ∈ s, x.coeff p.1 * y.coeff p.2
-- Std.Data.DTreeMap.Internal.Model
Std.DTreeMap.Internal.Impl.Const.getEntryLT?.go.eq_1 : ∀ {α : Type u} {β : Type v} [inst : Ord α] (k : α) (best : Option (α × β)),
  Std.DTreeMap.Internal.Impl.Const.getEntryLT?.go k best Std.DTreeMap.Internal.Impl.leaf = best
-- Mathlib.LinearAlgebra.Finsupp.Supported
Finsupp.range_restrictDom : ∀ {α : Type u_1} {M : Type u_2} {R : Type u_5} [inst : Semiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M]
  (s : Set α) [inst_3 : DecidablePred fun x => x ∈ s], (Finsupp.restrictDom M R s).range = ⊤
-- Init.Data.Nat.Basic
Nat.le_antisymm_iff : ∀ {a b : ℕ}, a = b ↔ a ≤ b ∧ b ≤ a
-- Mathlib.RingTheory.AlgebraicIndependent.Basic
algebraicIndependent_empty_iff : ∀ (R : Type u_2) (A : Type v) [inst : CommRing R] [inst_1 : CommRing A] [inst_2 : Algebra R A],
  AlgebraicIndependent R Subtype.val ↔ Function.Injective ⇑(algebraMap R A)
-- Mathlib.Analysis.InnerProductSpace.Spectrum
LinearMap.IsSymmetric.diagonalization.congr_simp : ∀ {𝕜 : Type u_1} [inst : RCLike 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E] [inst_2 : InnerProductSpace 𝕜 E]
  {T : E →ₗ[𝕜] E} [inst_3 : FiniteDimensional 𝕜 E] (hT : T.IsSymmetric), hT.diagonalization = hT.diagonalization
-- Init.Data.Iterators.PostconditionMonad
Std.Iterators.PostconditionT.pure.eq_1 : ∀ {m : Type w → Type w'} [inst : Pure m] {α : Type w} (a : α),
  Std.Iterators.PostconditionT.pure a = { Property := fun y => a = y, operation := pure ⟨a, ⋯⟩ }
-- Mathlib.Data.SubtypeNeLift
Function.subtypeNeLift_restriction : ∀ {ι : Type u_1} [inst : DecidableEq ι] {M : ι → Type u_2} (φ : (i : ι) → M i) (i₀ : ι),
  Function.subtypeNeLift i₀ (fun i => φ ↑i) (φ i₀) = φ
-- Mathlib.Data.Matrix.Block
Matrix.map_toSquareBlock : ∀ {m : Type u_2} {α : Type u_15} {β : Type u_16} (f : α → β) {M : Matrix m m α} {ι : Type u_18} {b : m → ι} {i : ι},
  (M.map f).toSquareBlock b i = (M.toSquareBlock b i).map f
-- Mathlib.Data.Multiset.Filter
Multiset.filter_comm : ∀ {α : Type u_1} (p : α → Prop) [inst : DecidablePred p] (q : α → Prop) [inst_1 : DecidablePred q] (s : Multiset α),
  Multiset.filter p (Multiset.filter q s) = Multiset.filter q (Multiset.filter p s)
-- Mathlib.MeasureTheory.Constructions.Pi
MeasureTheory.Measure.pi.sigmaFinite : ∀ {ι : Type u_1} {α : ι → Type u_3} [inst : Fintype ι] [inst_1 : (i : ι) → MeasurableSpace (α i)]
  (μ : (i : ι) → MeasureTheory.Measure (α i)) [∀ (i : ι), MeasureTheory.SigmaFinite (μ i)],
  MeasureTheory.SigmaFinite (MeasureTheory.Measure.pi μ)
-- Mathlib.GroupTheory.OrderOfElement
IsOfFinAddOrder.mem_multiples_iff_mem_zmultiples : ∀ {G : Type u_1} [inst : AddGroup G] {x y : G},
  IsOfFinAddOrder x → (y ∈ AddSubmonoid.multiples x ↔ y ∈ AddSubgroup.zmultiples x)
-- Lean.Data.Lsp.InitShutdown
Lean.Lsp.instToJsonInitializedParams : Lean.ToJson Lean.Lsp.InitializedParams
-- Mathlib.Analysis.BoxIntegral.Basic
BoxIntegral.Integrable.of_neg : ∀ {ι : Type u} {E : Type v} {F : Type w} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E]
  [inst_2 : NormedAddCommGroup F] [inst_3 : NormedSpace ℝ F] {I : BoxIntegral.Box ι} [inst_4 : Fintype ι]
  {l : BoxIntegral.IntegrationParams} {f : (ι → ℝ) → E} {vol : BoxIntegral.BoxAdditiveMap ι (E →L[ℝ] F) ⊤},
  BoxIntegral.Integrable I l (-f) vol → BoxIntegral.Integrable I l f vol
-- Mathlib.Algebra.Polynomial.UnitTrinomial
Polynomial.trinomial_leadingCoeff : ∀ {R : Type u_1} [inst : Semiring R] {k m n : ℕ} {u v w : R},
  k < m → m < n → w ≠ 0 → (Polynomial.trinomial k m n u v w).leadingCoeff = w
-- Mathlib.InformationTheory.Hamming
/-- Corresponds to `dist_pos`.  -/
hammingDist_pos : ∀ {ι : Type u_2} {β : ι → Type u_3} [inst : Fintype ι] [inst_1 : (i : ι) → DecidableEq (β i)] {x y : (i : ι) → β i},
  0 < hammingDist x y ↔ x ≠ y
-- Mathlib.CategoryTheory.Bicategory.Grothendieck
CategoryTheory.Pseudofunctor.CoGrothendieck.categoryStruct : {𝒮 : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} 𝒮] →
    {F : CategoryTheory.Pseudofunctor (CategoryTheory.LocallyDiscrete 𝒮ᵒᵖ) CategoryTheory.Cat} →
      CategoryTheory.CategoryStruct.{max v₂ v₁, max u₂ u₁} F.CoGrothendieck
-- Mathlib.NumberTheory.RamificationInertia.Basic
Ideal.quotientToQuotientRangePowQuotSucc_injective : ∀ {R : Type u} [inst : CommRing R] {S : Type v} [inst_1 : CommRing S] [inst_2 : Algebra R S] (p : Ideal R) (P : Ideal S)
  [hfp : NeZero (p.ramificationIdx' P)] [IsDedekindDomain S] [P.IsPrime] {i : ℕ},
  i < p.ramificationIdx' P →
    ∀ {a : S} (a_mem : a ∈ P ^ i), a ∉ P ^ (i + 1) → Function.Injective ⇑(p.quotientToQuotientRangePowQuotSucc P a_mem)
-- Mathlib.Algebra.Order.Floor.Ring
Int.natCast_floor_eq_floor : ∀ {R : Type u_2} [inst : Ring R] [inst_1 : LinearOrder R] [inst_2 : FloorRing R] {a : R}, 0 ≤ a → ↑⌊a⌋₊ = ⌊a⌋
-- Mathlib.CategoryTheory.Limits.Shapes.BinaryProducts
CategoryTheory.Limits.prodComparison.eq_1 : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{w, u₂} D]
  (F : CategoryTheory.Functor C D) (A B : C) [inst_2 : CategoryTheory.Limits.HasBinaryProduct A B]
  [inst_3 : CategoryTheory.Limits.HasBinaryProduct (F.obj A) (F.obj B)],
  CategoryTheory.Limits.prodComparison F A B =
    CategoryTheory.Limits.prod.lift (F.map CategoryTheory.Limits.prod.fst) (F.map CategoryTheory.Limits.prod.snd)
-- Lean.Elab.App
Lean.Elab.Term.ElabAppArgs.Context.mk.inj : ∀ {ellipsis explicit resultIsOutParamSupport : Bool} {numImplicitParams : ℕ}
  {ellipsis_1 explicit_1 resultIsOutParamSupport_1 : Bool} {numImplicitParams_1 : ℕ},
  { ellipsis := ellipsis, explicit := explicit, resultIsOutParamSupport := resultIsOutParamSupport,
        numImplicitParams := numImplicitParams } =
      { ellipsis := ellipsis_1, explicit := explicit_1, resultIsOutParamSupport := resultIsOutParamSupport_1,
        numImplicitParams := numImplicitParams_1 } →
    ellipsis = ellipsis_1 ∧
      explicit = explicit_1 ∧
        resultIsOutParamSupport = resultIsOutParamSupport_1 ∧ numImplicitParams = numImplicitParams_1
-- Mathlib.Algebra.Category.ModuleCat.Sheaf.LocallyFree
SheafOfModules.LocalGeneratorsData.IsLocallyFreeData.isIso : ∀ {C : Type u₁} {inst : CategoryTheory.Category.{v₁, u₁} C} {J : CategoryTheory.GrothendieckTopology C}
  {R : CategoryTheory.Sheaf J RingCat} {inst_1 : ∀ (X : C), CategoryTheory.HasWeakSheafify (J.over X) AddCommGrpCat}
  {inst_2 : ∀ (X : C), (J.over X).WEqualsLocallyBijective AddCommGrpCat} {M : SheafOfModules R}
  {q : M.LocalGeneratorsData} [self : q.IsLocallyFreeData] (i : q.I), CategoryTheory.IsIso (q.generators i).π
-- Mathlib.CategoryTheory.Monoidal.Mon
CategoryTheory.AddMon.EquivLaxMonoidalFunctorPUnit.addMonToLaxMonoidalObj_map : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.MonoidalCategory C]
  (A : CategoryTheory.AddMon C) {X Y : CategoryTheory.Discrete PUnit.{w + 1}} (x : X ⟶ Y),
  (CategoryTheory.AddMon.EquivLaxMonoidalFunctorPUnit.addMonToLaxMonoidalObj A).map x =
    CategoryTheory.CategoryStruct.id A.X
-- Std.Data.DHashMap.Lemmas
Std.DHashMap.Equiv.get?_eq : ∀ {α : Type u} {β : α → Type v} {x : BEq α} {x_1 : Hashable α} {m₁ m₂ : Std.DHashMap α β} [inst : LawfulBEq α] {k : α},
  m₁.Equiv m₂ → m₁.get? k = m₂.get? k
-- Mathlib.Topology.MetricSpace.Thickening
/-- The frontier of the (open) thickening of a set is contained in an `Metric.infEDist` level
set.  -/
Metric.frontier_thickening_subset : ∀ {α : Type u} [inst : PseudoEMetricSpace α] (E : Set α) {δ : ℝ},
  frontier (Metric.thickening δ E) ⊆ {x | Metric.infEDist x E = ENNReal.ofReal δ}
-- Lean.Server.Completion.SyntheticCompletion
_private.Lean.Server.Completion.SyntheticCompletion.0.Lean.Server.Completion.findBest? : {α : Type} →
  Lean.Elab.InfoTree →
    (α → α → Bool) →
      (Lean.Elab.ContextInfo → Lean.Elab.Info → Lean.PersistentArray Lean.Elab.InfoTree → Option α) → Option α
-- Mathlib.Order.CompleteLattice.Finset
Finset.set_biUnion_singleton : ∀ {α : Type u_2} {β : Type u_3} (a : α) (s : α → Set β), ⋃ x ∈ {a}, s x = s a
-- Mathlib.RingTheory.Perfection
Perfection.pthRootMonoidHom_eq_pthRoot : ∀ {R : Type u_1} [inst : CommSemiring R] {p : ℕ} [hp : Fact (Nat.Prime p)] [inst_1 : CharP R p],
  ⇑(Perfection.pthRootMonoidHom R p) = ⇑(Perfection.pthRoot R p)
-- Mathlib.Order.GaloisConnection.Defs
GaloisCoinsertion.u_surjective : ∀ {α : Type u} {β : Type v} {u : α → β} {l : β → α} [inst : Preorder α] [inst_1 : PartialOrder β]
  (gi : GaloisCoinsertion l u), Function.Surjective u
-- Mathlib.Algebra.Homology.CommSq
CategoryTheory.CommSq.shortComplex'_X₃ : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Preadditive C] {X₁ X₂ X₃ X₄ : C}
  [inst_2 : CategoryTheory.Limits.HasBinaryBiproduct X₂ X₃] {fst : X₁ ⟶ X₂} {snd : X₁ ⟶ X₃} {f : X₂ ⟶ X₄} {g : X₃ ⟶ X₄}
  (sq : CategoryTheory.CommSq fst snd f g), sq.shortComplex'.X₃ = X₄
-- Mathlib.Condensed.Discrete.Basic
LightCondensed.underlying_obj : ∀ (C : Type w) [inst : CategoryTheory.Category.{u, w} C]
  (j : CategoryTheory.Sheaf (CategoryTheory.coherentTopology LightProfinite) C),
  (LightCondensed.underlying C).obj j = j.obj.obj (Opposite.op (LightProfinite.of PUnit.{u + 1}))
-- Mathlib.Algebra.Homology.Additive
HomologicalComplex.instNegHom : {ι : Type u_1} →
  {V : Type u} →
    [inst : CategoryTheory.Category.{v, u} V] →
      [inst_1 : CategoryTheory.Preadditive V] → {c : ComplexShape ι} → {C D : HomologicalComplex V c} → Neg (C ⟶ D)
-- Mathlib.Algebra.Polynomial.EraseLead
Polynomial.two_le_natDegree_of_nextCoeff_eraseLead : ∀ {R : Type u_1} [inst : Semiring R] {f : Polynomial R}, f.eraseLead ≠ 0 → f.nextCoeff = 0 → 2 ≤ f.natDegree
-- Mathlib.Data.Set.Basic
Set.mem_ite_univ_left : ∀ {α : Type u} (p : Prop) [inst : Decidable p] (t : Set α) (x : α), (x ∈ if p then Set.univ else t) ↔ ¬p → x ∈ t
-- Lean.Elab.PreDefinition.TerminationHint
/-- A single `partial_fixpoint`, `inductive_fixpoint` or `coinductive_fixpoint` clause  -/
Lean.Elab.PartialFixpoint : Type
-- Mathlib.Algebra.Lie.CartanExists
LieAlgebra.exists_isCartanSubalgebra_engel : ∀ (K : Type u_1) (L : Type u_2) [inst : Field K] [inst_1 : LieRing L] [inst_2 : LieAlgebra K L] [Module.Finite K L]
  [Infinite K], ∃ x, (LieSubalgebra.engel K x).IsCartanSubalgebra
-- Mathlib.MeasureTheory.Constructions.BorelSpace.Real
/-- The set of finite `EReal` numbers is `MeasurableEquiv` to `ℝ`.  -/
MeasurableEquiv.erealEquivReal : ↑{⊥, ⊤}ᶜ ≃ᵐ ℝ
-- Std.Data.ExtTreeMap.Lemmas
Std.ExtTreeMap.minKey?_insert_of_isEmpty : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Std.ExtTreeMap α β cmp} [inst : Std.TransCmp cmp] {k : α}
  {v : β}, t.isEmpty = true → (t.insert k v).minKey? = some k
-- Mathlib.Topology.Constructions
Continuous.matrixVecCons : ∀ {X : Type u} {Z : Type u_1} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Z] {n : ℕ} {f : X → Z}
  {g : X → Fin n → Z}, Continuous f → Continuous g → Continuous fun a => Matrix.vecCons (f a) (g a)
-- Mathlib.RingTheory.Spectrum.Prime.ChevalleyComplexity
/-- The bound on the number of polynomials used to describe the constructible set appearing in
Chevalley's theorem with complexity bound.  -/
ChevalleyThm.numBound : ℕ → (m : ℕ) → ℕ → Multiset (Fin m) → ℕ
-- Mathlib.Topology.Algebra.Monoid
continuousOn_multiset_sum : ∀ {ι : Type u_1} {M : Type u_3} {X : Type u_5} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace M]
  [inst_2 : AddCommMonoid M] [ContinuousAdd M] {f : ι → X → M} (s : Multiset ι) {t : Set X},
  (∀ i ∈ s, ContinuousOn (f i) t) → ContinuousOn (fun a => (Multiset.map (fun i => f i a) s).sum) t
-- Mathlib.Order.Types.Arithmetic
OrderType.instZeroLEOneClass : ZeroLEOneClass OrderType.{u_1}
-- Lean.Meta.Tactic.Simp.BuiltinSimprocs.Int
Int.reduceGT : Lean.Meta.Simp.Simproc
-- Mathlib.FieldTheory.Fixed
FixedPoints.minpoly.eq_1 : ∀ (G : Type u) [inst : Group G] (F : Type v) [inst_1 : Field F] [inst_2 : MulSemiringAction G F] [inst_3 : Fintype G]
  (x : F), FixedPoints.minpoly G F x = (prodXSubSMul G F x).toSubring (FixedPoints.subfield G F).toSubring ⋯
-- Mathlib.RingTheory.Polynomial.Nilpotent
/-- Let `P` be a polynomial over `R`. If `P` is a unit, then all its coefficients are nilpotent,
except its constant term which is a unit.

See also `Polynomial.isUnit_iff_coeff_isUnit_isNilpotent`.  -/
Polynomial.coeff_isUnit_isNilpotent_of_isUnit : ∀ {R : Type u_1} [inst : CommRing R] {P : Polynomial R},
  IsUnit P → IsUnit (P.coeff 0) ∧ ∀ (i : ℕ), i ≠ 0 → IsNilpotent (P.coeff i)
-- Mathlib.Algebra.Lie.Loop
LieAlgebra.LoopAlgebra.twoCocycleOfBilinear_coe : ∀ (R : Type u_1) (A : Type u_2) (L : Type u_3) [inst : CommRing R] [inst_1 : LieRing L] [inst_2 : LieAlgebra R L]
  [inst_3 : CommRing A] [inst_4 : IsAddTorsionFree R] [inst_5 : Algebra A R] (Φ : LinearMap.BilinForm R L)
  (hΦ : LinearMap.BilinForm.lieInvariant L Φ) (hΦs : Φ.IsSymm),
  ↑(LieAlgebra.LoopAlgebra.twoCocycleOfBilinear R A L Φ hΦ hΦs) =
    LieAlgebra.LoopAlgebra.twoCochainOfBilinear R A L Φ hΦs
-- Mathlib.Data.Finsupp.Defs
Finsupp.equivFunOnFinite_symm_apply_support : ∀ {α : Type u_1} {M : Type u_4} [inst : Zero M] [inst_1 : Finite α] (f : α → M),
  (Finsupp.equivFunOnFinite.symm f).support = ⋯.toFinset
-- Mathlib.CategoryTheory.Shift.CommShiftTwo
/-- A bifunctor `G : C₁ ⥤ C₂ ⥤ D` commutes with the shifts by `M` if all functors
`G.obj X₁` and `G.flip X₂` are equipped with `Functor.CommShift` structures, in a way
that is natural in `X₁` and `X₂`, and that these isomorphisms commute up to
the multiplication with an element in `(CatCenter D)ˣ` which is determined by
a `CommShift₂Setup D M` structure. (In most cases, one should use the
abbreviation `CommShift₂Int`.)  -/
CategoryTheory.Functor.CommShift₂ : {C₁ : Type u_1} →
  {C₂ : Type u_3} →
    {D : Type u_5} →
      [inst : CategoryTheory.Category.{v_1, u_1} C₁] →
        [inst_1 : CategoryTheory.Category.{v_3, u_3} C₂] →
          [inst_2 : CategoryTheory.Category.{v_5, u_5} D] →
            {M : Type u_6} →
              [inst_3 : AddCommMonoid M] →
                [CategoryTheory.HasShift C₁ M] →
                  [CategoryTheory.HasShift C₂ M] →
                    [inst_6 : CategoryTheory.HasShift D M] →
                      CategoryTheory.Functor C₁ (CategoryTheory.Functor C₂ D) →
                        CategoryTheory.CommShift₂Setup D M → Type (max (max (max u_1 u_3) u_6) v_5)
-- Mathlib.Analysis.SpecialFunctions.Complex.Arg
Complex.arg_eq_zero_iff_zero_le : ∀ {z : ℂ}, z.arg = 0 ↔ 0 ≤ z
-- Mathlib.Order.SuccPred.Basic
/-- There is at most one way to define the successors in a `PartialOrder`.  -/
Order.instSubsingletonSuccOrder : ∀ {α : Type u_1} [inst : PartialOrder α], Subsingleton (SuccOrder α)
-- Mathlib.Analysis.Calculus.FDeriv.Mul
/-- **Alias** of `fderivWithin_finsetProd`. -/
fderivWithin_finset_prod : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {s : Set E} {ι : Type u_5} {𝔸' : Type u_7} [inst_3 : NormedCommRing 𝔸']
  [inst_4 : NormedAlgebra 𝕜 𝔸'] {u : Finset ι} {g : ι → E → 𝔸'} [inst_5 : DecidableEq ι] {x : E},
  UniqueDiffWithinAt 𝕜 s x →
    (∀ i ∈ u, DifferentiableWithinAt 𝕜 (g i) s x) →
      fderivWithin 𝕜 (fun x => ∏ i ∈ u, g i x) s x = ∑ i ∈ u, (∏ j ∈ u.erase i, g j x) • fderivWithin 𝕜 (g i) s x
-- Mathlib.Analysis.Normed.Operator.BoundedLinearMaps
/-- The function `ContinuousLinearMap.smulRight`, associating to a continuous linear map
`f : E → 𝕜` and a scalar `c : F` the tensor product `f ⊗ c` as a continuous linear map from `E` to
`F`, is a bounded bilinear map.  -/
isBoundedBilinearMap_smulRight : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : SeminormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {F : Type u_3} [inst_3 : SeminormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F],
  IsBoundedBilinearMap 𝕜 fun p => p.1.smulRight p.2
-- Mathlib.Analysis.SpecialFunctions.Pow.Continuity
ContinuousAt.const_cpow : ∀ {α : Type u_1} [inst : TopologicalSpace α] {f : α → ℂ} {a : α} {b : ℂ},
  ContinuousAt f a → b ≠ 0 ∨ f a ≠ 0 → ContinuousAt (fun x => b ^ f x) a
-- Std.Sat.CNF.Dimacs
_private.Std.Sat.CNF.Dimacs.0.Std.Sat.CNF.DimacsM : Type → Type
-- Mathlib.Algebra.Lie.Sl2
IsSl2Triple.h_ne_zero : ∀ {L : Type u_2} [inst : LieRing L] {h e f : L}, IsSl2Triple h e f → h ≠ 0