mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.SetTheory.Cardinal.Cofinality.Club
IsClub.iInter : ∀ {α : Type v} [inst : LinearOrder α] [WellFoundedLT α] {ι : Type u} {f : ι → Set α},
  Order.cof α ≠ Cardinal.aleph0 →
    Cardinal.lift.{v, u} (Cardinal.mk ι) < Cardinal.lift.{u, v} (Order.cof α) →
      (∀ (i : ι), IsClub (f i)) → IsClub (⋂ i, f i)
-- Mathlib.RingTheory.Artinian.Module
/-- The prime spectrum is in bijection with the maximal spectrum.  -/
IsArtinianRing.primeSpectrumEquivMaximalSpectrum : {R : Type u_1} → [inst : CommRing R] → [IsArtinianRing R] → PrimeSpectrum R ≃ MaximalSpectrum R
-- Mathlib.Tactic.Linarith.Datatypes
Mathlib.Tactic.Linarith.GlobalPreprocessor.mk.sizeOf_spec : ∀ (toPreprocessorBase : Mathlib.Tactic.Linarith.PreprocessorBase)
  (transform : List Lean.Expr → Lean.MetaM (List Lean.Expr)),
  sizeOf { toPreprocessorBase := toPreprocessorBase, transform := transform } = 1 + sizeOf toPreprocessorBase
-- Mathlib.Analysis.Asymptotics.Defs
Asymptotics.IsBigO.congr : ∀ {α : Type u_1} {E : Type u_3} {F : Type u_4} [inst : Norm E] [inst_1 : Norm F] {l : Filter α} {f₁ f₂ : α → E}
  {g₁ g₂ : α → F}, f₁ =O[l] g₁ → (∀ (x : α), f₁ x = f₂ x) → (∀ (x : α), g₁ x = g₂ x) → f₂ =O[l] g₂
-- Mathlib.Algebra.Order.Group.Pointwise.Bounds
BddBelow.range_neg : ∀ {G : Type u_2} [inst : AddGroup G] [inst_1 : Preorder G] [AddLeftMono G] [AddRightMono G] {α : Type u_4} {f : α → G},
  BddBelow (Set.range f) → BddAbove (Set.range fun x => -f x)
-- Mathlib.Combinatorics.SimpleGraph.Subgraph
SimpleGraph.Subgraph.coeEmbeddingSpanningCoe_apply : ∀ {V : Type u} {G : SimpleGraph V} (G' : G.Subgraph) (self : { x // x ∈ G'.verts }),
  G'.coeEmbeddingSpanningCoe self = ↑self
-- Mathlib.Algebra.MonoidAlgebra.MapDomain
AddMonoidAlgebra.mapDomainAddEquiv_single : ∀ {R : Type u_3} {M : Type u_6} {N : Type u_7} [inst : Semiring R] [inst_1 : Add M] [inst_2 : Add N] (e : M ≃ N) (r : R)
  (m : M), (AddMonoidAlgebra.mapDomainAddEquiv R e) (AddMonoidAlgebra.single m r) = AddMonoidAlgebra.single (e m) r
-- Mathlib.RingTheory.TotallySplit
/-- `S` is a finite, totally split `R`-algebra if `S` is isomorphic to `Fin n → R` for some `n`.
Geometrically, this is a trivial cover of degree `n`.  -/
Algebra.IsFiniteSplit : (R : Type u_1) → (S : Type u_2) → [inst : CommRing R] → [inst_1 : CommRing S] → [Algebra R S] → Prop
-- Mathlib.Topology.ContinuousMap.CompactlySupported
/-- The compactly supported continuous `ℝ≥0`-valued function as a compactly supported `ℝ`-valued
function.  -/
CompactlySupportedContinuousMap.toReal : {α : Type u_2} →
  [inst : TopologicalSpace α] → CompactlySupportedContinuousMap α NNReal → CompactlySupportedContinuousMap α ℝ
