mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Combinatorics.Additive.Dissociation
Finset.subset_mulSpan : ∀ {α : Type u_1} [inst : CommGroup α] [inst_1 : DecidableEq α] [inst_2 : Fintype α] {s : Finset α}, s ⊆ s.mulSpan
-- Mathlib.Data.Sym.Sym2
Sym2.eq : ∀ {α : Type u_1} {a b c d : α}, s(a, b) = s(c, d) ↔ Sym2.Rel α (a, b) (c, d)
-- Std.Data.ExtTreeMap.Lemmas
Std.ExtTreeMap.getKey.congr_simp : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} [inst : Std.TransCmp cmp] (t t_1 : Std.ExtTreeMap α β cmp)
  (e_t : t = t_1) (a a_1 : α) (e_a : a = a_1) (h : a ∈ t), t.getKey a h = t_1.getKey a_1 ⋯
-- Mathlib.MeasureTheory.OuterMeasure.Induced
/-- The trimmed property of a measure μ states that `μ.toOuterMeasure.trim = μ.toOuterMeasure`.
This theorem shows that a restricted trimmed outer measure is a trimmed outer measure.  -/
MeasureTheory.OuterMeasure.restrict_trim : ∀ {α : Type u_1} [inst : MeasurableSpace α] {μ : MeasureTheory.OuterMeasure α} {s : Set α},
  MeasurableSet s → ((MeasureTheory.OuterMeasure.restrict s) μ).trim = (MeasureTheory.OuterMeasure.restrict s) μ.trim
-- Mathlib.Topology.Constructions.SumProd
/-- Four-way commutativity of the disjoint union. The name matches `add_add_add_comm`.  -/
Homeomorph.sumSumSumComm : (X : Type u) →
  (Y : Type v) →
    (W : Type u_1) →
      (Z : Type u_2) →
        [inst : TopologicalSpace X] →
          [inst_1 : TopologicalSpace Y] →
            [inst_2 : TopologicalSpace W] → [inst_3 : TopologicalSpace Z] → (X ⊕ Y) ⊕ W ⊕ Z ≃ₜ (X ⊕ W) ⊕ Y ⊕ Z
-- Mathlib.LinearAlgebra.BilinearForm.Properties
LinearMap.BilinForm.isNonneg_zero : ∀ {R : Type u_1} {M : Type u_2} [inst : CommSemiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M]
  [inst_3 : Preorder R], LinearMap.BilinForm.IsNonneg 0
-- Mathlib.Data.Stream.Init
Stream'.get_zero_iterate : ∀ {α : Type u} (f : α → α) (a : α), (Stream'.iterate f a).get 0 = a
-- Mathlib.Combinatorics.Enumerative.Schroder
Nat.largeSchroder.eq_2 : ∀ (n : ℕ), n.succ.largeSchroder = n.largeSchroder + ∑ i, (↑i).largeSchroder * (n - ↑i).largeSchroder
-- Mathlib.LinearAlgebra.TensorProduct.Associator
TensorProduct.rid_comm : ∀ {R : Type u_1} [inst : CommSemiring R] {M : Type u_5} [inst_1 : AddCommMonoid M] [inst_2 : Module R M]
  (x : TensorProduct R R M), (TensorProduct.rid R M) ((TensorProduct.comm R R M) x) = (TensorProduct.lid R M) x
-- Std.Time.Zoned.ZoneRules
Std.Time.TimeZone.ZoneRules.mk.sizeOf_spec : ∀ (initialLocalTimeType : Std.Time.TimeZone.LocalTimeType) (transitions : Array Std.Time.TimeZone.Transition)
  (transitionRule : Option Std.Time.TimeZone.RecurringRule),
  sizeOf
      { initialLocalTimeType := initialLocalTimeType, transitions := transitions, transitionRule := transitionRule } =
    1 + sizeOf initialLocalTimeType + sizeOf transitions + sizeOf transitionRule
-- Mathlib.CategoryTheory.Bicategory.Product
CategoryTheory.Bicategory.Prod.sectL_mapComp_inv : ∀ (B : Type u₁) [inst : CategoryTheory.Bicategory B] {C : Type u₂} [inst_1 : CategoryTheory.Bicategory C] (c : C)
  {a b c_1 : B} (f : a ⟶ b) (g : b ⟶ c_1),
  ((CategoryTheory.Bicategory.Prod.sectL B c).mapComp f g).inv =
    CategoryTheory.Prod.mkHom (CategoryTheory.CategoryStruct.id (CategoryTheory.CategoryStruct.comp f g))
      (CategoryTheory.Bicategory.rightUnitor (CategoryTheory.CategoryStruct.id c)).hom
