mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.CategoryTheory.Products.Bifunctor
CategoryTheory.Bifunctor.map_comp_id : ∀ {C : Type u₁} {D : Type u₂} {E : Type u₃} [inst : CategoryTheory.Category.{v₁, u₁} C]
  [inst_1 : CategoryTheory.Category.{v₂, u₂} D] [inst_2 : CategoryTheory.Category.{v₃, u₃} E]
  (F : CategoryTheory.Functor (C × D) E) (X Y Z : C) (W : D) (f : X ⟶ Y) (g : Y ⟶ Z),
  F.map (CategoryTheory.Prod.mkHom (CategoryTheory.CategoryStruct.comp f g) (CategoryTheory.CategoryStruct.id W)) =
    CategoryTheory.CategoryStruct.comp (F.map (CategoryTheory.Prod.mkHom f (CategoryTheory.CategoryStruct.id W)))
      (F.map (CategoryTheory.Prod.mkHom g (CategoryTheory.CategoryStruct.id W)))
-- Std.Data.DTreeMap.Raw.Lemmas
Std.DTreeMap.Raw.Const.compare_minKeyD_modify_eq : ∀ {α : Type u} {cmp : α → α → Ordering} {β : Type v} {t : Std.DTreeMap.Raw α (fun x => β) cmp} [Std.TransCmp cmp],
  t.WF →
    ∀ {k : α} {f : β → β} {fallback : α},
      cmp ((Std.DTreeMap.Raw.Const.modify t k f).minKeyD fallback) (t.minKeyD fallback) = Ordering.eq