-- Mathlib.Tactic.Translate.Reorder
/-- The reordering of universe levels.  -/
Mathlib.Tactic.Translate.Reorder.univReorder : Mathlib.Tactic.Translate.Reorder → Mathlib.Tactic.Translate.Permutation
-- Init.Data.Iterators.Lemmas.Combinators.FilterMap
Std.Iter.step_map : ∀ {α β γ : Type w} [inst : Std.Iterator α Id β] {it : Std.Iter β} {f : β → γ},
  (Std.Iter.map f it).step =
    match it.step with
    | ⟨Std.IterStep.yield it' out, h⟩ => Std.PlausibleIterStep.yield (Std.Iter.map f it') (f out) ⋯
    | ⟨Std.IterStep.skip it', h⟩ => Std.PlausibleIterStep.skip (Std.Iter.map f it') ⋯
    | ⟨Std.IterStep.done, h⟩ => Std.PlausibleIterStep.done ⋯
-- Batteries.Data.List.Lemmas
List.getElem_idxOfNth_eq : ∀ {α : Type u_1} {x : α} {n : ℕ} {xs : List α} [inst : BEq α] [LawfulBEq α] {h : List.idxOfNth x xs n < xs.length},
  xs[List.idxOfNth x xs n] = x
-- Mathlib.Analysis.Calculus.FDeriv.Congr
HasFDerivWithinAt.congr : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : AddCommGroup E] [inst_2 : Module 𝕜 E]
  [inst_3 : TopologicalSpace E] {F : Type u_3} [inst_4 : AddCommGroup F] [inst_5 : Module 𝕜 F]
  [inst_6 : TopologicalSpace F] {f f₁ : E → F} {f' : E →L[𝕜] F} {x : E} {s : Set E},
  HasFDerivWithinAt f f' s x → Set.EqOn f₁ f s → f₁ x = f x → HasFDerivWithinAt f₁ f' s x
-- Mathlib.Probability.Distributions.Poisson.PoissonLimitThm
/-- Another version of Poisson Limit Theorem: convergence of `PMF.binomial` to `poissonPMF` in `ℝ≥0∞`
under the natural hypotheses (`∀ n, p n ≤ 1` and `r ≥ 0`).
 -/
ProbabilityTheory.binomial_tendsto_poissonPMFReal_atTop : ∀ (k : ℕ) {r : NNReal} {p : ℕ → ↑unitInterval},
  Filter.Tendsto (fun n => ↑n * ↑(p n)) Filter.atTop (nhds ↑r) →
    Filter.Tendsto (fun n => (ProbabilityTheory.binomial n (p n)) {k}) Filter.atTop
      (nhds ((ProbabilityTheory.poissonMeasure r) {k}))
-- Mathlib.Algebra.QuadraticAlgebra.NormDeterminant
/-- The norm of an element in a quadratic algebra is the determinant of the endomorphism defined by
left multiplication by that element.  -/
QuadraticAlgebra.det_toLinearMap_eq_norm : ∀ {R : Type u_1} [inst : CommRing R] {a b : R} (z : QuadraticAlgebra R a b),
  LinearMap.det (DistribSMul.toLinearMap R (QuadraticAlgebra R a b) z) = QuadraticAlgebra.norm z
-- Mathlib.CategoryTheory.Bicategory.NaturalTransformation.Lax
/-- The underlying lax natural transformation of a strong natural transformation.  -/
CategoryTheory.Lax.StrongTrans.toLax : {B : Type u₁} →
  [inst : CategoryTheory.Bicategory B] →
    {C : Type u₂} →
      [inst_1 : CategoryTheory.Bicategory C] →
        {F G : CategoryTheory.LaxFunctor B C} → CategoryTheory.Lax.StrongTrans F G → CategoryTheory.Lax.LaxTrans F G
-- Mathlib.Tactic.Translate.Core
_private.Mathlib.Tactic.Translate.Core.0.Mathlib.Tactic.Translate.targetName.translateNamespace : Mathlib.Tactic.Translate.TranslateData → Lean.Environment → Lean.Name → Lean.Name
-- Mathlib.LinearAlgebra.Projectivization.Subspace
Projectivization.lift.congr_simp : ∀ {K : Type u_1} {V : Type u_2} [inst : DivisionRing K] [inst_1 : AddCommGroup V] [inst_2 : Module K V] {α : Type u_3}
  (f f_1 : { v // v ≠ 0 } → α) (e_f : f = f_1) (hf : ∀ (a b : { v // v ≠ 0 }) (t : K), ↑a = t • ↑b → f a = f b)
  (x x_1 : Projectivization K V), x = x_1 → Projectivization.lift f hf x = Projectivization.lift f_1 ⋯ x_1
-- Mathlib.Algebra.SkewMonoidAlgebra.Basic
/-- If two additive homomorphisms from `SkewMonoidAlgebra k G ` are equal on each `single a b`,
then they are equal.  -/
SkewMonoidAlgebra.addHom_ext : ∀ {k : Type u_1} {G : Type u_2} [inst : AddCommMonoid k] {M : Type u_3} [inst_1 : AddZeroClass M]
  {f g : SkewMonoidAlgebra k G →+ M},
  (∀ (a : G) (b : k), f (SkewMonoidAlgebra.single a b) = g (SkewMonoidAlgebra.single a b)) → f = g
-- Mathlib.NumberTheory.ModularForms.CongruenceSubgroups
CongruenceSubgroup.Gamma1_mem' : ∀ {N : ℕ} {γ : ↥(CongruenceSubgroup.Gamma0 N)},
  γ ∈ CongruenceSubgroup.Gamma1' N ↔ (CongruenceSubgroup.Gamma0Map N) γ = 1
-- Std.Data.HashMap.Lemmas
Std.HashMap.keys_insertIfNew_perm : ∀ {α : Type u} {β : Type v} {x : BEq α} {x_1 : Hashable α} {m : Std.HashMap α β} [EquivBEq α] [LawfulHashable α] {k : α}
  {v : β}, (m.insertIfNew k v).keys.Perm (if k ∈ m then m.keys else k :: m.keys)
-- Mathlib.Analysis.Normed.Group.Seminorm
GroupSeminorm.comp_mono : ∀ {E : Type u_3} {F : Type u_4} [inst : Group E] [inst_1 : Group F] {p q : GroupSeminorm E} (f : F →* E),
  p ≤ q → p.comp f ≤ q.comp f
-- Mathlib.Control.Bitraversable.Instances
Bitraversable.flip : {t : Type u → Type u → Type u} → [Bitraversable t] → Bitraversable (flip t)
-- Mathlib.Algebra.Order.Archimedean.Class
MulArchimedeanClass.mk_mul_lt_mk_left_iff : ∀ {M : Type u_1} [inst : CommGroup M] [inst_1 : LinearOrder M] [inst_2 : IsOrderedMonoid M] {a b : M},
  MulArchimedeanClass.mk (a * b) < MulArchimedeanClass.mk a ↔ MulArchimedeanClass.mk b < MulArchimedeanClass.mk a
-- Mathlib.CategoryTheory.Monoidal.Category
CategoryTheory.MonoidalCategory.leftUnitorNatIso_hom_app : ∀ (C : Type u) [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.MonoidalCategory C] (X : C),
  (CategoryTheory.MonoidalCategory.leftUnitorNatIso C).hom.app X =
    (CategoryTheory.MonoidalCategoryStruct.leftUnitor X).hom
-- Mathlib.Data.List.Monad
List.instMonad : Monad List
-- Mathlib.RingTheory.AdicCompletion.Functoriality
AdicCompletion.piEquivOfFintype.eq_1 : ∀ {R : Type u_1} [inst : CommRing R] (I : Ideal R) {ι : Type u_6} (M : ι → Type u_7)
  [inst_1 : (i : ι) → AddCommGroup (M i)] [inst_2 : (i : ι) → Module R (M i)] [inst_3 : DecidableEq ι]
  [inst_4 : Fintype ι],
  AdicCompletion.piEquivOfFintype I M =
    (AdicCompletion.congr I (DirectSum.linearEquivFunOnFintype R ι M)).symm.trans
      ((AdicCompletion.sumEquivOfFintype I M).symm.trans
        (DirectSum.linearEquivFunOnFintype (AdicCompletion I R) ι fun j => AdicCompletion I (M j)))
-- Mathlib.LinearAlgebra.RootSystem.Defs
RootPairing.flip_coroot : ∀ {ι : 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),
  P.flip.coroot = P.root
-- Mathlib.Data.ENNReal.Basic
ENNReal.coe_mono : Monotone ENNReal.ofNNReal
-- Lean.Meta.Sym.SymM
/-- Applies hash-consing to `e`. Recall that all expressions in a `grind` goal have
been hash-consed. We perform this step before we internalize expressions.

This function does not try to `unfoldReducible` and `foldProjs` like `shareCommon`.
`cache` may contain the results accumulated by a run of `shareCommon` that was
interrupted by a check violation; see `repairAndShare`.
 -/
Lean.Meta.Sym.shareCommonWithoutChecks : Lean.Expr → optParam Lean.Meta.Sym.AlphaShareCommon.Cache ∅ → Lean.Meta.Sym.SymM Lean.Expr
-- Mathlib.CategoryTheory.Limits.Creates
CategoryTheory.CreatesLimitsOfShape.mk : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    {D : Type u₂} →
      [inst_1 : CategoryTheory.Category.{v₂, u₂} D] →
        {J : Type w} →
          [inst_2 : CategoryTheory.Category.{w', w} J] →
            {F : CategoryTheory.Functor C D} →
              autoParam ({K : CategoryTheory.Functor J C} → CategoryTheory.CreatesLimit K F)
                  CategoryTheory.CreatesLimitsOfShape.CreatesLimit._autoParam →
                CategoryTheory.CreatesLimitsOfShape J F
-- Std.Data.ExtTreeMap.Lemmas
Std.ExtTreeMap.getElem!_eq_default_of_contains_eq_false : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Std.ExtTreeMap α β cmp} [inst : Std.TransCmp cmp]
  [inst_1 : Inhabited β] {a : α}, t.contains a = false → t[a]! = default
-- Init.Data.ByteArray.Basic
/-- Moves the iterator's position forward by one byte. - -/
ByteArray.Iterator.next' : (it : ByteArray.Iterator) → it.hasNext = true → ByteArray.Iterator
-- Mathlib.Probability.Kernel.Composition.MapComap
ProbabilityTheory.Kernel.mapOfMeasurable_eq_map : ∀ {α : Type u_1} {β : Type u_2} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} {γ : Type u_4}
  {mγ : MeasurableSpace γ} (κ : ProbabilityTheory.Kernel α β) {f : β → γ} (hf : Measurable f),
  κ.mapOfMeasurable f hf = κ.map f
-- Mathlib.NumberTheory.NumberField.CanonicalEmbedding.Basic
NumberField.mixedEmbedding.eq_1 : ∀ (K : Type u_1) [inst : Field K],
  NumberField.mixedEmbedding K =
    (RingHom.pi fun w => NumberField.InfinitePlace.embedding_of_isReal ⋯).prod (RingHom.pi fun w => (↑w).embedding)
-- Mathlib.Algebra.Group.Action.End
MulDistribMulAction.toMulEquiv_apply : ∀ {G : Type u_1} (M : Type u_2) [inst : Group G] [inst_1 : Monoid M] [inst_2 : MulDistribMulAction G M] (x : G) (a : M),
  (MulDistribMulAction.toMulEquiv M x) a = x • a
-- Std.Data.HashMap.Lemmas
Std.HashMap.getKeyD_diff_of_mem_right : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} {β : Type v} {m₁ m₂ : Std.HashMap α β} [EquivBEq α] [LawfulHashable α]
  {k fallback : α}, k ∈ m₂ → (m₁ \ m₂).getKeyD k fallback = fallback
-- Mathlib.Analysis.SpecialFunctions.Pow.NNReal
NNReal.rpow_inv_le_iff : ∀ {x y : NNReal} {z : ℝ}, 0 < z → (x ^ z⁻¹ ≤ y ↔ x ≤ y ^ z)
-- Mathlib.Topology.CWComplex.Classical.Basic
Topology.RelCWComplex.union_iUnion_openCell_eq_complex : ∀ {X : Type u_1} [t : TopologicalSpace X] {C D : Set X} [inst : Topology.RelCWComplex C D],
  D ∪ ⋃ n, ⋃ j, Topology.RelCWComplex.openCell n j = C
-- Mathlib.Topology.Algebra.Monoid
separatelyContinuousMul_induced : ∀ {M : Type u_6} {N : Type u_7} {F : Type u_8} [inst : Mul M] [inst_1 : Mul N] [inst_2 : FunLike F M N]
  [MulHomClass F M N] [inst_4 : TopologicalSpace N] [SeparatelyContinuousMul N] (f : F), SeparatelyContinuousMul M
-- Mathlib.Topology.Homeomorph.Defs
/-- An inducing equiv between topological spaces is a homeomorphism.  -/
Equiv.toHomeomorphOfIsInducing : {X : Type u_1} →
  {Y : Type u_2} →
    [inst : TopologicalSpace X] → [inst_1 : TopologicalSpace Y] → (f : X ≃ Y) → Topology.IsInducing ⇑f → X ≃ₜ Y
-- Mathlib.Algebra.Module.ZLattice.Basic
instModuleFinite_of_discrete_submodule : ∀ {E : Type u_3} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] [FiniteDimensional ℝ E] (L : Submodule ℤ E)
  [DiscreteTopology ↥L], Module.Finite ℤ ↥L
-- Mathlib.Analysis.Complex.BorelCaratheodory
/-- Application of the Schwarz lemma to the transformed function. If `f` is differentiable on
the ball, maps into `{z | z.re ≤ M}`, and satisfies `f 0 = 0`, then the Schwarz transform
satisfies the bound from the Schwarz lemma.  -/
_private.Mathlib.Analysis.Complex.BorelCaratheodory.0.Complex.schwarz_applied : ∀ {f : ℂ → ℂ} {M R : ℝ} {z : ℂ},
  0 < M →
    DifferentiableOn ℂ f (Metric.ball 0 R) →
      Set.MapsTo f (Metric.ball 0 R) {z | z.re ≤ M} →
        z ∈ Metric.ball 0 R → f 0 = 0 → ‖f z / (2 * ↑M - f z)‖ ≤ 1 / R * ‖z‖
-- Lean.Data.Iterators.Producers.PersistentHashMap
Lean.PersistentHashMap.Zipper.brecOn.eq : ∀ {α : Type u} {β : Type v} {motive : Lean.PersistentHashMap.Zipper α β → Sort u_1}
  (t : Lean.PersistentHashMap.Zipper α β)
  (F_1 : (t : Lean.PersistentHashMap.Zipper α β) → Lean.PersistentHashMap.Zipper.below t → motive t),
  Lean.PersistentHashMap.Zipper.brecOn t F_1 = F_1 t (Lean.PersistentHashMap.Zipper.brecOn.go t F_1).2
-- Mathlib.CategoryTheory.Limits.Shapes.Kernels
CategoryTheory.Limits.cokernelIsoOfEq_refl : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C] {X Y : C}
  (f : X ⟶ Y) [inst_2 : CategoryTheory.Limits.HasCokernel f] {h : f = f},
  CategoryTheory.Limits.cokernelIsoOfEq h = CategoryTheory.Iso.refl (CategoryTheory.Limits.cokernel f)