-- Mathlib.CategoryTheory.Limits.Shapes.Opposites.Equalizers
CategoryTheory.Limits.parallelPairOpIso_hom_app_one : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {X Y : C} (f g : X ⟶ Y),
  (CategoryTheory.Limits.parallelPairOpIso f g).hom.app CategoryTheory.Limits.WalkingParallelPair.one =
    CategoryTheory.CategoryStruct.id
      ((CategoryTheory.Limits.parallelPair f.op g.op).obj CategoryTheory.Limits.WalkingParallelPair.one)
-- Mathlib.CategoryTheory.Shift.Adjunction
/-- The identity adjunction is compatible with the trivial `CommShift` structure on the
identity functor.
 -/
CategoryTheory.Adjunction.CommShift.instId : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] (A : Type u_3) [inst_1 : AddMonoid A]
  [inst_2 : CategoryTheory.HasShift C A], CategoryTheory.Adjunction.id.CommShift A
-- Mathlib.RingTheory.Localization.AsSubring
Localization.subalgebra.congr_simp : ∀ {A : Type u_1} (K : Type u_2) [inst : CommRing A] (S S_1 : Submonoid A) (e_S : S = S_1) [inst_1 : CommRing K]
  [inst_2 : Algebra A K] [inst_3 : IsFractionRing A K] (hS : S ≤ nonZeroDivisors A),
  Localization.subalgebra K S hS = Localization.subalgebra K S_1 ⋯
-- Mathlib.Algebra.Group.Action.Defs
AddDistribAddAction.ext_iff : ∀ {M : Type u_9} {N : Type u_10} {inst : AddMonoid M} {inst_1 : AddMonoid N} {x y : AddDistribAddAction M N},
  x = y ↔ VAdd.vadd = VAdd.vadd
-- Mathlib.Algebra.Homology.ShortComplex.RightHomology
CategoryTheory.ShortComplex.hasRightHomology_iff_unop : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  (S : CategoryTheory.ShortComplex Cᵒᵖ), S.HasRightHomology ↔ S.unop.HasLeftHomology
-- Mathlib.Algebra.Colimit.DirectLimit
DirectLimit.instAddGroup : {ι : Type u_2} →
  [inst : Preorder ι] →
    {G : ι → Type u_3} →
      {T : ⦃i j : ι⦄ → i ≤ j → Type u_6} →
        {f : (x x_1 : ι) → (h : x ≤ x_1) → T h} →
          [inst_1 : (i j : ι) → (h : i ≤ j) → FunLike (T h) (G i) (G j)] →
            [inst_2 : DirectedSystem G fun x1 x2 x3 => ⇑(f x1 x2 x3)] →
              [inst_3 : IsDirectedOrder ι] →
                [Nonempty ι] →
                  [inst_5 : (i : ι) → AddGroup (G i)] →
                    [∀ (i j : ι) (h : i ≤ j), AddMonoidHomClass (T h) (G i) (G j)] → AddGroup (DirectLimit G f)
-- Mathlib.MeasureTheory.Measure.Decomposition.RadonNikodym
MeasureTheory.Measure.inv_rnDeriv : ∀ {α : Type u_1} {m : MeasurableSpace α} {μ ν : MeasureTheory.Measure α} [MeasureTheory.SigmaFinite μ]
  [MeasureTheory.SigmaFinite ν], μ.AbsolutelyContinuous ν → (μ.rnDeriv ν)⁻¹ =ᵐ[μ] ν.rnDeriv μ
-- Mathlib.Algebra.Order.ToIntervalMod
toIocMod_add_left' : ∀ {α : Type u_1} [inst : AddCommGroup α] [inst_1 : LinearOrder α] [inst_2 : IsOrderedAddMonoid α] [hα : Archimedean α]
  {p : α} (hp : 0 < p) (a b : α), toIocMod hp (p + a) b = p + toIocMod hp a b
