mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Topology.Algebra.Support
hasCompactSupport_def : ∀ {α : Type u_2} {β : Type u_4} [inst : TopologicalSpace α] [inst_1 : Zero β] {f : α → β},
  HasCompactSupport f ↔ IsCompact (closure (Function.support f))
-- Lean.DocString.Parser
Lean.Doc.Parser.instDecidableEqUnorderedListType : DecidableEq Lean.Doc.Parser.UnorderedListType
-- Init.Prelude
/-- Marker for information that has been erased by the code generator.  -/
lcErased : Type
-- Mathlib.Algebra.Category.Ring.Basic
/-- The type of morphisms in `CommRingCat`.  -/
CommRingCat.Hom : CommRingCat → CommRingCat → Type u
-- Mathlib.CategoryTheory.Bicategory.Basic
CategoryTheory.Bicategory.whiskerRight_id_assoc : ∀ {B : Type u} [self : CategoryTheory.Bicategory B] {a b : B} {f g : a ⟶ b} (η : f ⟶ g) {Z : a ⟶ b}
  (h : CategoryTheory.CategoryStruct.comp g (CategoryTheory.CategoryStruct.id b) ⟶ Z),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.whiskerRight η (CategoryTheory.CategoryStruct.id b)) h =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.rightUnitor f).hom
      (CategoryTheory.CategoryStruct.comp η
        (CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.rightUnitor g).inv h))