-- Mathlib.Analysis.Complex.Trigonometric
Real.abs_sin_le_one : ∀ (x : ℝ), |Real.sin x| ≤ 1
-- Mathlib.Logic.Equiv.Sum
Equiv.sumAssoc_symm_apply_inl : ∀ {α : Type u_9} {β : Type u_10} {γ : Type u_11} (a : α), (Equiv.sumAssoc α β γ).symm (Sum.inl a) = Sum.inl (Sum.inl a)
-- Mathlib.RingTheory.Derivation.Basic
Derivation.instSub : {R : Type u_1} →
  [inst : CommRing R] →
    {A : Type u_2} →
      [inst_1 : CommRing A] →
        [inst_2 : Algebra R A] →
          {M : Type u_3} →
            [inst_3 : AddCommGroup M] → [inst_4 : Module A M] → [inst_5 : Module R M] → Sub (Derivation R A M)
-- Mathlib.Analysis.Normed.Module.Bases
/-- The sequence of candidate basis vectors.  -/
SchauderBasis.RankOneDecomposition.e : {𝕜 : Type u_1} →
  [inst : NontriviallyNormedField 𝕜] →
    {X : Type u_2} →
      [inst_1 : NormedAddCommGroup X] → [inst_2 : NormedSpace 𝕜 X] → SchauderBasis.RankOneDecomposition 𝕜 X → ℕ → X