-- Mathlib.Algebra.Group.Submonoid.Operations
/-- For many categories (monoids, modules, rings, ...) the set-theoretic image of a morphism `f` is
a subobject of the codomain. When this is the case, it is useful to define the range of a morphism
in such a way that the underlying carrier set of the range subobject is definitionally
`Set.range f`. In particular this means that the types `↥(Set.range f)` and `↥f.range` are
interchangeable without proof obligations.

A convenient candidate definition for range which is mathematically correct is `map ⊤ f`, just as
`Set.range` could have been defined as `f '' Set.univ`. However, this lacks the desired definitional
convenience, in that it both does not match `Set.range`, and that it introduces a redundant `x ∈ ⊤`
term which clutters proofs. In such a case one may resort to the `copy`
pattern. A `copy` function converts the definitional problem for the carrier set of a subobject
into a one-off propositional proof obligation which one discharges while writing the definition of
the definitionally convenient range (the parameter `hs` in the example below).

A good example is the case of a morphism of monoids. A convenient definition for
`MonoidHom.mrange` would be `(⊤ : Submonoid M).map f`. However since this lacks the required
definitional convenience, we first define `Submonoid.copy` as follows:
```lean
protected def copy (S : Submonoid M) (s : Set M) (hs : s = S) : Submonoid M :=
  { carrier  := s,
    one_mem' := hs.symm ▸ S.one_mem',
    mul_mem' := hs.symm ▸ S.mul_mem' }
```
and then finally define:
```lean
def mrange (f : M →* N) : Submonoid N :=
  ((⊤ : Submonoid M).map f).copy (Set.range f) Set.image_univ.symm
```
 -/
LibraryNote.range_copy_pattern : Batteries.Util.LibraryNote
-- Mathlib.Tactic.NormNum.OfScientific
/-- The `norm_num` extension which identifies expressions in scientific notation, normalizing them
to rat casts if the scientific notation is inherited from the one for rationals.  -/
Mathlib.Meta.NormNum.evalOfScientific : Mathlib.Meta.NormNum.NormNumExt
-- Mathlib.Analysis.Calculus.AddTorsor.AffineMap
ContDiff.lineMap : ∀ {𝕜 : Type u_1} {V : Type u_2} {E : Type u_3} [inst : NontriviallyNormedField 𝕜] [inst_1 : NormedAddCommGroup V]
  [inst_2 : NormedSpace 𝕜 V] [inst_3 : NormedAddCommGroup E] [inst_4 : NormedSpace 𝕜 E] {f₁ f₂ : E → V} {g : E → 𝕜}
  {n : WithTop ℕ∞},
  ContDiff 𝕜 n f₁ → ContDiff 𝕜 n f₂ → ContDiff 𝕜 n g → ContDiff 𝕜 n fun x => (AffineMap.lineMap (f₁ x) (f₂ x)) (g x)
-- Mathlib.CategoryTheory.Bicategory.Adjunction.Mate
/-- Squares between left adjoints can be composed "vertically" by pasting.  -/
CategoryTheory.Bicategory.leftAdjointSquare.vcomp : {B : Type u} →
  [inst : CategoryTheory.Bicategory B] →
    {a b c d e f : B} →
      {g₁ : a ⟶ c} →
        {g₂ : c ⟶ e} →
          {h₁ : b ⟶ d} →
            {h₂ : d ⟶ f} →
              {l₁ : a ⟶ b} →
                {l₂ : c ⟶ d} →
                  {l₃ : e ⟶ f} →
                    (CategoryTheory.CategoryStruct.comp g₁ l₂ ⟶ CategoryTheory.CategoryStruct.comp l₁ h₁) →
                      (CategoryTheory.CategoryStruct.comp g₂ l₃ ⟶ CategoryTheory.CategoryStruct.comp l₂ h₂) →
                        (CategoryTheory.CategoryStruct.comp (CategoryTheory.CategoryStruct.comp g₁ g₂) l₃ ⟶
                          CategoryTheory.CategoryStruct.comp l₁ (CategoryTheory.CategoryStruct.comp h₁ h₂))
-- Mathlib.Analysis.Calculus.IteratedDeriv.Defs
/-- The `n`-th iterated derivative can be obtained by iterating `n` times the
differentiation operation.  -/
iteratedDeriv_eq_iterate : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {F : Type u_2} [inst_1 : NormedAddCommGroup F]
  [inst_2 : NormedSpace 𝕜 F] {n : ℕ} {f : 𝕜 → F}, iteratedDeriv n f = deriv^[n] f