-- Mathlib.CategoryTheory.WithTerminal.Cone
Under.hasColimit_of_hasColimit_liftFromUnder : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {J : Type w} [inst_1 : CategoryTheory.Category.{w', w} J]
  {X : C} (F : CategoryTheory.Functor J (CategoryTheory.Under X))
  [CategoryTheory.Limits.HasColimit (CategoryTheory.WithInitial.liftFromUnder.obj F)],
  CategoryTheory.Limits.HasColimit F
-- Mathlib.Topology.Algebra.Valued.WithVal
WithVal.instFinite : ∀ {R : Type u_1} {Γ₀ : Type u_2} [inst : LinearOrderedCommGroupWithZero Γ₀] [inst_1 : Ring R] (v : Valuation R Γ₀)
  {S : Type u_3} [inst_2 : AddCommMonoid S] [inst_3 : Module R S] [Module.Finite R S], Module.Finite (WithVal v) S
-- Std.Sync.Channel
/-- Try to receive a value from the channel, if this can be completed right away without blocking return
`some value`, otherwise return `none`.
 -/
Std.CloseableChannel.Sync.tryRecv : {α : Type} → Std.CloseableChannel.Sync α → BaseIO (Option α)
-- Init.Data.List.MinMaxIdx
_private.Init.Data.List.MinMaxIdx.0.List.minIdxOn_eq_go_drop : ∀ {β : Type u_1} {α : Type u_2} [inst : LE β] [inst_1 : DecidableLE β] [Std.IsLinearPreorder β] {f : α → β}
  {xs : List α} (h : xs ≠ []) {k : ℕ},
  ∃ i,
    ∃ (hlt : i < xs.length),
      i ≤ k ∧
        xs[i] = List.minOn f (List.take (k + 1) xs) ⋯ ∧
          List.minIdxOn f xs h =
            List.minIdxOn.go✝ f (List.minOn f (List.take (k + 1) xs) ⋯) i (k + 1) (List.drop (k + 1) xs)
-- Mathlib.Topology.Algebra.Order.Field
Filter.Tendsto.inv_tendsto_atBot : ∀ {𝕜 : Type u_1} {α : Type u_2} [inst : Field 𝕜] [inst_1 : LinearOrder 𝕜] [IsStrictOrderedRing 𝕜]
  [inst_3 : TopologicalSpace 𝕜] [OrderTopology 𝕜] {l : Filter α} {f : α → 𝕜},
  Filter.Tendsto f l Filter.atBot → Filter.Tendsto f⁻¹ l (nhds 0)
-- Mathlib.Data.Nat.GCD.Basic
Nat.Coprime.of_dvd : ∀ {a₁ a₂ b₁ b₂ : ℕ}, a₁ ∣ a₂ → b₁ ∣ b₂ → a₂.Coprime b₂ → a₁.Coprime b₁
-- Lean.Data.Lsp.Basic
Lean.Lsp.ApplyWorkspaceEditParams.mk.inj : ∀ {label? : Option String} {edit : Lean.Lsp.WorkspaceEdit} {label?_1 : Option String} {edit_1 : Lean.Lsp.WorkspaceEdit},
  { label? := label?, edit := edit } = { label? := label?_1, edit := edit_1 } → label? = label?_1 ∧ edit = edit_1
-- Mathlib.Analysis.Convex.SpecificFunctions.Pow
Real.concaveOn_rpow : ∀ {p : ℝ}, 0 ≤ p → p ≤ 1 → ConcaveOn ℝ (Set.Ici 0) fun x => x ^ p
-- Mathlib.Analysis.SpecialFunctions.Complex.LogBounds
/-- Represent `log (1 - z)⁻¹` as an integral over the unit interval  -/
Complex.log_inv_eq_integral : ∀ {z : ℂ}, 1 - z ∈ Complex.slitPlane → Complex.log (1 - z)⁻¹ = z * ∫ (t : ℝ) in 0..1, (1 - t • z)⁻¹
-- Mathlib.NumberTheory.NumberField.InfinitePlace.Embeddings
/-- Let `B` be a real number. The set of algebraic integers in `K` whose conjugates are all
smaller in norm than `B` is finite.  -/
NumberField.Embeddings.finite_of_norm_le : ∀ (K : Type u_1) [inst : Field K] [NumberField K] (A : Type u_2) [inst_2 : NormedField A] [IsAlgClosed A]
  [NormedAlgebra ℚ A] (B : ℝ), {x | IsIntegral ℤ x ∧ ∀ (φ : K →+* A), ‖φ x‖ ≤ B}.Finite
-- Mathlib.LinearAlgebra.RootSystem.Defs
RootPairing.isPerfPair_toLinearMap : ∀ {ι : 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] (self : RootPairing ι R M N), self.IsPerfPair
-- Mathlib.RingTheory.MvPolynomial.Homogeneous
MvPolynomial.homogeneousComponent_zero : ∀ {σ : Type u_1} {R : Type u_3} [inst : CommSemiring R] (φ : MvPolynomial σ R),
  (MvPolynomial.homogeneousComponent 0) φ = MvPolynomial.C (MvPolynomial.coeff 0 φ)
-- Mathlib.RingTheory.DividedPowers.SubDPIdeal
DividedPowers.dpEqualizer_is_dp_ideal_left : ∀ {A : Type u_1} [inst : CommSemiring A] {I : Ideal A} (hI hI' : DividedPowers I), hI.IsSubDPIdeal (hI.dpEqualizer hI')
-- Init.Data.Range.Polymorphic.IntLemmas
Int.toList_roo_eq_nil : ∀ {m n : ℤ}, n ≤ m + 1 → (m<...n).toList = []
-- Mathlib.Algebra.Group.Units.Defs
IsAddUnit.exists_neg' : ∀ {M : Type u_1} [inst : AddMonoid M] {a : M}, IsAddUnit a → ∃ b, b + a = 0
-- Mathlib.Algebra.MonoidAlgebra.MapDomain
MonoidAlgebra.mapRingHom_single : ∀ {R : Type u_3} {S : Type u_4} {M : Type u_6} [inst : Semiring R] [inst_1 : Semiring S] [inst_2 : Monoid M]
  (f : R →+* S) (a : M) (b : R),
  (MonoidAlgebra.mapRingHom M f) (MonoidAlgebra.single a b) = MonoidAlgebra.single a (f b)
-- Mathlib.AlgebraicTopology.SimplexCategory.SemiSimplexCategory
SemiSimplexCategory.mk.injEq : ∀ (len len_1 : ℕ), ({ len := len } = { len := len_1 }) = (len = len_1)
-- Mathlib.Geometry.RingedSpace.PresheafedSpace
AlgebraicGeometry.PresheafedSpace.instCoeSortType : {C : Type u_1} →
  [inst : CategoryTheory.Category.{v_1, u_1} C] → CoeSort (AlgebraicGeometry.PresheafedSpace C) (Type u_2)
-- Mathlib.Algebra.TrivSqZeroExt.Ideal
TrivSqZeroExt.mem_kerIdeal_iff_inr : ∀ (R : Type u_1) (M : Type u_2) [inst : CommSemiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M]
  [inst_3 : Module Rᵐᵒᵖ M] [inst_4 : IsCentralScalar R M] (x : TrivSqZeroExt R M),
  x ∈ TrivSqZeroExt.kerIdeal R M ↔ x = TrivSqZeroExt.inr x.snd
-- Mathlib.Order.Defs.PartialOrder
lt_irrefl : ∀ {α : Type u_1} [inst : Preorder α] (a : α), ¬a < a
-- Mathlib.Combinatorics.SimpleGraph.Tutte
/-- This lemma shows an alternating cycle exists in a specific subcase of the proof
of Tutte's theorem.  -/
_private.Mathlib.Combinatorics.SimpleGraph.Tutte.0.SimpleGraph.tutte_exists_isAlternating_isCycles : ∀ {V : Type u_1} {G G' : SimpleGraph V} {x b a c : V} {M : (G ⊔ SimpleGraph.edge a c).Subgraph} (p : G'.Walk a x),
  p.IsPath →
    G'.IsAlternating M.spanningCoe →
      ¬M.Adj x a →
        p.toSubgraph.Adj a c →
          ¬p.toSubgraph.Adj x b →
            M.Adj a c →
              G.Adj x a →
                x ≠ c →
                  a ≠ b →
                    p.toSubgraph.spanningCoe ≤ G ⊔ SimpleGraph.edge a c →
                      (∀ (c' : V), c' ≠ a → p.toSubgraph.Adj c' x → M.Adj c' x) →
                        ∃ G',
                          G'.IsAlternating M.spanningCoe ∧
                            G'.IsCycles ∧ ¬G'.Adj x b ∧ G'.Adj a c ∧ G' ≤ G ⊔ SimpleGraph.edge a c
-- Std.Data.ExtDHashMap.Lemmas
Std.ExtDHashMap.get!_ofList_of_contains_eq_false : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} {β : α → Type v} [inst : LawfulBEq α] {l : List ((a : α) × β a)} {k : α}
  [inst_1 : Inhabited (β k)], (List.map Sigma.fst l).contains k = false → (Std.ExtDHashMap.ofList l).get! k = default
-- Mathlib.CategoryTheory.Bicategory.NaturalTransformation.Oplax
CategoryTheory.Oplax.StrongTrans.categoryStruct_comp_app : ∀ {B : Type u₁} [inst : CategoryTheory.Bicategory B] {C : Type u₂} [inst_1 : CategoryTheory.Bicategory C]
  {X Y Z : CategoryTheory.OplaxFunctor B C} (η : CategoryTheory.Oplax.StrongTrans X Y)
  (θ : CategoryTheory.Oplax.StrongTrans Y Z) (a : B),
  (CategoryTheory.CategoryStruct.comp η θ).app a = (η.toOplax.vcomp θ.toOplax).app a
-- Mathlib.Analysis.SpecialFunctions.Complex.Log
Complex.log_exp_exists : ∀ (z : ℂ), ∃ n, Complex.log (Complex.exp z) = z + ↑n * (2 * ↑Real.pi * Complex.I)
-- Std.Data.DHashMap.Basic
/-- Checks if all elements satisfy the predicate, short-circuiting if a predicate fails.  -/
Std.DHashMap.all : {α : Type u} → {β : α → Type v} → {x : BEq α} → {x_1 : Hashable α} → Std.DHashMap α β → ((a : α) → β a → Bool) → Bool
-- Init.Control.Lawful.Basic
/-- A `bind` followed by a functorial map is equivalent to `Applicative` sequencing.

This means that the effect sequencing from `Monad` and `Applicative` are the same.
 -/
LawfulMonad.bind_map : ∀ {m : Type u → Type v} {inst : Monad m} [self : LawfulMonad m] {α β : Type u} (f : m (α → β)) (x : m α),
  (do
      let x_1 ← f
      x_1 <$> x) =
    f <*> x
-- Mathlib.Analysis.SpecialFunctions.Log.Basic
/-- The real logarithm function tends to `+∞` at `+∞`.  -/
Real.tendsto_log_atTop : Filter.Tendsto Real.log Filter.atTop Filter.atTop
-- Mathlib.Algebra.Homology.HomologicalComplex
HomologicalComplex.eval_obj : ∀ {ι : Type u_1} (V : Type u) [inst : CategoryTheory.Category.{v, u} V]
  [inst_1 : CategoryTheory.Limits.HasZeroMorphisms V] (c : ComplexShape ι) (i : ι) (C : HomologicalComplex V c),
  (HomologicalComplex.eval V c i).obj C = C.X i
-- Lean.Elab.Match
_private.Lean.Elab.Match.0.Lean.Elab.Term.mkUserNameFor : Lean.Expr → Lean.Elab.TermElabM Lean.Name
-- Mathlib.Algebra.Homology.Embedding.Extend
HomologicalComplex.extend.XOpIso_hom_d_op_assoc : ∀ {ι : Type u_1} {c : ComplexShape ι} {C : Type u_3} [inst : CategoryTheory.Category.{v_1, u_3} C]
  [inst_1 : CategoryTheory.Limits.HasZeroObject C] [inst_2 : CategoryTheory.Limits.HasZeroMorphisms C]
  (K : HomologicalComplex C c) (i j : Option ι) {Z : Cᵒᵖ} (h : Opposite.op (HomologicalComplex.extend.X K j) ⟶ Z),
  CategoryTheory.CategoryStruct.comp (HomologicalComplex.extend.XOpIso K i).hom
      (CategoryTheory.CategoryStruct.comp (HomologicalComplex.extend.d K j i).op h) =
    CategoryTheory.CategoryStruct.comp (HomologicalComplex.extend.d K.op i j)
      (CategoryTheory.CategoryStruct.comp (HomologicalComplex.extend.XOpIso K j).hom h)
-- Init.Data.Array.Attach
Array.foldl_wfParam : ∀ {α : Type u_1} {β : Type u_2} {xs : Array α} {f : β → α → β} {x : β},
  Array.foldl f x (wfParam xs) = Array.foldl f x xs.attach.unattach
-- Mathlib.Algebra.Order.Archimedean.Real.Basic
/-- As `⨆ i, f i = 0` when the domain of the real-valued function `f` is empty or unbounded above,
it suffices to show that all values of `f` are nonnegative to show that `0 ≤ ⨆ i, f i`.  -/
Real.iSup_nonneg : ∀ {ι : Sort u_1} {f : ι → ℝ}, (∀ (i : ι), 0 ≤ f i) → 0 ≤ ⨆ i, f i
-- Mathlib.Algebra.Order.Group.OrderIso
OrderIso.subLeft.eq_1 : ∀ {α : Type u} [inst : AddGroup α] [inst_1 : LE α] [inst_2 : AddLeftMono α] [inst_3 : AddRightMono α] (a : α),
  OrderIso.subLeft a = { toEquiv := (Equiv.subLeft a).trans OrderDual.toDual, map_rel_iff' := ⋯ }
-- Mathlib.NumberTheory.Harmonic.ZetaAsymp
differentiable_riemannZeta₀ : Differentiable ℂ riemannZeta₀
-- Mathlib.CategoryTheory.Join.Basic
/-- The "canonical" natural transformation from `(Prod.fst C D) ⋙ inclLeft C D` to
`(Prod.snd C D) ⋙ inclRight C D`. This is bundling together all the edge morphisms
into the data of a natural transformation.  -/
CategoryTheory.Join.edgeTransform : (C : Type u₁) →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    (D : Type u₂) →
      [inst_1 : CategoryTheory.Category.{v₂, u₂} D] →
        (CategoryTheory.Prod.fst C D).comp (CategoryTheory.Join.inclLeft C D) ⟶
          (CategoryTheory.Prod.snd C D).comp (CategoryTheory.Join.inclRight C D)
-- Lean.DocString.Types
Lean.Doc.Block.concat.inj : ∀ {i : Type u} {b : Type v} {content content_1 : Array (Lean.Doc.Block i b)},
  Lean.Doc.Block.concat content = Lean.Doc.Block.concat content_1 → content = content_1
-- Mathlib.Order.Hom.BoundedLattice
BoundedLatticeHom.comp_id : ∀ {α : Type u_2} {β : Type u_3} [inst : Lattice α] [inst_1 : Lattice β] [inst_2 : BoundedOrder α]
  [inst_3 : BoundedOrder β] (f : BoundedLatticeHom α β), f.comp (BoundedLatticeHom.id α) = f
-- Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Rpow.Basic
CFC.sqrt_eq_cfc : ∀ {A : Type u_1} [inst : PartialOrder A] [inst_1 : Ring A] [inst_2 : StarRing A] [inst_3 : TopologicalSpace A]
  [inst_4 : StarOrderedRing A] [inst_5 : Algebra ℝ A] [inst_6 : ContinuousFunctionalCalculus ℝ A IsSelfAdjoint]
  [inst_7 : NonnegSpectrumClass ℝ A] [IsSemitopologicalRing A] [T2Space A] {a : A}, CFC.sqrt a = cfc (⇑NNReal.sqrt) a
-- Lean.Server.Completion.EligibleHeaderDecls
Lean.Server.Completion.getCompletionTagsForDecl : Lean.Name → Lean.MetaM (Array Lean.Lsp.CompletionItemTag)
-- Mathlib.RingTheory.FractionalIdeal.Norm
FractionalIdeal.absNorm_span_singleton : ∀ (R : Type u_1) [inst : CommRing R] [inst_1 : IsDedekindDomain R] [inst_2 : Module.Free ℤ R]
  [inst_3 : Module.Finite ℤ R] {K : Type u_2} [inst_4 : CommRing K] [inst_5 : Algebra R K] [inst_6 : IsFractionRing R K]
  [IsLocalization (Algebra.algebraMapSubmonoid R (nonZeroDivisors ℤ)) K] [inst_8 : Algebra ℚ K] [Module.Finite ℚ K]
  (x : K), FractionalIdeal.absNorm (FractionalIdeal.spanSingleton (nonZeroDivisors R) x) = |(Algebra.norm ℚ) x|
-- Mathlib.Analysis.Asymptotics.TVS
Asymptotics.IsLittleOTVS.neg_left : ∀ {α : Type u_1} {𝕜 : Type u_3} {E : Type u_4} {F : Type u_5} [inst : NontriviallyNormedField 𝕜]
  [inst_1 : AddCommGroup E] [inst_2 : TopologicalSpace E] [inst_3 : Module 𝕜 E] [inst_4 : AddCommGroup F]
  [inst_5 : TopologicalSpace F] [inst_6 : Module 𝕜 F] {l : Filter α} {f : α → E} {g : α → F} [ContinuousNeg E],
  f =o[𝕜; l] g → (-f) =o[𝕜; l] g
-- Init.Data.Option.Lemmas
Option.some_or : ∀ {α : Type u_1} {a : α} {o : Option α}, (some a).or o = some a
-- Mathlib.CategoryTheory.Triangulated.Triangulated
/-- `m₃` is the morphism `b` of (TR 4) as presented in Stacks.  -/
CategoryTheory.Triangulated.Octahedron.m₃ : {C : Type u_1} →
  [inst : CategoryTheory.Category.{v_1, u_1} C] →
    [inst_1 : CategoryTheory.Preadditive C] →
      [inst_2 : CategoryTheory.Limits.HasZeroObject C] →
        [inst_3 : CategoryTheory.HasShift C ℤ] →
          [inst_4 : ∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive] →
            [inst_5 : CategoryTheory.Pretriangulated C] →
              {X₁ X₂ X₃ Z₁₂ Z₂₃ Z₁₃ : C} →
                {u₁₂ : X₁ ⟶ X₂} →
                  {u₂₃ : X₂ ⟶ X₃} →
                    {u₁₃ : X₁ ⟶ X₃} →
                      {comm : CategoryTheory.CategoryStruct.comp u₁₂ u₂₃ = u₁₃} →
                        {v₁₂ : X₂ ⟶ Z₁₂} →
                          {w₁₂ : Z₁₂ ⟶ (CategoryTheory.shiftFunctor C 1).obj X₁} →
                            {h₁₂ :
                                CategoryTheory.Pretriangulated.Triangle.mk u₁₂ v₁₂ w₁₂ ∈
                                  CategoryTheory.Pretriangulated.distinguishedTriangles} →
                              {v₂₃ : X₃ ⟶ Z₂₃} →
                                {w₂₃ : Z₂₃ ⟶ (CategoryTheory.shiftFunctor C 1).obj X₂} →
                                  {h₂₃ :
                                      CategoryTheory.Pretriangulated.Triangle.mk u₂₃ v₂₃ w₂₃ ∈
                                        CategoryTheory.Pretriangulated.distinguishedTriangles} →
                                    {v₁₃ : X₃ ⟶ Z₁₃} →
                                      {w₁₃ : Z₁₃ ⟶ (CategoryTheory.shiftFunctor C 1).obj X₁} →
                                        {h₁₃ :
                                            CategoryTheory.Pretriangulated.Triangle.mk u₁₃ v₁₃ w₁₃ ∈
                                              CategoryTheory.Pretriangulated.distinguishedTriangles} →
                                          CategoryTheory.Triangulated.Octahedron comm h₁₂ h₂₃ h₁₃ → (Z₁₃ ⟶ Z₂₃)
-- Mathlib.CategoryTheory.Limits.Weighted.HasWeightedLimit
CategoryTheory.Functor.weightedLimFlipObjMap_comp : ∀ {J : Type u} [inst : CategoryTheory.Category.{v, u} J] {C : Type u'} [inst_1 : CategoryTheory.Category.{v', u'} C]
  {W W' W'' : CategoryTheory.Functor J (Type w)} (g : W ⟶ W') (g' : W' ⟶ W'') (F : CategoryTheory.Functor J C)
  [inst_2 : CategoryTheory.Limits.HasWeightedLimit W F] [inst_3 : CategoryTheory.Limits.HasWeightedLimit W' F]
  [inst_4 : CategoryTheory.Limits.HasWeightedLimit W'' F],
  CategoryTheory.CategoryStruct.comp (CategoryTheory.Functor.weightedLimFlipObjMap g' F)
      (CategoryTheory.Functor.weightedLimFlipObjMap g F) =
    CategoryTheory.Functor.weightedLimFlipObjMap (CategoryTheory.CategoryStruct.comp g g') F
-- Mathlib.Data.Erased
Erased.out_inj : ∀ {α : Sort u_1} (a b : Erased α), a.out = b.out → a = b
-- Std.Do.Triple.SpecLemmas
Std.Do.Iter.fold_mapM : ∀ {ps : Std.Do.PostShape} {α β γ δ : Type w} {n : Type w → Type w''} [inst : Std.Iterator α Id β]
  [Std.Iterators.Finite α Id] [inst_2 : Monad n] [inst_3 : MonadAttach n] [LawfulMonad n] [WeaklyLawfulMonadAttach n]
  [inst_6 : Std.Do.WPMonad n ps] [inst_7 : Std.IteratorLoop α Id n] [Std.LawfulIteratorLoop α Id n] {f : β → n γ}
  {g : δ → γ → δ} {init : δ} {it : Std.Iter β} {P : Std.Do.Assertion ps} {Q : Std.Do.PostCond δ ps},
  ⦃P⦄
      Std.Iter.foldM
        (fun d b => do
          let c ← f b
          pure (g d c))
        init it ⦃Q⦄ →
    ⦃P⦄ Std.IterM.fold g init (Std.Iter.mapM f it) ⦃Q⦄
-- Lean.Meta.Match.MatcherInfo
Lean.Meta.Match.Overlaps.mk.injEq : ∀ (map map_1 : Std.HashMap ℕ (Std.TreeSet ℕ compare)), ({ map := map } = { map := map_1 }) = (map = map_1)
-- Mathlib.MeasureTheory.Group.Action
MeasureTheory.smulInvariantMeasure_iterateMulAct : ∀ {α : Type w} {f : α → α} {x : MeasurableSpace α} {μ : MeasureTheory.Measure α},
  Measurable f → (MeasureTheory.SMulInvariantMeasure (IterateMulAct f) α μ ↔ MeasureTheory.MeasurePreserving f μ μ)
-- Mathlib.Analysis.Calculus.TangentCone.Basic
IsOpen.uniqueDiffOn : ∀ {𝕜 : Type u_1} {E : Type u_2} [inst : DivisionSemiring 𝕜] [inst_1 : AddCommGroup E] [inst_2 : Module 𝕜 E]
  [inst_3 : TopologicalSpace E] [inst_4 : TopologicalSpace 𝕜] [(nhdsWithin 0 {0}ᶜ).NeBot] [ContinuousSMul 𝕜 E]
  {s : Set E} [ContinuousAdd E], IsOpen s → UniqueDiffOn 𝕜 s
-- Mathlib.Topology.MetricSpace.Gluing
Metric.instMetricSpaceInductiveLimit : {X : ℕ → Type u} →
  [inst : (n : ℕ) → MetricSpace (X n)] →
    {f : (n : ℕ) → X n → X (n + 1)} → {I : ∀ (n : ℕ), Isometry (f n)} → MetricSpace (Metric.InductiveLimit I)
-- Mathlib.AlgebraicTopology.ModelCategory.FibrantObjectHomotopy
HomotopicalAlgebra.FibrantObject.instCofibrationIResolutionObj : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : HomotopicalAlgebra.ModelCategory C] (X : C),
  HomotopicalAlgebra.Cofibration (HomotopicalAlgebra.FibrantObject.HoCat.iResolutionObj X)
-- Mathlib.AlgebraicGeometry.Morphisms.Finite
AlgebraicGeometry.IsFinite.instIsIntegralHom : ∀ {X Y : AlgebraicGeometry.Scheme} (f : X ⟶ Y) [AlgebraicGeometry.IsFinite f], AlgebraicGeometry.IsIntegralHom f
-- Mathlib.Dynamics.TopologicalEntropy.Subset
Dynamics.coverEntropyInf_biUnion_le : ∀ {X : Type u_1} {ι : Type u_2} [inst : UniformSpace X] (s : Set ι) (T : X → X) (F : ι → Set X),
  ⨆ i ∈ s, Dynamics.coverEntropyInf T (F i) ≤ Dynamics.coverEntropyInf T (⋃ i ∈ s, F i)
-- Mathlib.Algebra.Ring.Aut
/-- The group operation on automorphisms of a ring is defined by
`fun g h => RingEquiv.trans h g`.
This means that multiplication agrees with composition, `(g*h)(x) = g (h x)`.  -/
RingAut.instGroup : (R : Type u_1) → [inst : Mul R] → [inst_1 : Add R] → Group (RingAut R)
-- Mathlib.FieldTheory.Relrank
IntermediateField.relrank_dvd_rank_top_of_le : ∀ {F : Type u} {E : Type v} [inst : Field F] [inst_1 : Field E] [inst_2 : Algebra F E] {A B : IntermediateField F E},
  A ≤ B → A.relrank B ∣ Module.rank (↥A) E
-- Mathlib.Combinatorics.SimpleGraph.Acyclic
/-- A nontrivial tree has a vertex of degree one.  -/
SimpleGraph.IsTree.exists_vert_degree_one_of_nontrivial : ∀ {V : Type u_1} {G : SimpleGraph V} [inst : Fintype V] [Nontrivial V] [inst_2 : DecidableRel G.Adj],
  G.IsTree → ∃ v, G.degree v = 1
-- Mathlib.ModelTheory.Basic
/-- The homomorphism commutes with the interpretations of the function symbols  -/
FirstOrder.Language.Hom.map_fun' : ∀ {L : FirstOrder.Language} {M : Type w} {N : Type w'} [inst : L.Structure M] [inst_1 : L.Structure N]
  (self : L.Hom M N) {n : ℕ} (f : L.Functions n) (x : Fin n → M),
  self.toFun (FirstOrder.Language.Structure.funMap f x) = FirstOrder.Language.Structure.funMap f (self.toFun ∘ x)
-- Mathlib.Condensed.Discrete.Colimit
Condensed.lanPresheafExt_hom : ∀ {F G : CategoryTheory.Functor Profiniteᵒᵖ (Type (u + 1))} (S : Profiniteᵒᵖ)
  (i : FintypeCat.toProfinite.op.comp F ≅ FintypeCat.toProfinite.op.comp G),
  (Condensed.lanPresheafExt i).hom.app S =
    CategoryTheory.Limits.colimMap
      ((CategoryTheory.CostructuredArrow.proj FintypeCat.toProfinite.op S).whiskerLeft i.hom)
-- Mathlib.Data.List.Basic
List.mem_of_mem_filter : ∀ {α : Type u} {p : α → Bool} {a : α} {l : List α}, a ∈ List.filter p l → a ∈ l
-- Mathlib.CategoryTheory.Equivalence.Symmetry
CategoryTheory.Equivalence.symmEquivInverse_obj_counitIso_inv : ∀ (C : Type u_1) [inst : CategoryTheory.Category.{v_1, u_1} C] (D : Type u_2)
  [inst_1 : CategoryTheory.Category.{v_2, u_2} D] (X : (D ≌ C)ᵒᵖ),
  ((CategoryTheory.Equivalence.symmEquivInverse C D).obj X).counitIso.inv = (Opposite.unop X).unitIso.hom
-- Std.Async.Basic
Std.Async.MaybeTask.pure.sizeOf_spec : ∀ {α : Type} [inst : SizeOf α] (a : α), sizeOf (Std.Async.MaybeTask.pure a) = 1 + sizeOf a
-- Init.Data.UInt.Lemmas
UInt64.toUInt32_ofNat : ∀ {n : ℕ}, (OfNat.ofNat n).toUInt32 = OfNat.ofNat n
-- Mathlib.Algebra.Order.Module.Defs
SMulPosStrictMono.toSMulPosReflectLE : ∀ {α : Type u_1} {β : Type u_2} [inst : SMul α β] [inst_1 : LinearOrder α] [inst_2 : Preorder β] [inst_3 : Zero β]
  [SMulPosStrictMono α β], SMulPosReflectLE α β
-- Mathlib.Analysis.Analytic.Order
/-- The order is additive when multiplying analytic functions.  -/
analyticOrderAt_mul : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {f g : 𝕜 → 𝕜} {z₀ : 𝕜},
  AnalyticAt 𝕜 f z₀ → AnalyticAt 𝕜 g z₀ → analyticOrderAt (f * g) z₀ = analyticOrderAt f z₀ + analyticOrderAt g z₀
-- Mathlib.LinearAlgebra.Matrix.Charpoly.Basic
Matrix.charpoly_units_conj : ∀ {R : Type u_1} [inst : CommRing R] {n : Type u_4} [inst_1 : DecidableEq n] [inst_2 : Fintype n] (M : (Matrix n n R)ˣ)
  (N : Matrix n n R), (↑M * N * (↑M)⁻¹).charpoly = N.charpoly
-- Mathlib.MeasureTheory.Function.LpSeminorm.Basic
MeasureTheory.memLp_of_bounded : ∀ {α : Type u_1} {m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} [MeasureTheory.IsFiniteMeasure μ] {a b : ℝ}
  {f : α → ℝ},
  (∀ᵐ (x : α) ∂μ, f x ∈ Set.Icc a b) →
    MeasureTheory.AEStronglyMeasurable f μ → ∀ (p : ENNReal), MeasureTheory.MemLp f p μ
-- Mathlib.Dynamics.Ergodic.Action.Regular
instErgodicVAddAddOppositeOfIsAddRightInvariant : ∀ {G : Type u_1} [inst : AddGroup G] [inst_1 : MeasurableSpace G] [MeasurableAdd₂ G] [MeasurableNeg G]
  {μ : MeasureTheory.Measure G} [MeasureTheory.SFinite μ] [μ.IsAddRightInvariant], ErgodicVAdd Gᵃᵒᵖ G μ
-- Std.Data.DTreeMap.Internal.Zipper
Std.DTreeMap.Internal.toList_roi : ∀ {α : Type u} {β : α → Type v} [inst : Ord α] [Std.TransOrd α] (t : Std.DTreeMap.Internal.Impl α β),
  t.Ordered →
    ∀ (lowerBound : α),
      Std.Slice.toList (Std.Roi.Sliceable.mkSlice t lowerBound<...*) =
        List.filter (fun e => (compare e.fst lowerBound).isGT) t.toList
-- Mathlib.Algebra.Homology.Augment
_private.Mathlib.Algebra.Homology.Augment.0.CochainComplex.augment.match_1.eq_1 : ∀ (motive : ℕ → ℕ → Sort u_1) (h_1 : Unit → motive 0 1) (h_2 : (i j : ℕ) → motive i.succ j.succ)
  (h_3 : (x x_1 : ℕ) → motive x x_1),
  (match 0, 1 with
    | 0, 1 => h_1 ()
    | i.succ, j.succ => h_2 i j
    | x, x_1 => h_3 x x_1) =
    h_1 ()
-- Init.Data.UInt.Lemmas
UInt64.ofNat_finVal : ∀ (n : Fin UInt64.size), UInt64.ofNat ↑n = UInt64.ofFin n
-- Mathlib.AlgebraicTopology.SimplicialSet.Degenerate
SSet.degenerate_le_preimage : ∀ {X Y : SSet} (f : X ⟶ Y) (n : ℕ),
  X.degenerate n ⊆ ⇑(CategoryTheory.ConcreteCategory.hom (f.app (Opposite.op { len := n }))) ⁻¹' Y.degenerate n
-- Mathlib.AlgebraicGeometry.OpenImmersion
AlgebraicGeometry.IsOpenImmersion.isPullback : ∀ {U V X Y : AlgebraicGeometry.Scheme} (g : U ⟶ V) (iU : U ⟶ X) (iV : V ⟶ Y) (f : X ⟶ Y)
  [inst : AlgebraicGeometry.IsOpenImmersion iU] [inst_1 : AlgebraicGeometry.IsOpenImmersion iV],
  CategoryTheory.CategoryStruct.comp iU f = CategoryTheory.CategoryStruct.comp g iV →
    (TopologicalSpace.Opens.map f.base).obj (AlgebraicGeometry.Scheme.Hom.opensRange iV) =
        AlgebraicGeometry.Scheme.Hom.opensRange iU →
      CategoryTheory.IsPullback g iU iV f