-- Mathlib.CategoryTheory.Sites.Descent.DescentDataAsCoalgebra
CategoryTheory.Pseudofunctor.DescentDataAsCoalgebra.coalgebraEquivalence_functor_obj_A : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C]
  (F :
    CategoryTheory.Pseudofunctor (CategoryTheory.LocallyDiscrete Cᵒᵖ)
      (CategoryTheory.Bicategory.Adj CategoryTheory.Cat))
  (ι : Type u_1) [inst_1 : Unique ι] {X S : C} (f : X ⟶ S) (D : F.DescentDataAsCoalgebra fun x => f),
  ((CategoryTheory.Pseudofunctor.DescentDataAsCoalgebra.coalgebraEquivalence F ι f).functor.obj D).A = D.obj default
-- Mathlib.CategoryTheory.Localization.CalculusOfFractions.Fractions
/-- the numerator of the first left fraction  -/
CategoryTheory.MorphismProperty.LeftFraction₃.f : {C : Type u_1} →
  [inst : CategoryTheory.Category.{v_1, u_1} C] →
    {W : CategoryTheory.MorphismProperty C} → {X Y : C} → (self : W.LeftFraction₃ X Y) → X ⟶ self.Y'
-- Mathlib.Data.Stream.Init
Stream'.mem_cycle : ∀ {α : Type u} {a : α} {l : List α} (h : l ≠ []), a ∈ l → a ∈ Stream'.cycle l h
-- Mathlib.NumberTheory.SelbergSieve
_private.Mathlib.NumberTheory.SelbergSieve.0.BoundingSieve.sum_divisors_lambda_sq_larger_sum : ∀ (f : ℕ → ℕ → ℕ → ℝ) (n : ℕ),
  (∑ d ∈ n.divisors, ∑ d1 ∈ d.divisors, ∑ d2 ∈ d.divisors, if d = d1.lcm d2 then f d1 d2 d else 0) =
    ∑ d ∈ n.divisors, ∑ d1 ∈ n.divisors, ∑ d2 ∈ n.divisors, if d = d1.lcm d2 then f d1 d2 d else 0