-- Mathlib.AlgebraicTopology.SimplicialSet.HoFunctorMonoidal
SSet.Truncated.HomotopyCategory.instUniqueObjOppositeTruncatedTensorUnit : {n : ℕ} →
  (d : (SimplexCategory.Truncated n)ᵒᵖ) →
    Unique ((CategoryTheory.MonoidalCategoryStruct.tensorUnit (SSet.Truncated n)).obj d)
-- Mathlib.Tactic.NormNum.DivMod
/-- Given a result for evaluating `a b` in `ℤ` where `b > 0`, evaluate `a % b`.  -/
_private.Mathlib.Tactic.NormNum.DivMod.0.Mathlib.Meta.NormNum.evalIntMod.core : (a na : Q(ℤ)) →
  ℤ →
    Q(Mathlib.Meta.NormNum.IsInt «$a» «$na») →
      (b : Q(ℤ)) →
        (nb : Q(ℕ)) →
          Q(Mathlib.Meta.NormNum.IsNat «$b» «$nb») → (r : Q(ℕ)) × Q(Mathlib.Meta.NormNum.IsNat («$a» % «$b») «$r»)
-- Mathlib.CategoryTheory.Monoidal.Rigid.Basic
/-- The composition of right adjoint mates is the adjoint mate of the composition.  -/
CategoryTheory.comp_rightAdjointMate_assoc : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.MonoidalCategory C] {X Y Z : C}
  [inst_2 : CategoryTheory.HasRightDual X] [inst_3 : CategoryTheory.HasRightDual Y]
  [inst_4 : CategoryTheory.HasRightDual Z] {f : X ⟶ Y} {g : Y ⟶ Z} {Z_1 : C} (h : Xᘁ ⟶ Z_1),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.CategoryStruct.comp f gᘁ) h =
    CategoryTheory.CategoryStruct.comp (gᘁ) (CategoryTheory.CategoryStruct.comp (fᘁ) h)
-- Mathlib.SetTheory.Cardinal.Cofinality.Basic
/-- **Alias** of `OrderIso.lift_cof_congr`. -/
RelIso.cof_eq_lift : ∀ {α : Type u} {β : Type v} [inst : Preorder α] [inst_1 : Preorder β] (f : α ≃o β),
  Cardinal.lift.{v, u} (Order.cof α) = Cardinal.lift.{u, v} (Order.cof β)
-- Mathlib.Analysis.Normed.Group.Pointwise
ball_mul : ∀ {E : Type u_1} [inst : SeminormedCommGroup E] (δ : ℝ) (s : Set E) (x : E),
  Metric.ball x δ * s = x • Metric.thickening δ s
-- Mathlib.GroupTheory.MonoidLocalization.Maps
/-- Given a Localization map `f : M →* N` for a Submonoid `S`, we get an isomorphism between
the Localization of `M` at `S` as a quotient type and `N`.  -/
Localization.mulEquivOfQuotient : {M : Type u_1} →
  [inst : CommMonoid M] →
    {S : Submonoid M} → {N : Type u_2} → [inst_1 : CommMonoid N] → S.LocalizationMap N → Localization S ≃* N
-- Mathlib.Algebra.Order.BigOperators.Group.Finset
Fintype.prod_lt_one : ∀ {ι : Type u_1} {M : Type u_4} [inst : Fintype ι] [inst_1 : CommMonoid M] [inst_2 : PartialOrder M]
  [IsOrderedCancelMonoid M] {f : ι → M}, f < 1 → ∏ i, f i < 1