-- Init.Data.Fin.Lemmas
Fin.cast_natAdd_zero : ∀ {n n' : ℕ} (i : Fin n) (h : 0 + n = n'), Fin.cast h (Fin.natAdd 0 i) = Fin.cast ⋯ i
-- Mathlib.Algebra.Free
FreeAddSemigroup.add_bind : ∀ {α β : Type u} (f : α → FreeAddSemigroup β) (x y : FreeAddSemigroup α), x + y >>= f = (x >>= f) + (y >>= f)
-- Mathlib.CategoryTheory.FiberedCategory.HasFibers
/-- Given a fibered category p, b' b in Fib R, and a pullback ψ : b ⟶ a in 𝒳, i.e.
```
b'       b --ψ--> a
|        |        |
v        v        v
R ====== R --f--> S
```
Then the induced map τ : b' ⟶ b can be lifted to the fiber over R  -/
HasFibers.inducedMap : {𝒮 : Type u₁} →
  {𝒳 : Type u₂} →
    [inst : CategoryTheory.Category.{v₁, u₁} 𝒮] →
      [inst_1 : CategoryTheory.Category.{v₂, u₂} 𝒳] →
        {p : CategoryTheory.Functor 𝒳 𝒮} →
          [inst_2 : HasFibers p] →
            {R S : 𝒮} →
              {a : 𝒳} →
                {b b' : HasFibers.Fib p R} →
                  (f : R ⟶ S) →
                    (ψ : (HasFibers.ι R).obj b' ⟶ a) →
                      [p.IsCartesian f ψ] → (φ : (HasFibers.ι R).obj b ⟶ a) → [p.IsHomLift f φ] → b ⟶ b'
-- Init.Data.Iterators.Consumers.Loop
/-- Returns the first non-`none` result of applying the monadic function `f` to each output
of the iterator, in order. Returns `none` if `f` returns `none` for all outputs.

`O(|it|)`. Short-circuits when `f` returns `some _`. The outputs of `it` are
examined in order of iteration.

If the iterator is not finite, this function might run forever. The variant
`it.ensureTermination.findSomeM?` always terminates after finitely many steps.

Example:
```lean example
#eval [7, 6, 5, 8, 1, 2, 6].iter.findSomeM? fun i => do
  if i < 5 then
    return some (i * 10)
  if i ≤ 6 then
    IO.println s!"Almost! {i}"
  return none
```
```output
Almost! 6
Almost! 5
```
```output
some 10
```
 -/
Std.Iter.findSomeM? : {α β : Type w} →
  {γ : Type x} →
    {m : Type x → Type w'} →
      [Monad m] →
        [inst : Std.Iterator α Id β] → [Std.IteratorLoop α Id m] → Std.Iter β → (β → m (Option γ)) → m (Option γ)
-- Mathlib.Geometry.Euclidean.Incenter
Affine.Simplex.excenterWeightsUnnorm_compl : ∀ {V : Type u_1} {P : Type u_2} [inst : NormedAddCommGroup V] [inst_1 : InnerProductSpace ℝ V] [inst_2 : MetricSpace P]
  [inst_3 : NormedAddTorsor V P] {n : ℕ} [inst_4 : NeZero n] (s : Affine.Simplex ℝ P n) (signs : Finset (Fin (n + 1))),
  s.excenterWeightsUnnorm signsᶜ = -s.excenterWeightsUnnorm signs
-- Aesop.Rule.Name
_private.Aesop.Rule.Name.0.Aesop.RuleName.Json.mk.injEq : ∀ (name : Lean.Name) (builder : Aesop.BuilderName) (phase : Aesop.PhaseName) (scope : Aesop.ScopeName)
  (rendered : String) (name_1 : Lean.Name) (builder_1 : Aesop.BuilderName) (phase_1 : Aesop.PhaseName)
  (scope_1 : Aesop.ScopeName) (rendered_1 : String),
  ({ name := name, builder := builder, phase := phase, scope := scope, rendered := rendered } =
      { name := name_1, builder := builder_1, phase := phase_1, scope := scope_1, rendered := rendered_1 }) =
    (name = name_1 ∧ builder = builder_1 ∧ phase = phase_1 ∧ scope = scope_1 ∧ rendered = rendered_1)
-- Mathlib.CategoryTheory.Abelian.Preradical.Colon
/-- The second projection of the pullback defining the colon preradical.  -/
CategoryTheory.Abelian.Preradical.colonπ : {C : Type u_1} →
  [inst : CategoryTheory.Category.{u_2, u_1} C] →
    [inst_1 : CategoryTheory.Abelian C] →
      (Φ Ψ : CategoryTheory.Abelian.Preradical C) → (Φ.colon Ψ).r ⟶ Φ.quotient.comp Ψ.r
-- Lean.Data.Lsp.Workspace
Lean.Lsp.WorkspaceFolder.mk : Lean.Lsp.DocumentUri → String → Lean.Lsp.WorkspaceFolder
-- Mathlib.Algebra.Order.Field.Subfield
/-- A subfield of an ordered field is an ordered field.  -/
Subfield.toIsStrictOrderedRing : ∀ {K : Type u_1} [inst : Field K] [inst_1 : LinearOrder K] [IsStrictOrderedRing K] (s : Subfield K),
  IsStrictOrderedRing ↥s
-- Mathlib.Topology.VectorBundle.ContinuousAlternatingMap
Bundle.Pretrivialization.continuousAlternatingMap_symm_apply : ∀ {𝕜 : Type u_1} {ι : Type u_2} [inst : NontriviallyNormedField 𝕜] {B : Type u_3} [inst_1 : TopologicalSpace B]
  {F₁ : Type u_4} [inst_2 : NormedAddCommGroup F₁] [inst_3 : NormedSpace 𝕜 F₁] {E₁ : B → Type u_5}
  [inst_4 : (x : B) → AddCommGroup (E₁ x)] [inst_5 : (x : B) → Module 𝕜 (E₁ x)]
  [inst_6 : TopologicalSpace (Bundle.TotalSpace F₁ E₁)] {F₂ : Type u_6} [inst_7 : NormedAddCommGroup F₂]
  [inst_8 : NormedSpace 𝕜 F₂] {E₂ : B → Type u_7} [inst_9 : (x : B) → AddCommGroup (E₂ x)]
  [inst_10 : (x : B) → Module 𝕜 (E₂ x)] [inst_11 : TopologicalSpace (Bundle.TotalSpace F₂ E₂)]
  [inst_12 : (x : B) → TopologicalSpace (E₁ x)] [inst_13 : FiberBundle F₁ E₁]
  [inst_14 : (x : B) → TopologicalSpace (E₂ x)] [inst_15 : FiberBundle F₂ E₂]
  {e₁ : Bundle.Trivialization F₁ Bundle.TotalSpace.proj} {e₂ : Bundle.Trivialization F₂ Bundle.TotalSpace.proj}
  [inst_16 : Bundle.Trivialization.IsLinear 𝕜 e₁] [inst_17 : Bundle.Trivialization.IsLinear 𝕜 e₂]
  (p : B × F₁ [⋀^ι]→L[𝕜] F₂),
  ↑(Bundle.Pretrivialization.continuousAlternatingMap 𝕜 ι e₁ e₂).symm p =
    ⟨p.1,
      (Bundle.Trivialization.symmL 𝕜 e₂ p.1).compContinuousAlternatingMap
        (p.2.compContinuousLinearMap (Bundle.Trivialization.continuousLinearMapAt 𝕜 e₁ p.1))⟩
-- Mathlib.LinearAlgebra.Matrix.DotProduct
Matrix.mul_conjTranspose_mul_self_eq_zero : ∀ {m : Type u_1} {n : Type u_2} {R : Type u_4} [inst : Fintype m] [inst_1 : Fintype n] [inst_2 : PartialOrder R]
  [inst_3 : NonUnitalRing R] [inst_4 : StarRing R] [StarOrderedRing R] [NoZeroDivisors R] {p : Type u_5}
  (A : Matrix m n R) (B : Matrix p n R), B * (A.conjTranspose * A) = 0 ↔ B * A.conjTranspose = 0
-- Mathlib.Algebra.BigOperators.Group.Finset.Basic
Finset.prod_finset_coe : ∀ {ι : Type u_1} {M : Type u_4} [inst : CommMonoid M] (f : ι → M) (s : Finset ι), ∏ i, f ↑i = ∏ i ∈ s, f i
-- Mathlib.CategoryTheory.Monoidal.NaturalTransformation
CategoryTheory.LaxMonoidalFunctor.Hom.mk.sizeOf_spec : ∀ {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 D]
  {F G : CategoryTheory.LaxMonoidalFunctor C D} [inst_4 : SizeOf C] [inst_5 : SizeOf D]
  (hom : F.toFunctor ⟶ G.toFunctor)
  (isMonoidal :
    autoParam (CategoryTheory.NatTrans.IsMonoidal hom) CategoryTheory.LaxMonoidalFunctor.Hom.isMonoidal._autoParam),
  sizeOf { hom := hom, isMonoidal := isMonoidal } = 1 + sizeOf hom + sizeOf isMonoidal
-- Mathlib.Analysis.Normed.Group.HomCompletion
/-- Completion of normed group homs as a normed group hom.  -/
normedAddGroupHomCompletionHom : {G : Type u_1} →
  [inst : SeminormedAddCommGroup G] →
    {H : Type u_2} →
      [inst_1 : SeminormedAddCommGroup H] →
        NormedAddGroupHom G H →+ NormedAddGroupHom (UniformSpace.Completion G) (UniformSpace.Completion H)
-- Mathlib.Analysis.Convex.Deriv
ConcaveOn.slope_le_derivWithin : ∀ {S : Set ℝ} {f : ℝ → ℝ} {x y : ℝ},
  ConcaveOn ℝ S f → x ∈ S → y ∈ S → x < y → DifferentiableWithinAt ℝ f S x → slope f x y ≤ derivWithin f S x
-- Mathlib.CategoryTheory.Preadditive.AdditiveFunctor
CategoryTheory.additiveFunctor_iff : ∀ {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] [inst_2 : CategoryTheory.Preadditive C]
  [inst_3 : CategoryTheory.Preadditive D] (F : CategoryTheory.Functor C D),
  CategoryTheory.additiveFunctor C D F ↔ F.Additive
-- Mathlib.Algebra.Ring.Int.Defs
Int.instCommRing : CommRing ℤ
-- Mathlib.Tactic.CrossRefAttribute
/-- The syntax category for the database name.  -/
Lean.Parser.Category.stacksTagDB : Lean.Parser.Category
-- Lean.CoreM
Lean.Core.withFreshMacroScope : {α : Type} → Lean.CoreM α → Lean.CoreM α
-- Mathlib.Algebra.Order.CauSeq.Completion
/-- The map from Cauchy sequences into the Cauchy completion.  -/
CauSeq.Completion.mk : {α : Type u_1} →
  [inst : Field α] →
    [inst_1 : LinearOrder α] →
      [inst_2 : IsStrictOrderedRing α] →
        {β : Type u_2} →
          [inst_3 : Ring β] →
            {abv : β → α} → [inst_4 : IsAbsoluteValue abv] → CauSeq β abv → CauSeq.Completion.Cauchy abv
-- Mathlib.NumberTheory.Zsqrtd.Basic
/-- Addition of elements of `ℤ√d`  -/
Zsqrtd.instAdd : {d : ℤ} → Add (ℤ√d)
-- Mathlib.CategoryTheory.IsoCat
CategoryTheory.IsoCat.trans_functor : ∀ {C : Type u_1} {D : Type u_2} {E : Type u_3} [inst : CategoryTheory.Category.{v_1, u_1} C]
  [inst_1 : CategoryTheory.Category.{v_2, u_2} D] [inst_2 : CategoryTheory.Category.{v_3, u_3} E]
  (e : CategoryTheory.IsoCat C D) (f : CategoryTheory.IsoCat D E), (e.trans f).functor = e.functor.comp f.functor
-- Mathlib.Order.LiminfLimsup
Filter.lt_mem_sets_of_limsSup_lt : ∀ {α : Type u_1} [inst : ConditionallyCompleteLinearOrder α] {f : Filter α} {b : α},
  Filter.IsBounded (fun x1 x2 => x1 ≤ x2) f → f.limsSup < b → ∀ᶠ (a : α) in f, a < b
-- Mathlib.RingTheory.Extension.Basic
/-- A chosen (set-theoretic) section of an extension.  -/
Algebra.Extension.σ : {R : Type u} →
  {S : Type v} →
    [inst : CommRing R] →
      [inst_1 : CommRing S] → [inst_2 : Algebra R S] → (self : Algebra.Extension R S) → S → self.Ring
-- Mathlib.RingTheory.Polynomial.ScaleRoots
Polynomial.Splits.scaleRoots : ∀ {R : Type u_1} [inst : CommSemiring R] {p : Polynomial R}, p.Splits → ∀ (r : R), (p.scaleRoots r).Splits
-- Mathlib.Topology.Sets.Closeds
TopologicalSpace.Closeds.coe_closure : ∀ {α : Type u_2} [inst : TopologicalSpace α] (s : Set α), ↑(TopologicalSpace.Closeds.closure s) = closure s
-- Lean.Meta.Tactic.Grind.Arith.Simproc
Lean.Meta.Grind.Arith.normIntDivInst : Lean.Meta.Simp.DSimproc
-- Mathlib.Analysis.Convex.Between
wbtw_swap_right_iff : ∀ (R : Type u_1) {V : Type u_2} {P : Type u_4} [inst : Ring R] [inst_1 : PartialOrder R] [inst_2 : AddCommGroup V]
  [inst_3 : Module R V] [inst_4 : AddTorsor V P] [IsOrderedRing R] [IsDomain R] [Module.IsTorsionFree R V] (x : P)
  {y z : P}, Wbtw R x y z ∧ Wbtw R x z y ↔ y = z
-- Mathlib.Geometry.Manifold.IsManifold.Basic
ModelWithCorners.isClosedEmbedding : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {H : Type u_3} [inst_3 : TopologicalSpace H] (I : ModelWithCorners 𝕜 E H),
  Topology.IsClosedEmbedding ↑I
-- Mathlib.Tactic.FieldSimp
/-- Build a transparent expression for the product of powers represented by `l : qNF M`.  -/
Mathlib.Tactic.FieldSimp.qNF.evalPretty : {v : Lean.Level} →
  {M : Q(Type v)} →
    (iM : Q(CommGroupWithZero «$M»)) →
      (l : Mathlib.Tactic.FieldSimp.qNF M) →
        Lean.MetaM
          ((e : Q(«$M»)) ×
            have a := l.toNF;
            Q(«$a».eval = «$e»))
-- Mathlib.CategoryTheory.Sites.PreservesSheafification
CategoryTheory.GrothendieckTopology.PreservesSheafification.mk : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {J : CategoryTheory.GrothendieckTopology C} {A : Type u_1}
  {B : Type u_2} [inst_1 : CategoryTheory.Category.{v_1, u_1} A] [inst_2 : CategoryTheory.Category.{v_2, u_2} B]
  {F : CategoryTheory.Functor A B},
  J.W ≤ J.W.inverseImage ((CategoryTheory.Functor.whiskeringRight Cᵒᵖ A B).obj F) → J.PreservesSheafification F
-- Mathlib.Topology.Algebra.Category.ProfiniteGrp.Completion
ProfiniteGrp.ProfiniteCompletion.diagram.eq_1 : ∀ (G : GrpCat),
  ProfiniteGrp.ProfiniteCompletion.diagram G =
    (ProfiniteGrp.ProfiniteCompletion.finiteGrpDiagram G).comp (CategoryTheory.forget₂ FiniteGrp.{u} ProfiniteGrp.{u})
-- Mathlib.Analysis.SpecialFunctions.Trigonometric.Deriv
HasFDerivAt.cos : ∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] {f : E → ℝ} {f' : StrongDual ℝ E} {x : E},
  HasFDerivAt f f' x → HasFDerivAt (fun x => Real.cos (f x)) (-Real.sin (f x) • f') x
-- Std.Tactic.BVDecide.Normalize.Equal
Std.Tactic.BVDecide.Frontend.Normalize.BitVec.eq_sub_iff_add_eq : ∀ {w : ℕ} (a b c : BitVec w), (a == c + (~~~b + 1#w)) = (a + b == c)
-- Mathlib.Geometry.Manifold.IsManifold.InteriorBoundary
Diffeomorph.preimage_interior : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {H : Type u_3} [inst_3 : TopologicalSpace H] {I : ModelWithCorners 𝕜 E H} {M : Type u_4}
  [inst_4 : TopologicalSpace M] [inst_5 : ChartedSpace H M] {E' : Type u_5} [inst_6 : NormedAddCommGroup E']
  [inst_7 : NormedSpace 𝕜 E'] {H' : Type u_6} [inst_8 : TopologicalSpace H'] {I' : ModelWithCorners 𝕜 E' H'}
  {N : Type u_7} [inst_9 : TopologicalSpace N] [inst_10 : ChartedSpace H' N] {n : WithTop ℕ∞},
  n ≠ 0 → ∀ (Φ : Diffeomorph I I' M N n), ⇑Φ ⁻¹' ModelWithCorners.interior N = ModelWithCorners.interior M
-- Mathlib.Order.SuccPred.Basic
Order.le_iff_eq_or_le_pred' : ∀ {α : Type u_1} [inst : PartialOrder α] [inst_1 : PredOrder α] {a b : α}, b ≤ a ↔ a = b ∨ b ≤ Order.pred a
-- Mathlib.AlgebraicGeometry.Morphisms.Etale
AlgebraicGeometry.Etale.instHasOfPostcompPropertyScheme : CategoryTheory.MorphismProperty.HasOfPostcompProperty @AlgebraicGeometry.Etale @AlgebraicGeometry.Etale
-- Mathlib.MeasureTheory.Measure.Prod
Measurable.map_prodMk_right : ∀ {α : Type u_1} {β : Type u_2} [inst : MeasurableSpace α] [inst_1 : MeasurableSpace β] {μ : MeasureTheory.Measure α}
  [MeasureTheory.SFinite μ], Measurable fun y => MeasureTheory.Measure.map (fun x => (x, y)) μ
-- Mathlib.CategoryTheory.Sites.SheafCohomology.Basic
/-- `H` as a functor.  -/
CategoryTheory.Sheaf.functorH : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    (J : CategoryTheory.GrothendieckTopology C) →
      [inst_1 : CategoryTheory.HasSheafify J AddCommGrpCat] →
        [CategoryTheory.HasExt (CategoryTheory.Sheaf J AddCommGrpCat)] →
          ℕ → CategoryTheory.Functor (CategoryTheory.Sheaf J AddCommGrpCat) AddCommGrpCat
-- Batteries.Recycling.RBTree.Lemmas
_private.Batteries.Recycling.RBTree.Lemmas.0.RBTree.RBNode.isOrdered.match_1.eq_2 : ∀ {α : Type u_1} (motive : Option α → Option α → Sort u_2) (x x_1 : Option α)
  (h_1 : (l r : α) → motive (some l) (some r)) (h_2 : (x x_2 : Option α) → motive x x_2),
  (∀ (l r : α), x = some l → x_1 = some r → False) →
    (match x, x_1 with
      | some l, some r => h_1 l r
      | x, x_3 => h_2 x x_3) =
      h_2 x x_1
-- Mathlib.GroupTheory.GroupAction.Hom
DistribMulActionHom.toAddMonoidHom_injective : ∀ {M : Type u_1} [inst : Monoid M] {N : Type u_2} [inst_1 : Monoid N] {φ : M →* N} {A : Type u_4} [inst_2 : AddMonoid A]
  [inst_3 : DistribMulAction M A] {B : Type u_5} [inst_4 : AddMonoid B] [inst_5 : DistribMulAction N B]
  {f g : A →ₑ+[φ] B}, ↑f = ↑g → f = g
-- Mathlib.Data.Finset.NoncommProd
Finset.noncommProd_eq_pow_card : ∀ {α : Type u_3} {β : Type u_4} [inst : Monoid β] (s : Finset α) (f : α → β)
  (comm : (↑s).Pairwise (Function.onFun Commute f)) (m : β), (∀ x ∈ s, f x = m) → s.noncommProd f comm = m ^ s.card
-- Mathlib.LinearAlgebra.RootSystem.Defs
RootPairing.root'_coroot_eq_pairing : ∀ {ι : Type u_1} {R : Type u_2} {M : Type u_3} {N : Type u_4} [inst : CommRing R] [inst_1 : AddCommGroup M]
  [inst_2 : Module R M] [inst_3 : AddCommGroup N] [inst_4 : Module R N] (P : RootPairing ι R M N) (i j : ι),
  (P.root' i) (P.coroot j) = P.pairing i j
-- Init.Data.UInt.Lemmas
USize.toFin_ofNatClamp_of_lt : ∀ {n : ℕ} (hn : n < USize.size), (USize.ofNatClamp n).toFin = ⟨n, hn⟩
-- Mathlib.AlgebraicGeometry.ResidueField
/-- The global evaluation map from `Γ(X, ⊤)` to the residue field at `x`.  -/
AlgebraicGeometry.Scheme.Γevaluation : (X : AlgebraicGeometry.Scheme) → (x : ↥X) → X.presheaf.obj (Opposite.op ⊤) ⟶ X.residueField x
-- Mathlib.NumberTheory.NumberField.InfinitePlace.Ramification
NumberField.InfinitePlace.isUnramified_mk_iff_forall_isConj : ∀ {k : Type u_1} [inst : Field k] {K : Type u_2} [inst_1 : Field K] [inst_2 : Algebra k K] [IsGalois k K] {φ : K →+* ℂ},
  NumberField.InfinitePlace.IsUnramified k (NumberField.InfinitePlace.mk φ) ↔
    ∀ (σ : Gal(K/k)), NumberField.ComplexEmbedding.IsConj φ σ → σ = 1
-- Mathlib.Algebra.Category.Semigrp.Basic
/-- Ensure that `forget₂ AddCommMonCat AddMonCat` automatically reflects
isomorphisms.  -/
AddSemigrp.forget₂_full : (CategoryTheory.forget₂ AddSemigrp AddMagmaCat).Full
-- Mathlib.Algebra.Homology.SpectralObject.Basic
CategoryTheory.Abelian.SpectralObject.Hom.ext_iff : ∀ {C : Type u_1} {ι : Type u_2} {inst : CategoryTheory.Category.{u_3, u_1} C}
  {inst_1 : CategoryTheory.Category.{u_4, u_2} ι} {inst_2 : CategoryTheory.Abelian C}
  {X X' : CategoryTheory.Abelian.SpectralObject C ι} {x y : X.Hom X'}, x = y ↔ x.hom = y.hom
-- Mathlib.RingTheory.Polynomial.Chebyshev
Polynomial.Chebyshev.C.eq_1 : ∀ (R : Type u_1) [inst : CommRing R], Polynomial.Chebyshev.C R 0 = 2
-- Mathlib.GroupTheory.Descent
/-- If `G` is a group and `f : G →* G` is an endomorphism sending subgroups into themselves,
and if there is a "height function" `h : G → ℝ` with respect to `f` and a finite subset `s`
of `G`, then `G` is finitely generated.  -/
Group.fg_of_descent : ∀ {G : Type u_1} [inst : Group G] {f : G →* G},
  (∀ (U : Subgroup G), Subgroup.map f U ≤ U) →
    ∀ {s : Set G} {h : G → ℝ} {a b c : ℝ},
      0 ≤ a →
        a < b →
          s.Finite →
            s * ↑f.range = Set.univ →
              (∀ g ∈ s, ∀ (x : G), h x ≤ a * h (g * x) + c) →
                (∀ (x : G), b * h x - c ≤ h (f x)) → ∀ [Northcott h], Group.FG G
-- Mathlib.Data.Real.ConjExponents
ENNReal.HolderConjugate.toNNReal : ∀ {p q : ENNReal}, 1 < p.toNNReal → ∀ [p.HolderConjugate q], p.toNNReal.HolderConjugate q.toNNReal
-- Aesop.Tree.Data
Aesop.MVarCluster.modify : (Aesop.MVarClusterData Aesop.Goal Aesop.Rapp → Aesop.MVarClusterData Aesop.Goal Aesop.Rapp) →
  Aesop.MVarCluster → Aesop.MVarCluster
-- Mathlib.Analysis.Normed.Operator.Conformal
isConformalMap_of_subsingleton : ∀ {R : Type u_1} {M : Type u_2} {N : Type u_3} [inst : NormedField R] [inst_1 : SeminormedAddCommGroup M]
  [inst_2 : SeminormedAddCommGroup N] [inst_3 : NormedSpace R M] [inst_4 : NormedSpace R N] [Subsingleton M]
  (f' : M →L[R] N), IsConformalMap f'
-- Mathlib.Topology.Algebra.Constructions
MulOpposite.opHomeomorph.eq_1 : ∀ {M : Type u_1} [inst : TopologicalSpace M],
  MulOpposite.opHomeomorph = { toEquiv := MulOpposite.opEquiv, continuous_toFun := ⋯, continuous_invFun := ⋯ }
-- Std.Http.Data.URI.Encoding
/-- Validates that all percent signs in a byte array are followed by exactly two hexadecimal digits.
This ensures proper percent-encoding according to RFC 3986.

For example:
- `%20` is valid (percent followed by two hex digits)
- `%` is invalid (percent with no following digits)
- `%2` is invalid (percent followed by only one digit)
- `%GG` is invalid (percent followed by non-hex characters)
 -/
Std.Http.URI.isValidPercentEncoding : ByteArray → Bool
-- Mathlib.RingTheory.Ideal.Cotangent
/-- In a local ring with its maximal ideal finitely generated,
the dimension of the cotangent space is equal to the span rank of the maximal ideal.
 -/
IsLocalRing.rank_cotangentSpace_eq_spanrank_maximalIdeal_of_fg : ∀ {R : Type u_1} [inst : CommRing R] [inst_1 : IsLocalRing R],
  (IsLocalRing.maximalIdeal R).FG →
    Module.rank (IsLocalRing.ResidueField R) (IsLocalRing.CotangentSpace R) =
      Submodule.spanRank (IsLocalRing.maximalIdeal R)
-- Init.GrindInstances.Ring.Fin
Lean.Grind.Fin.sub_eq_add_neg : ∀ {n : ℕ} [NeZero n] (a b : Fin n), a - b = a + -b
-- Mathlib.ModelTheory.Arithmetic.Presburger.Semilinear.Basic
_private.Mathlib.ModelTheory.Arithmetic.Presburger.Semilinear.Basic.0.IsProperLinearSet.base.congr_simp : ∀ {ι : Type u_3} {s s_1 : Set (ι → ℕ)} (e_s : s = s_1) (hs : IsProperLinearSet s) (a a_1 : ι),
  a = a_1 → IsProperLinearSet.base✝ hs a = IsProperLinearSet.base✝ ⋯ a_1
-- Mathlib.Probability.Process.FiniteDimensionalLaws
/-- Two stochastic processes have same law iff they have the same
finite-dimensional distributions.  -/
ProbabilityTheory.map_eq_iff_forall_finset_map_restrict_eq : ∀ {T : Type u_1} {Ω : Type u_2} {𝓧 : T → Type u_3} {mΩ : MeasurableSpace Ω} {mα : (t : T) → MeasurableSpace (𝓧 t)}
  {X Y : (t : T) → Ω → 𝓧 t} {P : MeasureTheory.Measure Ω} [MeasureTheory.IsFiniteMeasure P],
  AEMeasurable (fun ω x => X x ω) P →
    AEMeasurable (fun ω x => Y x ω) P →
      (MeasureTheory.Measure.map (fun ω x => X x ω) P = MeasureTheory.Measure.map (fun ω x => Y x ω) P ↔
        ∀ (I : Finset T),
          MeasureTheory.Measure.map (fun ω => I.restrict fun x => X x ω) P =
            MeasureTheory.Measure.map (fun ω => I.restrict fun x => Y x ω) P)
-- Mathlib.Topology.CWComplex.Classical.Basic
Topology.RelCWComplex.toCWComplex_cell : ∀ {X : Type u_1} [inst : TopologicalSpace X] (C : Set X) [inst_1 : Topology.RelCWComplex C ∅] (n : ℕ),
  Topology.CWComplex.cell C n = Topology.RelCWComplex.cell C n
-- Mathlib.AlgebraicTopology.SimplicialObject.Basic
/-- Drop the augmentation.  -/
CategoryTheory.CosimplicialObject.Augmented.drop : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    CategoryTheory.Functor (CategoryTheory.CosimplicialObject.Augmented C) (CategoryTheory.CosimplicialObject C)
-- Mathlib.Combinatorics.SimpleGraph.Walk.Traversal
SimpleGraph.Walk.mk_mem_edges_iff_exists : ∀ {V : Type u} {G : SimpleGraph V} {u v u' v' : V} (p : G.Walk u v),
  s(u', v') ∈ p.edges ↔ ∃ i < p.length, s(p.getVert i, p.getVert (i + 1)) = s(u', v')
-- Mathlib.Probability.Kernel.Composition.IntegralCompProd
ProbabilityTheory.Kernel.integral_fn_integral_sub_comp : ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} {E : Type u_4} {mα : MeasurableSpace α} {mβ : MeasurableSpace β}
  {mγ : MeasurableSpace γ} [inst : NormedAddCommGroup E] {a : α} {κ : ProbabilityTheory.Kernel α β}
  {η : ProbabilityTheory.Kernel β γ} [inst_1 : NormedSpace ℝ E] {E' : Type u_5} [inst_2 : NormedAddCommGroup E']
  [inst_3 : NormedSpace ℝ E'] ⦃f g : γ → E⦄ (F : E → E'),
  MeasureTheory.Integrable f ((η.comp κ) a) →
    MeasureTheory.Integrable g ((η.comp κ) a) →
      ∫ (x : β), F (∫ (y : γ), f y - g y ∂η x) ∂κ a = ∫ (x : β), F (∫ (y : γ), f y ∂η x - ∫ (y : γ), g y ∂η x) ∂κ a
-- Batteries.CodeAction.Attr
Batteries.CodeAction.mkTacticCodeAction.unsafe_impl_2 : Lean.Name → Lean.Environment → Lean.Options → ExceptT String Id Batteries.CodeAction.TacticCodeAction
-- Mathlib.Topology.Algebra.Module.Spaces.ContinuousLinearMap
ContinuousLinearMap.toLinearMap₁₂_injective : ∀ {R : Type u_1} {𝕜₂ : Type u_3} {𝕜₃ : Type u_4} {E : Type u_5} {F : Type u_6} {G : Type u_7} [inst : Semiring R]
  [inst_1 : NormedField 𝕜₂] [inst_2 : NormedField 𝕜₃] [inst_3 : AddCommMonoid E] [inst_4 : Module R E]
  [inst_5 : TopologicalSpace E] [inst_6 : AddCommGroup F] [inst_7 : Module 𝕜₂ F] [inst_8 : TopologicalSpace F]
  [inst_9 : AddCommGroup G] [inst_10 : Module 𝕜₃ G] [inst_11 : TopologicalSpace G] [inst_12 : IsTopologicalAddGroup G]
  [inst_13 : ContinuousConstSMul 𝕜₃ G] {σ₁₃ : R →+* 𝕜₃} {σ₂₃ : 𝕜₂ →+* 𝕜₃},
  Function.Injective ⇑ContinuousLinearMap.toLinearMap₁₂
-- Mathlib.CategoryTheory.Limits.WeakLimits.WeakKernels
/-- The map from `weakKernel f` into the source of `f`.  -/
CategoryTheory.Limits.weakKernel.ι : {C : Type u_1} →
  [inst : CategoryTheory.Category.{v_1, u_1} C] →
    [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C] →
      {X Y : C} →
        (f : X ⟶ Y) → [inst_2 : CategoryTheory.Limits.HasWeakKernel f] → CategoryTheory.Limits.weakKernel f ⟶ X