-- Mathlib.Data.PFunctor.Univariate.M
PFunctor.Approx.agree_trivial : ∀ {F : PFunctor.{uA, uB}} {x : PFunctor.Approx.CofixA F 0} {y : PFunctor.Approx.CofixA F 1}, PFunctor.Approx.Agree x y
-- Mathlib.GroupTheory.Order.Min
ZMod.minOrder : ∀ {n : ℕ}, n ≠ 0 → n ≠ 1 → AddMonoid.minOrder (ZMod n) = ↑n.minFac
-- Mathlib.Data.Int.Cast.Defs
AddGroupWithOne.sub_eq_add_neg : ∀ {R : Type u} [self : AddGroupWithOne R] (a b : R), a - b = a + -b
-- Mathlib.Dynamics.PeriodicPts.Defs
Function.iterate_mod_minimalPeriod_eq : ∀ {α : Type u_1} {f : α → α} {x : α} {n : ℕ}, f^[n % Function.minimalPeriod f x] x = f^[n] x
-- Mathlib.ModelTheory.Complexity
FirstOrder.Language.BoundedFormula.not_all_isAtomic : ∀ {L : FirstOrder.Language} {α : Type u'} {n : ℕ} (φ : L.BoundedFormula α (n + 1)), ¬φ.all.IsAtomic
-- Mathlib.Topology.Category.LightProfinite.Basic
lightProfiniteToLightDiagram_map : ∀ {X Y : LightProfinite} (f : X ⟶ Y),
  lightProfiniteToLightDiagram.map f = CategoryTheory.InducedCategory.homMk (CategoryTheory.InducedCategory.homMk f.hom)
-- Mathlib.Data.List.Nodup
List.Nodup.prefix_of_head_mem_of_infix : ∀ {α : Type u} {l₁ l₂ : List α}, l₁ <:+: l₂ → ∀ {hne : l₂ ≠ []}, l₂.head hne ∈ l₁ → l₂.Nodup → l₁ <+: l₂
-- Mathlib.Algebra.Group.Subgroup.Lattice
Subgroup.toAddSubgroup'_closure : ∀ {A : Type u_2} [inst : AddGroup A] (S : Set (Multiplicative A)),
  Subgroup.toAddSubgroup' (Subgroup.closure S) = AddSubgroup.closure (⇑Multiplicative.ofAdd ⁻¹' S)