-- Mathlib.Analysis.CStarAlgebra.Classes
MulOpposite.instCommCStarAlgebra : {A : Type u_1} → [CommCStarAlgebra A] → CommCStarAlgebra Aᵐᵒᵖ
-- Lean.Expr
/-- Return the "body" of a forall expression.
Example: let `e` be the representation for `forall (p : Prop) (q : Prop), p ∧ q`, then
`getForallBody e` returns ``.app (.app (.const `And []) (.bvar 1)) (.bvar 0)``
 -/
Lean.Expr.getForallBody : Lean.Expr → Lean.Expr
-- Mathlib.CategoryTheory.Monoidal.Braided.Basic
CategoryTheory.BraidedCategory.hexagon_reverse_iso : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.MonoidalCategory C]
  [inst_2 : CategoryTheory.BraidedCategory C] (X Y Z : C),
  (CategoryTheory.MonoidalCategoryStruct.associator X Y Z).symm ≪≫
      β_ (CategoryTheory.MonoidalCategoryStruct.tensorObj X Y) Z ≪≫
        (CategoryTheory.MonoidalCategoryStruct.associator Z X Y).symm =
    CategoryTheory.MonoidalCategory.whiskerLeftIso X (β_ Y Z) ≪≫
      (CategoryTheory.MonoidalCategoryStruct.associator X Z Y).symm ≪≫
        CategoryTheory.MonoidalCategory.whiskerRightIso (β_ X Z) Y
-- Mathlib.RingTheory.Extension.Generators
Algebra.Generators.defaultHom_val : ∀ {R : Type u} {S : Type v} {ι : Type w} [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : Algebra R S]
  (P : Algebra.Generators R S ι) {R' : Type u_1} {S' : Type u_2} {ι' : Type u_3} [inst_3 : CommRing R']
  [inst_4 : CommRing S'] [inst_5 : Algebra R' S'] (P' : Algebra.Generators R' S' ι') [inst_6 : Algebra S S'] (a : ι),
  (P.defaultHom P').val a = (P'.σ ∘ ⇑(algebraMap S S') ∘ P.val) a
-- Mathlib.Tactic.ClickSuggestions.FindPremises
/-- Entries for the `rw` discrimination tree.  -/
_private.Mathlib.Tactic.ClickSuggestions.FindPremises.0.Mathlib.Tactic.ClickSuggestions.Entries.rw : Mathlib.Tactic.ClickSuggestions.Entries✝ →
  Array
    (Lean.Meta.RefinedDiscrTree.Key × Lean.Meta.RefinedDiscrTree.LazyEntry × Mathlib.Tactic.ClickSuggestions.RwLemma)
-- Mathlib.Analysis.SpecialFunctions.Log.ENNRealLogExp
EReal.tendsto_exp_nhds_top_nhds_top : Filter.Tendsto EReal.exp (nhds ⊤) (nhds ⊤)
-- Mathlib.Topology.MetricSpace.HausdorffDistance
/-- The Hausdorff distance is controlled by the diameter of the union.  -/
Metric.hausdorffEDist_le_ediam : ∀ {α : Type u} [inst : PseudoEMetricSpace α] {s t : Set α},
  s.Nonempty → t.Nonempty → Metric.hausdorffEDist s t ≤ Metric.ediam (s ∪ t)
-- Mathlib.Topology.UniformSpace.UniformConvergence
/-- An analogue of `Filter.HasBasis.tendsto_iff` for `TendstoUniformly`.  -/
Filter.HasBasis.tendstoUniformly_iff : ∀ {α : Type u_1} {β : Type u_2} [inst : UniformSpace β] {X : Type u_5} {ιX : Type u_6} {ιβ : Type u_8} {F : X → α → β}
  {f : α → β} {l : Filter X} {pX : ιX → Prop} {sX : ιX → Set X},
  l.HasBasis pX sX →
    ∀ {pβ : ιβ → Prop} {sβ : ιβ → Set (β × β)},
      (uniformity β).HasBasis pβ sβ →
        (TendstoUniformly F f l ↔ ∀ (i : ιβ), pβ i → ∃ j, pX j ∧ ∀ ⦃x : X⦄, x ∈ sX j → ∀ (a : α), (f a, F x a) ∈ sβ i)
-- Mathlib.Topology.FiberBundle.Trivialization
Bundle.Pretrivialization.ext : ∀ {B : Type u_1} {F : Type u_2} {Z : Type u_4} [inst : TopologicalSpace B] [inst_1 : TopologicalSpace F] {proj : Z → B}
  {e e' : Bundle.Pretrivialization F proj},
  (∀ (x : Z), ↑e x = ↑e' x) → (∀ (x : B × F), ↑e.symm x = ↑e'.symm x) → e.baseSet = e'.baseSet → e = e'
-- Mathlib.RingTheory.IntegralClosure.IsIntegral.Basic
RingHom.isIntegralElem_one : ∀ {R : Type u_1} {B : Type u_3} [inst : CommRing R] [inst_1 : Ring B] (f : R →+* B), f.IsIntegralElem 1
-- Mathlib.Data.Finset.Card
Finset.card_pos : ∀ {α : Type u_1} {s : Finset α}, 0 < s.card ↔ s.Nonempty
-- Mathlib.Probability.Kernel.Deterministic
ProbabilityTheory.Kernel.instIsDeterministicProdCopy : ∀ {α : Type u_1} {mα : MeasurableSpace α}, ProbabilityTheory.IsDeterministic (ProbabilityTheory.Kernel.copy α)
-- Mathlib.MeasureTheory.Function.LpSeminorm.Basic
MeasureTheory.eLpNorm_le_of_ae_enorm_bound : ∀ {α : Type u_1} {m0 : MeasurableSpace α} {p : ENNReal} {μ : MeasureTheory.Measure α} {ε : Type u_7}
  [inst : TopologicalSpace ε] [inst_1 : ESeminormedAddMonoid ε] {f : α → ε} {C : ENNReal},
  (∀ᵐ (x : α) ∂μ, ‖f x‖ₑ ≤ C) → MeasureTheory.eLpNorm f p μ ≤ C • μ Set.univ ^ p.toReal⁻¹
-- Mathlib.Algebra.Ring.ULift
ULift.commRing : {R : Type u} → [CommRing R] → CommRing (ULift.{u_1, u} R)
-- Aesop.Util.OrderedHashSet
Aesop.OrderedHashSet.mk.inj : ∀ {α : Type u_1} {inst : BEq α} {inst_1 : Hashable α} {toArray : Array α} {toHashSet : Std.HashSet α}
  {toArray_1 : Array α} {toHashSet_1 : Std.HashSet α},
  { toArray := toArray, toHashSet := toHashSet } = { toArray := toArray_1, toHashSet := toHashSet_1 } →
    toArray = toArray_1 ∧ toHashSet = toHashSet_1
-- Mathlib.Algebra.Order.Group.Synonym
ofDual_zero : ∀ {α : Type u_1} [inst : Zero α], OrderDual.ofDual 0 = 0
-- Mathlib.Computability.Ackermann
/-- The two-argument Ackermann function, defined so that

- `ack 0 n = n + 1`
- `ack (m + 1) 0 = ack m 1`
- `ack (m + 1) (n + 1) = ack m (ack (m + 1) n)`.

This is of interest as both a fast-growing function, and as an example of a recursive function that
isn't primitive recursive.  -/
ack : ℕ → ℕ → ℕ
-- Mathlib.Algebra.Group.Subgroup.Map
AddSubgroup.map_isAddCommutative : ∀ {G : Type u_1} {G' : Type u_2} [inst : AddGroup G] [inst_1 : AddGroup G'] (H : AddSubgroup G) (f : G →+ G')
  [IsAddCommutative ↥H], IsAddCommutative ↥(AddSubgroup.map f H)
-- Std.Data.TreeSet.Raw.Basic
/-- Tries to retrieve the smallest element that is less than the given element,
returning `none` if no such element exists.
 -/
Std.TreeSet.Raw.getLT? : {α : Type u} → {cmp : α → α → Ordering} → Std.TreeSet.Raw α cmp → α → Option α
-- Mathlib.Algebra.Order.Hom.MonoidWithZero
OrderMonoidIso.withZero_symm_apply_symm_apply : ∀ {G : Type u_6} {H : Type u_7} [inst : Group G] [inst_1 : PartialOrder G] [inst_2 : Group H] [inst_3 : PartialOrder H]
  (e : WithZero G ≃*o WithZero H) (x : H), (OrderMonoidIso.withZero.symm e).symm x = WithZero.unzero ⋯
-- Mathlib.RingTheory.Flat.TorsionFree
/-- Flat modules have no torsion.  -/
Module.Flat.torsion_eq_bot : ∀ {R : Type u_1} {M : Type u_2} [inst : CommRing R] [inst_1 : AddCommGroup M] [inst_2 : Module R M] [Module.Flat R M],
  Submodule.torsion R M = ⊥
-- Mathlib.CategoryTheory.Limits.Shapes.Biproducts
CategoryTheory.Limits.biproduct.isoProduct.eq_1 : ∀ {J : Type w} {C : Type u} [inst : CategoryTheory.Category.{v, u} C]
  [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C] (f : J → C) [inst_2 : CategoryTheory.Limits.HasBiproduct f],
  CategoryTheory.Limits.biproduct.isoProduct f =
    (CategoryTheory.Limits.biproduct.isLimit f).conePointUniqueUpToIso
      (CategoryTheory.Limits.limit.isLimit (CategoryTheory.Discrete.functor f))
-- Init.Data.Range.Polymorphic.UInt
UInt64.upwardEnumerableLE_ofBitVec : ∀ {x y : BitVec 64},
  Std.PRange.UpwardEnumerable.LE { toBitVec := x } { toBitVec := y } ↔ Std.PRange.UpwardEnumerable.LE x y
-- Mathlib.RingTheory.Coprime.Basic
/-- If a 2-vector `p` satisfies `IsCoprime (p 0) (p 1)`, then `p ≠ 0`.  -/
IsCoprime.ne_zero : ∀ {R : Type u} [inst : CommSemiring R] [Nontrivial R] {p : Fin 2 → R}, IsCoprime (p 0) (p 1) → p ≠ 0
-- Mathlib.Combinatorics.SimpleGraph.Extremal.TuranDensity
/-- `extremalNumber n H` is asymptotically equivalent to `turanDensity H * n.choose 2` as `n`
approaches `∞`.  -/
SimpleGraph.isEquivalent_extremalNumber : ∀ {W : Type u_1} {H : SimpleGraph W},
  H.turanDensity ≠ 0 →
    Asymptotics.IsEquivalent Filter.atTop (fun n => ↑(SimpleGraph.extremalNumber n H)) fun n =>
      H.turanDensity * ↑(n.choose 2)
-- Mathlib.Analysis.InnerProductSpace.Positive
LinearMap.IsPositive.nonneg_eigenvalues : ∀ {𝕜 : Type u_1} {E : Type u_2} [inst : RCLike 𝕜] [inst_1 : NormedAddCommGroup E] [inst_2 : InnerProductSpace 𝕜 E]
  [inst_3 : FiniteDimensional 𝕜 E] {T : E →ₗ[𝕜] E} {n : ℕ} (hT : T.IsPositive) (hn : Module.finrank 𝕜 E = n)
  (i : Fin n), 0 ≤ ⋯.eigenvalues hn i
-- Mathlib.CategoryTheory.Square
CategoryTheory.Square.flipFunctor_map_τ₄ : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {X Y : CategoryTheory.Square C} (φ : X ⟶ Y),
  (CategoryTheory.Square.flipFunctor.map φ).τ₄ = φ.τ₄
-- Init.Data.Vector.Lemmas
Vector.foldr_flatten : ∀ {α : Type u_1} {β : Type u_2} {m n : ℕ} {f : α → β → β} {b : β} {xss : Vector (Vector α m) n},
  Vector.foldr f b xss.flatten = Vector.foldr (fun xs b => Vector.foldr f b xs) b xss
-- Mathlib.Algebra.GroupWithZero.NonZeroDivisors
notMem_nonZeroDivisors_iff : ∀ {M₀ : Type u_2} [inst : MonoidWithZero M₀] {r : M₀},
  r ∉ nonZeroDivisors M₀ ↔ {s | r * s = 0 ∧ s ≠ 0}.Nonempty ∨ {s | s * r = 0 ∧ s ≠ 0}.Nonempty
-- Mathlib.AlgebraicTopology.FundamentalGroupoid.InducedMaps
/-- Proof that `H.evalAt x = H(0 ⟶ 1, x ⟶ x)`, with the appropriate casts  -/
ContinuousMap.Homotopy.evalAt_eq : ∀ {X Y : TopCat} {f g : C(↑X, ↑Y)} (H : f.Homotopy g) (x : ↑X),
  ⟦H.evalAt x⟧ =
    CategoryTheory.CategoryStruct.comp (ContinuousMap.Homotopy.hcast ⋯)
      (CategoryTheory.CategoryStruct.comp
        ((FundamentalGroupoid.fundamentalGroupoidFunctor.map (TopCat.ofHom H.uliftMap)).map
          (ContinuousMap.Homotopy.prodToProdTopI unitInterval.uhpath01
            (CategoryTheory.CategoryStruct.id (FundamentalGroupoid.fromTop x))))
        (ContinuousMap.Homotopy.hcast ⋯))
-- Mathlib.Control.Bifunctor
Function.bicompr.bifunctor : {F : Type u₀ → Type u₁ → Type u₂} →
  [Bifunctor F] → (G : Type u₂ → Type u_1) → [Functor G] → Bifunctor (Function.bicompr G F)
-- Init.Data.String.Lemmas.Iter
_private.Init.Data.String.Lemmas.Iter.0.Std.Iter.intercalateString.match_1.eq_1 : ∀ (motive : Option String → String → Sort u_1) (sl : String) (h_1 : (sl : String) → motive none sl)
  (h_2 : (str sl : String) → motive (some str) sl),
  (match none, sl with
    | none, sl => h_1 sl
    | some str, sl => h_2 str sl) =
    h_1 sl
-- Init.Data.Stream
ToStream : Type u_1 → outParam (Type u_1) → Type u_1
-- Mathlib.Order.Bounds.Image
/-- An antitone map sends a greatest element of a set to a least element of its image.  -/
Antitone.map_isGreatest : ∀ {α : Type u} {β : Type v} [inst : Preorder α] [inst_1 : Preorder β] {f : α → β},
  Antitone f → ∀ {a : α} {s : Set α}, IsGreatest s a → IsLeast (f '' s) (f a)
-- Mathlib.Analysis.Normed.Group.SemiNormedGrp
/-- The type of morphisms in `SemiNormedGrp₁`  -/
SemiNormedGrp₁.Hom : SemiNormedGrp₁ → SemiNormedGrp₁ → Type u
-- Mathlib.Geometry.Manifold.ContMDiff.NormedSpace
ContMDiff.clm_apply : ∀ {𝕜 : 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] {F₁ : Type u_8} [inst_6 : NormedAddCommGroup F₁]
  [inst_7 : NormedSpace 𝕜 F₁] {F₂ : Type u_9} [inst_8 : NormedAddCommGroup F₂] [inst_9 : NormedSpace 𝕜 F₂]
  {n : WithTop ℕ∞} {g : M → F₁ →L[𝕜] F₂} {f : M → F₁},
  ContMDiff I (modelWithCornersSelf 𝕜 (F₁ →L[𝕜] F₂)) n g →
    ContMDiff I (modelWithCornersSelf 𝕜 F₁) n f → ContMDiff I (modelWithCornersSelf 𝕜 F₂) n fun x => (g x) (f x)
-- Std.Data.HashMap.Lemmas
Std.HashMap.forM_eq_forM : ∀ {α : Type u} {β : Type v} {x : BEq α} {x_1 : Hashable α} {m : Std.HashMap α β} {m' : Type w → Type w'}
  [inst : Monad m'] [LawfulMonad m'] {f : α → β → m' PUnit.{w + 1}}, Std.HashMap.forM f m = forM m fun a => f a.1 a.2
-- Mathlib.Tactic.NormNum.Core
/-- Elaborator for `norm_num1` conv tactic.  -/
Mathlib.Tactic.elabNormNum1Conv : Lean.Elab.Tactic.Tactic
-- Mathlib.GroupTheory.SpecificGroups.Alternating
/-- The alternating group is the only subgroup of index 2 of the permutation group.  -/
Equiv.Perm.eq_alternatingGroup_of_index_eq_two : ∀ {α : Type u_1} [inst : Fintype α] [inst_1 : DecidableEq α] {G : Subgroup (Equiv.Perm α)},
  G.index = 2 → G = alternatingGroup α
-- Mathlib.Algebra.Module.LinearMap.FiniteRange
LinearMap.isQuasiInverse_congr : ∀ {K : Type u_1} {V₂ : Type u_4} {V₃ : Type u_6} [inst : CommRing K] [inst_1 : AddCommGroup V₂] [inst_2 : Module K V₂]
  [inst_3 : AddCommGroup V₃] [inst_4 : Module K V₃] {u u' : V₃ →ₗ[K] V₂} {v v' : V₂ →ₗ[K] V₃},
  u' ≈ u → v' ≈ v → (u.IsQuasiInverse v ↔ u'.IsQuasiInverse v')