-- Std.Http.Data.URI.Parser
/-- Parses a URI path with combined parsing and validation.
 -/
Std.Http.URI.Parser.parsePath : Std.Http.URI.Config → Bool → Bool → Std.Internal.Parsec.ByteArray.Parser Std.Http.URI.Path
-- Mathlib.MeasureTheory.Measure.Haar.Basic
MeasureTheory.Measure.haar.addPrehaar_nonneg : ∀ {G : Type u_1} [inst : AddGroup G] [inst_1 : TopologicalSpace G] (K₀ : TopologicalSpace.PositiveCompacts G)
  {U : Set G} (K : TopologicalSpace.Compacts G), 0 ≤ MeasureTheory.Measure.haar.addPrehaar (↑K₀) U K
-- Mathlib.CategoryTheory.Shift.Localization
CategoryTheory.Localization.liftNatIso.congr_simp : ∀ {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)
  (W : CategoryTheory.MorphismProperty C) {E : Type u_3} [inst_2 : CategoryTheory.Category.{v_3, u_3} E]
  [inst_3 : L.IsLocalization W] (F₁ F₂ : CategoryTheory.Functor C E) (F₁' F₂' : CategoryTheory.Functor D E)
  [h₁ : CategoryTheory.Localization.Lifting L W F₁ F₁'] [h₂ : CategoryTheory.Localization.Lifting L W F₂ F₂']
  (e e_1 : F₁ ≅ F₂),
  e = e_1 →
    CategoryTheory.Localization.liftNatIso L W F₁ F₂ F₁' F₂' e =
      CategoryTheory.Localization.liftNatIso L W F₁ F₂ F₁' F₂' e_1
-- Mathlib.Algebra.Homology.HomologySequence
HomologicalComplex.HomologySequence.instEpiMap'ComposableArrows₃OfNatNat : ∀ {C : Type u_1} {ι : Type u_2} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Preadditive C]
  {c : ComplexShape ι} (K : HomologicalComplex C c) (i j : ι) [inst_2 : K.HasHomology i] [inst_3 : K.HasHomology j],
  CategoryTheory.Epi
    ((HomologicalComplex.HomologySequence.composableArrows₃ K i j).map' 2 3
      HomologicalComplex.HomologySequence.instEpiMap'ComposableArrows₃OfNatNat._proof_2
      HomologicalComplex.HomologySequence.instEpiMap'ComposableArrows₃OfNatNat._proof_3)
-- Std.Data.ExtTreeMap.Basic
/-- Updates the values of the map by applying the given function to all mappings.  -/
Std.ExtTreeMap.map : {α : Type u} →
  {β : Type v} → {γ : Type w} → {cmp : α → α → Ordering} → (α → β → γ) → Std.ExtTreeMap α β cmp → Std.ExtTreeMap α γ cmp
-- Mathlib.RingTheory.LocalRing.ResidueField.Fiber
/-- The fiber `PrimeSpectrum S → PrimeSpectrum R` at a prime ideal
`p : PrimeSpectrum R` is in bijection with the prime spectrum of `κ(p) ⊗[R] S`.  -/
PrimeSpectrum.preimageEquivFiber : (R : Type u_1) →
  (S : Type u_2) →
    [inst : CommRing R] →
      [inst_1 : CommRing S] →
        [inst_2 : Algebra R S] →
          (p : PrimeSpectrum R) → ↑(PrimeSpectrum.comap (algebraMap R S) ⁻¹' {p}) ≃ PrimeSpectrum (p.asIdeal.Fiber S)
-- Mathlib.RepresentationTheory.Homological.GroupHomology.Functoriality
groupHomology.mapIso_inv : ∀ {k G H : Type u} [inst : CommRing k] [inst_1 : Group G] [inst_2 : Group H] {A : Rep.{u, u, u} k G}
  {B : Rep.{u, u, u} k H} (e : G ≃* H) (e' : ↑A ≃ₗ[k] ↑B) (he : ∀ (g : G), ↑e' ∘ₗ A.ρ g = B.ρ (e g) ∘ₗ ↑e') (n : ℕ),
  (groupHomology.mapIso e e' he n).inv =
    groupHomology.map (↑e.symm) (Rep.ofHom { toLinearMap := ↑e'.symm, isIntertwining' := ⋯ }) n
-- Mathlib.AlgebraicGeometry.EllipticCurve.Weierstrass
WeierstrassCurve.map_a₃ : ∀ {R : Type u} [inst : CommRing R] (W : WeierstrassCurve R) {A : Type v} [inst_1 : CommRing A] (f : R →+* A),
  (W.map f).a₃ = f W.a₃
-- Init.Data.String.Pattern.String
_private.Init.Data.String.Pattern.String.0.String.Slice.Pattern.ForwardSliceSearcher.instIteratorIdSearchStep.match_1.eq_3 : ∀ (s : String.Slice) (motive : String.Slice.Pattern.ForwardSliceSearcher s → Sort u_1) (needle : String.Slice)
  (table : Vector ℕ needle.utf8ByteSize) (ht : table = String.Slice.Pattern.ForwardSliceSearcher.buildTable needle)
  (stackPos needlePos : String.Pos.Raw) (hn : needlePos < needle.rawEndPos)
  (h_1 : (pos : s.Pos) → motive (String.Slice.Pattern.ForwardSliceSearcher.emptyBefore pos))
  (h_2 : (pos : s.Pos) → (h : pos ≠ s.endPos) → motive (String.Slice.Pattern.ForwardSliceSearcher.emptyAt pos h))
  (h_3 :
    (needle : String.Slice) →
      (table : Vector ℕ needle.utf8ByteSize) →
        (ht : table = String.Slice.Pattern.ForwardSliceSearcher.buildTable needle) →
          (stackPos needlePos : String.Pos.Raw) →
            (hn : needlePos < needle.rawEndPos) →
              motive (String.Slice.Pattern.ForwardSliceSearcher.proper needle table ht stackPos needlePos hn))
  (h_4 : Unit → motive String.Slice.Pattern.ForwardSliceSearcher.atEnd),
  (match String.Slice.Pattern.ForwardSliceSearcher.proper needle table ht stackPos needlePos hn with
    | String.Slice.Pattern.ForwardSliceSearcher.emptyBefore pos => h_1 pos
    | String.Slice.Pattern.ForwardSliceSearcher.emptyAt pos h => h_2 pos h
    | String.Slice.Pattern.ForwardSliceSearcher.proper needle table ht stackPos needlePos hn =>
      h_3 needle table ht stackPos needlePos hn
    | String.Slice.Pattern.ForwardSliceSearcher.atEnd => h_4 ()) =
    h_3 needle table ht stackPos needlePos hn
-- Mathlib.CategoryTheory.Idempotents.HomologicalComplex
CategoryTheory.Idempotents.KaroubiHomologicalComplexEquivalence.unitIso_inv_app_f_f : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Preadditive C] {ι : Type u_2}
  {c : ComplexShape ι} (P : CategoryTheory.Idempotents.Karoubi (HomologicalComplex C c)) (n : ι),
  (CategoryTheory.Idempotents.KaroubiHomologicalComplexEquivalence.unitIso.inv.app P).f.f n = P.p.f n
-- Mathlib.Data.Tree.Basic
BinaryTree.node : {α : Type u} → α → BinaryTree α → BinaryTree α → BinaryTree α
-- Mathlib.Control.Traversable.Lemmas
sequence.eq_1 : ∀ {t : Type u → Type u} {α : Type u} {f : Type u → Type u} [inst : Applicative f] [inst_1 : Traversable t],
  sequence = traverse id
-- Mathlib.AlgebraicTopology.ModelCategory.Bifibrant
HomotopicalAlgebra.CofibrantObject.instIsCofibrantObjCofibrantObjects : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : HomotopicalAlgebra.CategoryWithCofibrations C]
  [inst_2 : CategoryTheory.Limits.HasInitial C] (X : HomotopicalAlgebra.CofibrantObject C),
  HomotopicalAlgebra.IsCofibrant X.obj
-- Batteries.Data.BinomialHeap.Basic
Batteries.BinomialHeap.Imp.Heap.realSize.eq_1 : ∀ {α : Type u_1}, Batteries.BinomialHeap.Imp.Heap.nil.realSize = 0