mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Tactic.Linter.Whitespace
/-- The `whitespace` linter emits a warning if
* either a command does not start at the beginning of a line;
* or the "hypotheses segment" of a declaration does not coincide with its pretty-printed version.

In practice, this makes sure that the spacing in a typical declaration looks like
```lean
example (a : Nat) {R : Type} [Add R] : <not linted part>
```
as opposed to
```lean
example (a: Nat) {R:Type}  [Add  R] : <not linted part>
```
 -/
_private.Mathlib.Tactic.Linter.Whitespace.0.Mathlib.Linter.Style.Whitespace.whitespaceLinter : Lean.Linter
-- Init.Data.Vector.Attach
Vector.pmap_congr_left : ∀ {α : Type u_1} {β : Type u_2} {n : ℕ} {p q : α → Prop} {f : (a : α) → p a → β} {g : (a : α) → q a → β}
  (xs : Vector α n) {H₁ : ∀ a ∈ xs, p a} {H₂ : ∀ a ∈ xs, q a},
  (∀ a ∈ xs, ∀ (h₁ : p a) (h₂ : q a), f a h₁ = g a h₂) → Vector.pmap f xs H₁ = Vector.pmap g xs H₂
-- Mathlib.Data.Fintype.EquivFin
/-- If every finset in a type has bounded cardinality, that type is finite.  -/
fintypeOfFinsetCardLe : {ι : Type u_4} → (n : ℕ) → (∀ (s : Finset ι), s.card ≤ n) → Fintype ι
-- Mathlib.Data.Ordmap.Ordset
Ordnode.Valid'.node4L_lemma₃ : ∀ {b c d : ℕ}, 2 * d ≤ b + c + 1 → b ≤ 3 * c → d ≤ 3 * c
-- Mathlib.Order.CompletePartialOrder
/-- A complete partial order is an conditionally complete partial order.  -/
instConditionallyCompletePartialOrderSup : {α : Type u_2} → [CompletePartialOrder α] → ConditionallyCompletePartialOrderSup α
-- Mathlib.CategoryTheory.Monad.Kleisli
CategoryTheory.Cokleisli.Hom.mk.sizeOf_spec : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {U : CategoryTheory.Comonad C}
  {c c' : CategoryTheory.Cokleisli U} [inst_1 : SizeOf C] (of : U.obj c.of ⟶ c'.of), sizeOf { of := of } = 1 + sizeOf of
-- Mathlib.AlgebraicGeometry.AffineTransitionLimit
AlgebraicGeometry.ExistsHomHomCompEqCompAux.h𝒰S : ∀ {I : Type u} [inst : CategoryTheory.Category.{u, u} I] {S X : AlgebraicGeometry.Scheme}
  {D : CategoryTheory.Functor I AlgebraicGeometry.Scheme} {t : D ⟶ (CategoryTheory.Functor.const I).obj S} {f : X ⟶ S}
  (self : AlgebraicGeometry.ExistsHomHomCompEqCompAux D t f) (i : self.𝒰S.I₀), AlgebraicGeometry.IsAffine (self.𝒰S.X i)
-- Mathlib.MeasureTheory.SetSemiring
MeasureTheory.IsSetRing.partialSups_mem : ∀ {α : Type u_1} {C : Set (Set α)} {ι : Type u_2} [inst : Preorder ι] [inst_1 : LocallyFiniteOrderBot ι],
  MeasureTheory.IsSetRing C → ∀ {s : ι → Set α}, (∀ (n : ι), s n ∈ C) → ∀ (n : ι), (partialSups s) n ∈ C
-- Mathlib.NumberTheory.Fermat
Int.fermatNumber_eq_fermatNumber_sq_sub_two_mul_fermatNumber_sub_one_sq : ∀ (n : ℕ), ↑(n + 2).fermatNumber = ↑(n + 1).fermatNumber ^ 2 - 2 * (↑n.fermatNumber - 1) ^ 2
-- Mathlib.CategoryTheory.Limits.Shapes.BinaryBiproducts
/-- `HasBinaryBiproduct P Q` expresses the mere existence of a bicone which is
simultaneously a limit and a colimit of the diagram `pair P Q`.  -/
CategoryTheory.Limits.HasBinaryBiproduct : {C : Type uC} → [inst : CategoryTheory.Category.{uC', uC} C] → [CategoryTheory.Limits.HasZeroMorphisms C] → C → C → Prop
-- Mathlib.Geometry.Manifold.Submersion
/-- If `f` is a submersion at `x` w.r.t. some complement `F`, it is a submersion at `x`.

Note that the proof contains a small formalisation-related subtlety: `F` can live in any universe,
while being a submersion at `x` requires the existence of a complement in the same universe as
the model normed space of `N`. This is solved by `smallComplement` and `smallEquiv`.  -/
Manifold.IsSubmersionAtOfComplement.isSubmersionAt : ∀ {𝕜 : Type u_1} {E'' : Type u_3} {F : Type u_5} {H : Type u_7} {G : Type u_9} {E : Type u}
  [inst : NontriviallyNormedField 𝕜] [inst_1 : NormedAddCommGroup E] [inst_2 : NormedSpace 𝕜 E]
  [inst_3 : NormedAddCommGroup E''] [inst_4 : NormedSpace 𝕜 E''] [inst_5 : NormedAddCommGroup F]
  [inst_6 : NormedSpace 𝕜 F] [inst_7 : TopologicalSpace H] [inst_8 : TopologicalSpace G] {I : ModelWithCorners 𝕜 E H}
  {J : ModelWithCorners 𝕜 E'' G} {M : Type u_11} {N : Type u_13} [inst_9 : TopologicalSpace M]
  [inst_10 : ChartedSpace H M] [inst_11 : TopologicalSpace N] [inst_12 : ChartedSpace G N] {n : WithTop ℕ∞} {f : M → N}
  {x : M}, Manifold.IsSubmersionAtOfComplement F I J n f x → Manifold.IsSubmersionAt I J n f x
-- Mathlib.CategoryTheory.DifferentialObject
CategoryTheory.DifferentialObject.Hom.ext : ∀ {S : Type u_1} {inst : AddMonoidWithOne S} {C : Type u} {inst_1 : CategoryTheory.Category.{v, u} C}
  {inst_2 : CategoryTheory.Limits.HasZeroMorphisms C} {inst_3 : CategoryTheory.HasShift C S}
  {X Y : CategoryTheory.DifferentialObject S C} {x y : X.Hom Y}, x.f = y.f → x = y
-- Mathlib.AlgebraicGeometry.Morphisms.Integral
AlgebraicGeometry.IsIntegralHom.iff_universallyClosed_and_isAffineHom : ∀ {X Y : AlgebraicGeometry.Scheme} {f : X ⟶ Y},
  AlgebraicGeometry.IsIntegralHom f ↔ AlgebraicGeometry.UniversallyClosed f ∧ AlgebraicGeometry.IsAffineHom f
-- Lean.Meta.Tactic.Grind.Arith.CommRing.Types
/-- Shared state for non-commutative and commutative rings.  -/
Lean.Meta.Grind.Arith.CommRing.Ring : Type
-- Mathlib.Analysis.InnerProductSpace.TensorProduct
/-- `TensorProduct.map` as a continuous linear map, i.e. the continuous linear map
`x ⊗ₜ[𝕜] y ↦ f(x) ⊗ₜ[𝕜] g(y)` formed from the continuous linear maps `f` and `g`.  -/
TensorProduct.mapL : {𝕜 : Type u_1} →
  {E : Type u_2} →
    {F : Type u_3} →
      {G : Type u_4} →
        {H : Type u_5} →
          [inst : RCLike 𝕜] →
            [inst_1 : NormedAddCommGroup E] →
              [inst_2 : InnerProductSpace 𝕜 E] →
                [inst_3 : NormedAddCommGroup F] →
                  [inst_4 : InnerProductSpace 𝕜 F] →
                    [inst_5 : NormedAddCommGroup G] →
                      [inst_6 : InnerProductSpace 𝕜 G] →
                        [inst_7 : NormedAddCommGroup H] →
                          [inst_8 : InnerProductSpace 𝕜 H] →
                            (E →L[𝕜] F) → (G →L[𝕜] H) → TensorProduct 𝕜 E G →L[𝕜] TensorProduct 𝕜 F H
-- Init.Data.List.BasicAux
/-- Returns the last element in the list. Panics and returns `default` if the list is empty.

Safer alternatives include:
* `getLast?`, which returns an `Option`,
* `getLastD`, which takes a fallback value for empty lists, and
* `getLast`, which requires a proof that the list is non-empty.

Examples:
* `["circle", "rectangle"].getLast! = "rectangle"`
* `["circle"].getLast! = "circle"`
 -/
List.getLast! : {α : Type u_1} → [Inhabited α] → List α → α
-- Lean.Meta.Tactic.Simp.Types
Lean.Meta.Simp.Result.getProof : Lean.Meta.Simp.Result → Lean.MetaM Lean.Expr
-- Mathlib.NumberTheory.Harmonic.ZetaAsymp
/-- Formula for `Λ 1`. Note that mathematically `Λ 1` is undefined, but our construction ascribes
this particular value to it.  -/
completedRiemannZeta_one : completedRiemannZeta 1 = (↑Real.eulerMascheroniConstant - Complex.log (4 * ↑Real.pi)) / 2
-- Mathlib.CategoryTheory.Equivalence
CategoryTheory.Equivalence.changeFunctor_unitIso_inv_app : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  (e : C ≌ D) {G : CategoryTheory.Functor C D} (iso : e.functor ≅ G) (X : C),
  (e.changeFunctor iso).unitIso.inv.app X =
    CategoryTheory.CategoryStruct.comp (e.inverse.map (iso.inv.app X)) (e.unitIso.inv.app X)
-- Mathlib.Topology.FiberBundle.Trivialization
/-- Given two bundle trivializations `e`, `e'` of a topological fiber bundle `proj : Z → B`
over a linearly ordered base `B` and a point `a ∈ e.baseSet ∩ e'.baseSet` such that
`e` equals `e'` on `proj ⁻¹' {a}`, `e.piecewise_le_of_eq e' a He He' Heq` is the bundle
trivialization over `Set.ite (Iic a) e.baseSet e'.baseSet` that is equal to `e` on points `p`
such that `proj p ≤ a` and is equal to `e'` otherwise.  -/
Bundle.Trivialization.piecewiseLeOfEq : {B : Type u_1} →
  {F : Type u_2} →
    {Z : Type u_4} →
      [inst : TopologicalSpace B] →
        [inst_1 : TopologicalSpace F] →
          {proj : Z → B} →
            [inst_2 : TopologicalSpace Z] →
              [inst_3 : LinearOrder B] →
                [OrderTopology B] →
                  (e e' : Bundle.Trivialization F proj) →
                    (a : B) →
                      a ∈ e.baseSet →
                        a ∈ e'.baseSet → (∀ (p : Z), proj p = a → ↑e p = ↑e' p) → Bundle.Trivialization F proj
-- Mathlib.Topology.MetricSpace.Pseudo.Defs
Metric.iUnion_ball_nat : ∀ {α : Type u} [inst : PseudoMetricSpace α] (x : α), ⋃ n, Metric.ball x ↑n = Set.univ
-- Init.Data.Iterators.Lemmas.Consumers.Loop
Std.Iter.forIn_eq_forIn_toIterM : ∀ {α β : Type w} [inst : Std.Iterator α Id β] [Std.Iterators.Finite α Id] {m : Type w → Type w''} [inst_2 : Monad m]
  [LawfulMonad m] [inst_4 : Std.IteratorLoop α Id m] {γ : Type w} {it : Std.Iter β} {init : γ}
  {f : β → γ → m (ForInStep γ)}, forIn it init f = forIn it.toIterM init f
-- Mathlib.Dynamics.Circle.RotationNumber.TranslationNumber
CircleDeg1Lift.translate_inv_apply : ∀ (x y : ℝ), ↑(CircleDeg1Lift.translate (Multiplicative.ofAdd x))⁻¹ y = -x + y
-- Mathlib.Probability.StrongLaw
ProbabilityTheory.truncation_eq_self : ∀ {α : Type u_1} {f : α → ℝ} {A : ℝ} {x : α}, |f x| < A → ProbabilityTheory.truncation f A x = f x
-- Mathlib.Combinatorics.SimpleGraph.Hasse
SimpleGraph.hasse_prod : ∀ (α : Type u_1) (β : Type u_2) [inst : PartialOrder α] [inst_1 : PartialOrder β],
  SimpleGraph.hasse (α × β) = SimpleGraph.hasse α □ SimpleGraph.hasse β
-- Mathlib.CategoryTheory.Comma.Presheaf.Basic
CategoryTheory.OverPresheafAux.counitAuxAux_hom : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {A : CategoryTheory.Functor Cᵒᵖ (Type v)}
  (F : CategoryTheory.Functor (CategoryTheory.CostructuredArrow CategoryTheory.yoneda A)ᵒᵖ (Type v))
  (s : CategoryTheory.CostructuredArrow CategoryTheory.yoneda A),
  (CategoryTheory.OverPresheafAux.counitAuxAux F s).hom =
    TypeCat.ofHom (CategoryTheory.OverPresheafAux.counitForward F s)
-- Mathlib.CategoryTheory.Abelian.GrothendieckAxioms.Basic
CategoryTheory.instAB4OfSize : ∀ (C : Type u) [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Limits.HasCoproducts C]
  [CategoryTheory.AB4OfSize.{w, v, u} C], CategoryTheory.AB4OfSize.{0, v, u} C
-- Init.Data.SInt.Lemmas
UInt16.toUInt16_toInt16 : ∀ (x : UInt16), x.toInt16.toUInt16 = x
-- Mathlib.Topology.Connected.LocallyConnected
/-- Any topology coinduced by a locally connected topology is locally connected.  -/
Topology.IsCoinducing.locallyConnectedSpace : ∀ {α : Type u} {β : Type v} [inst : TopologicalSpace α] [LocallyConnectedSpace α] [inst_2 : TopologicalSpace β]
  {f : α → β}, Topology.IsCoinducing f → LocallyConnectedSpace β
-- Mathlib.Algebra.Quaternion
QuaternionAlgebra.coe_add : ∀ {R : Type u_3} {c₁ c₂ c₃ : R} (x y : R) [inst : AddZeroClass R], ↑(x + y) = ↑x + ↑y
-- Mathlib.Analysis.CStarAlgebra.CStarMatrix
CStarMatrix.norm_entry_le_norm : ∀ {m : Type u_1} {n : Type u_2} {A : Type u_5} [inst : Fintype m] [inst_1 : NonUnitalCStarAlgebra A]
  [inst_2 : PartialOrder A] [inst_3 : StarOrderedRing A] [inst_4 : Fintype n] {M : CStarMatrix m n A} {i : m} {j : n},
  ‖M i j‖ ≤ ‖M‖
-- Lean.Widget.InteractiveDiagnostic
Lean.Widget.MsgEmbed.widget.inj : ∀ {wi : Lean.Widget.WidgetInstance} {alt : Lean.Widget.TaggedText Lean.Widget.MsgEmbed}
  {wi_1 : Lean.Widget.WidgetInstance} {alt_1 : Lean.Widget.TaggedText Lean.Widget.MsgEmbed},
  Lean.Widget.MsgEmbed.widget wi alt = Lean.Widget.MsgEmbed.widget wi_1 alt_1 → wi = wi_1 ∧ alt = alt_1
-- Mathlib.Topology.Sets.Opens
TopologicalSpace.Opens.gc : ∀ {α : Type u_2} [inst : TopologicalSpace α], GaloisConnection SetLike.coe TopologicalSpace.Opens.interior
-- Mathlib.RingTheory.Ideal.Cotangent
Ideal.cotangentEquivIdeal_symm_apply : ∀ {R : Type u} [inst : CommRing R] (I : Ideal R) (x : R) (hx : x ∈ I),
  I.cotangentEquivIdeal.symm ⟨(Submodule.mkQ (I ^ 2)) x, ⋯⟩ = I.toCotangent ⟨x, hx⟩
-- Mathlib.RingTheory.Etale.Finite
/-- The fiber functor for finite étale `R`-algebras at the geometric point `Ω`: This is the
functor sending `S` to `R`-algebra homomorphisms `S →ₐ[R] Ω`.  -/
CommAlgCat.FiniteEtale.fiber : (R : Type u) →
  [inst : CommRing R] →
    (Ω : Type w) → [inst_1 : Field Ω] → [Algebra R Ω] → CategoryTheory.Functor (CommAlgCat.FiniteEtale R)ᵒᵖ FintypeCat
-- Mathlib.NumberTheory.ModularForms.Basic
CuspForm.coe_mulModularForm : ∀ {Γ : Subgroup (GL (Fin 2) ℝ)} [inst : Γ.HasDetPlusMinusOne] {k₁ k₂ : ℤ} (f : CuspForm Γ k₁) (g : ModularForm Γ k₂),
  ⇑(f.mulModularForm g) = ⇑f * ⇑g
-- Mathlib.RingTheory.MvPowerSeries.LinearTopology
/-- A power series `f` belongs to the two-sided ideal `basis σ R ⟨J, d⟩`
if and only if `coeff e f ∈ J` for all `e ≤ d`.  -/
MvPowerSeries.LinearTopology.mem_basis_iff : ∀ {σ : Type u_1} {R : Type u_2} [inst : Ring R] {f : MvPowerSeries σ R} {Jd : TwoSidedIdeal R × (σ →₀ ℕ)},
  f ∈ MvPowerSeries.LinearTopology.basis σ R Jd ↔ ∀ e ≤ Jd.2, (MvPowerSeries.coeff e) f ∈ Jd.1
-- Std.Data.DHashMap.IteratorLemmas
Std.DHashMap.toListRev_valuesIter : ∀ {α β : Type u} [inst : BEq α] [inst_1 : Hashable α] {m : Std.DHashMap α fun x => β},
  m.valuesIter.toListRev = (List.map Sigma.snd m.toList).reverse
-- Init.Data.Vector.Lemmas
Vector.push_append : ∀ {α : Type u_1} {n m : ℕ} {as : Vector α n} {bs : Vector α m} {a : α}, (as ++ bs).push a = as ++ bs.push a
-- Mathlib.Topology.Order.Basic
/-- For a function taking values in a second countable space, the set of points `x` for
which the image under `f` of `(x, ∞)` is separated above from `f x` is countable.  -/
countable_image_lt_image_Ioi : ∀ {α : Type u} {β : Type v} [inst : TopologicalSpace α] [inst_1 : LinearOrder α] [OrderTopology α]
  [inst_3 : LinearOrder β] (f : β → α) [SecondCountableTopology α],
  {x | ∃ z, f x < z ∧ ∀ (y : β), x < y → z ≤ f y}.Countable
-- Mathlib.CategoryTheory.Presentable.Directed
CategoryTheory.IsCardinalFiltered.exists_cardinal_directed.functor_obj : ∀ (J : Type w) [inst : CategoryTheory.SmallCategory J] (κ : Cardinal.{w})
  (D : CategoryTheory.IsCardinalFiltered.exists_cardinal_directed.DiagramWithUniqueTerminal J κ),
  (CategoryTheory.IsCardinalFiltered.exists_cardinal_directed.functor J κ).obj D = D.top
-- Mathlib.Order.Comparable
IncompRel.not_antisymmRel : ∀ {α : Type u_1} {a b : α} {r : α → α → Prop}, IncompRel r a b → ¬AntisymmRel r a b
-- Mathlib.CategoryTheory.Sites.Equivalence
CategoryTheory.hasColimitsEssentiallySmallSite : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] (J : CategoryTheory.GrothendieckTopology C) (A : Type u₃)
  [inst_1 : CategoryTheory.Category.{v₃, u₃} A] [inst_2 : CategoryTheory.EssentiallySmall.{w, v₁, u₁} C]
  [CategoryTheory.Limits.HasColimits
      (CategoryTheory.Sheaf ((CategoryTheory.equivSmallModel C).inverse.inducedTopology J) A)],
  CategoryTheory.Limits.HasColimitsOfSize.{max v₃ w, max v₃ w, max u₁ v₃, max (max (max u₃ u₁) v₃) v₁}
    (CategoryTheory.Sheaf J A)
-- Lean.Compiler.IR.Basic
Lean.IR.Index.lt : Lean.IR.Index → Lean.IR.Index → Bool
-- Mathlib.Topology.Algebra.GroupWithZero
ContinuousWithinAt.div_const : ∀ {α : Type u_1} {G₀ : Type u_3} [inst : DivInvMonoid G₀] [inst_1 : TopologicalSpace G₀] [SeparatelyContinuousMul G₀]
  {f : α → G₀} {s : Set α} [inst_3 : TopologicalSpace α] {a : α},
  ContinuousWithinAt f s a → ∀ (y : G₀), ContinuousWithinAt (fun x => f x / y) s a
-- Mathlib.LinearAlgebra.ExteriorPower.Basis
/-- If `b` is a basis of `M` (indexed by a linearly ordered type), then the family
`exteriorPower.ιMulti R n b` of the `n`-fold exterior products of its elements is linearly
independent in the `n`th exterior power of `M`.  -/
exteriorPower.ιMulti_family_linearIndependent_ofBasis : ∀ (R : Type u_1) {M : Type u_3} (n : ℕ) [inst : CommRing R] [inst_1 : AddCommGroup M] [inst_2 : Module R M]
  {I : Type u_5} [inst_3 : LinearOrder I] (b : Module.Basis I R M),
  LinearIndependent (ι := ↑(Set.powersetCard I n)) R (exteriorPower.ιMulti_family R n ⇑b)
-- Mathlib.Data.Ordmap.Ordnode
Ordnode.Emem.decidable : {α : Type u_1} → (x : α) → [DecidableEq α] → (t : Ordnode α) → Decidable (Ordnode.Emem x t)
-- Mathlib.Algebra.Ring.Periodic
Function.Periodic.zsmul_sub_eq : ∀ {α : Type u_1} {β : Type u_2} {f : α → β} {c x : α} [inst : AddCommGroup α],
  Function.Periodic f c → ∀ (n : ℤ), f (n • c - x) = f (-x)
-- Mathlib.NumberTheory.ModularForms.EisensteinSeries.Basic
/-- This defines Eisenstein series as modular forms of weight `k`, level `Γ(N)` and congruence
condition given by `a : Fin 2 → ZMod N`.  -/
ModularForm.eisensteinSeriesMF : {k : ℤ} →
  {N : ℕ} →
    [NeZero N] →
      3 ≤ k →
        (Fin 2 → ZMod N) → ModularForm (Subgroup.map (Matrix.SpecialLinearGroup.mapGL ℝ) (CongruenceSubgroup.Gamma N)) k
-- Mathlib.Combinatorics.HalesJewett
/-- The **multidimensional Hales-Jewett theorem**, aka **extended Hales-Jewett theorem**: For any
finite types `η`, `α` and `κ`, there exists a finite type `ι` such that whenever the hypercube
`ι → α` is `κ`-colored, there is a monochromatic combinatorial subspace of dimension `η`.  -/
Combinatorics.Subspace.exists_mono_in_high_dimension : ∀ (α : Type u_5) (κ : Type u_6) (η : Type u_7) [Finite α] [Finite κ] [Finite η],
  ∃ ι x, ∀ (C : (ι → α) → κ), ∃ l, Combinatorics.Subspace.IsMono C l
-- Mathlib.CategoryTheory.Shift.ShiftedHom
CategoryTheory.ShiftedHom.mk₀_comp_mk₀ : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] {M : Type u_4} [inst_1 : AddMonoid M]
  [inst_2 : CategoryTheory.HasShift C M] {X Y Z : C} (f : X ⟶ Y) (g : Y ⟶ Z) {a b c : M} (h : b + a = c) (ha : a = 0)
  (hb : b = 0),
  (CategoryTheory.ShiftedHom.mk₀ a ha f).comp (CategoryTheory.ShiftedHom.mk₀ b hb g) h =
    CategoryTheory.ShiftedHom.mk₀ c ⋯ (CategoryTheory.CategoryStruct.comp f g)
-- Mathlib.Order.Filter.Pointwise
Filter.comap_inv : ∀ {α : Type u_2} [inst : InvolutiveInv α] {f : Filter α}, Filter.comap Inv.inv f = f⁻¹
-- Mathlib.GroupTheory.OrderOfElement
Subgroup.orderOf_coe : ∀ {G : Type u_1} [inst : Group G] {H : Subgroup G} (a : ↥H), orderOf ↑a = orderOf a
-- Init.Data.Nat.Basic
Nat.one_mul : ∀ (n : ℕ), 1 * n = n
-- Mathlib.Algebra.Group.Hom.Defs
AddMonoidHom.instFunLike.eq_1 : ∀ {M : Type u_4} {N : Type u_5} [inst : AddZero M] [inst_1 : AddZero N],
  AddMonoidHom.instFunLike = { coe := fun f => (↑f).toFun, coe_injective := ⋯ }
-- Mathlib.Combinatorics.Additive.PluenneckeRuzsa
/-- **Ruzsa's triangle inequality**. Div-div-mul version.  -/
Finset.card_div_mul_le_card_div_mul_card_mul : ∀ {G : Type u_1} [inst : DecidableEq G] [inst_1 : CommGroup G] (A B C : Finset G),
  (A / C).card * B.card ≤ (A / B).card * (B * C).card
-- Mathlib.Algebra.Order.SuccPred
Order.add_one_le_iff_of_not_isMax' : ∀ {α : Type u_1} {x y : α} [inst : Preorder α] [inst_1 : Add α] [inst_2 : One α] [SuccAddOrder α],
  ¬IsMax y → (x + 1 ≤ y ↔ x < y)
-- Mathlib.Algebra.Order.CauSeq.Completion
CauSeq.Completion.zero_ne_one : ∀ {α : Type u_1} [inst : Field α] [inst_1 : LinearOrder α] [inst_2 : IsStrictOrderedRing α] {β : Type u_2}
  [inst_3 : DivisionRing β] {abv : β → α} [inst_4 : IsAbsoluteValue abv], 0 ≠ 1
-- Mathlib.Order.Partition.Basic
Partition.parts_top_subset : ∀ {α : Type u_1} {s : α} [inst : CompleteLattice α], ↑⊤ ⊆ {s}
-- Mathlib.Algebra.Group.Pointwise.Finset.Basic
Finset.image_pow : ∀ {F : Type u_1} {α : Type u_2} {β : Type u_3} [inst : DecidableEq α] [inst_1 : DecidableEq β] [inst_2 : Monoid α]
  [inst_3 : Monoid β] [inst_4 : FunLike F α β] [MonoidHomClass F α β] (f : F) (s : Finset α) (n : ℕ),
  Finset.image (⇑f) (s ^ n) = Finset.image (⇑f) s ^ n
-- Mathlib.Data.Rat.Floor
Rat.isNat_round : ∀ {R : Type u_3} [inst : Ring R] [inst_1 : LinearOrder R] [IsStrictOrderedRing R] [inst_3 : FloorRing R] (r : R)
  (m : ℕ), Mathlib.Meta.NormNum.IsNat r m → Mathlib.Meta.NormNum.IsNat (round r) m
-- Mathlib.MeasureTheory.Measure.Content
/-- A content `μ` is called regular if for every compact set `K`,
`μ(K) = inf {μ(K') : K ⊂ int K' ⊂ K'}`. See Paul Halmos (1950), Measure Theory, §54.  -/
MeasureTheory.Content.ContentRegular : {G : Type w} → [inst : TopologicalSpace G] → MeasureTheory.Content G → Prop
-- Lean.Data.Lsp.Extra
Lean.Lsp.LineRange.start : Lean.Lsp.LineRange → ℕ
-- Mathlib.Algebra.Order.Sub.Unbundled.Basic
tsub_add_tsub_cancel : ∀ {α : Type u_1} [inst : AddCommSemigroup α] [inst_1 : PartialOrder α] [ExistsAddOfLE α] [AddLeftMono α]
  [inst_4 : Sub α] [OrderedSub α] {a b c : α}, b ≤ a → c ≤ b → a - b + (b - c) = a - c
-- Mathlib.Geometry.Manifold.BumpFunction
SmoothBumpFunction.closedBall_subset : ∀ {E : Type uE} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] {H : Type uH} [inst_2 : TopologicalSpace H]
  {I : ModelWithCorners ℝ E H} {M : Type uM} [inst_3 : TopologicalSpace M] [inst_4 : ChartedSpace H M] {c : M}
  (self : SmoothBumpFunction I c),
  Metric.closedBall (↑(extChartAt I c) c) self.rOut ∩ Set.range ↑I ⊆ (extChartAt I c).target
-- Batteries.Recycling.RBTree.Lemmas
RBTree.RBNode.lowerBound?.eq_def : ∀ {α : Type u_1} (cut : α → Ordering) (x : RBTree.RBNode α) (x_1 : Option α),
  RBTree.RBNode.lowerBound? cut x x_1 =
    match x, x_1 with
    | RBTree.RBNode.nil, lb => lb
    | RBTree.RBNode.node c a y b, lb =>
      match cut y with
      | Ordering.lt => RBTree.RBNode.lowerBound? cut a lb
      | Ordering.gt => RBTree.RBNode.lowerBound? cut b (some y)
      | Ordering.eq => some y
-- Mathlib.Topology.CantorBendixson
CantorBendixson.iteratedDerivedSet_succ : ∀ {X : Type u} [inst : TopologicalSpace X] {s : Set X} {a : Ordinal.{u}},
  CantorBendixson.iteratedDerivedSet s (a + 1) = relDerivedSet (CantorBendixson.iteratedDerivedSet s a)
-- Mathlib.Combinatorics.Colex
Finset.Colex.toColex_sdiff_le_toColex_sdiff' : ∀ {α : Type u_1} [inst : PartialOrder α] {s t : Finset α} [inst_1 : DecidableEq α],
  toColex (s \ t) ≤ toColex (t \ s) ↔ toColex s ≤ toColex t
-- Mathlib.Algebra.Lie.Basic
instIsLieTower : ∀ {L : Type v} {M : Type w} [inst : LieRing L] [inst_1 : AddCommGroup M] [inst_2 : LieRingModule L M], IsLieTower L L M
-- Mathlib.Topology.Algebra.LinearTopology
/-- The discrete topology on any `R`-module is `R`-linear.  -/
IsLinearTopology.instOfDiscreteTopology : ∀ {R : Type u_1} {M : Type u_3} [inst : Ring R] [inst_1 : AddCommGroup M] [inst_2 : Module R M]
  [inst_3 : TopologicalSpace M] [DiscreteTopology M], IsLinearTopology R M
-- Mathlib.Analysis.Normed.Ring.Basic
ULift.nonUnitalNormedCommRing : {α : Type u_2} → [NonUnitalNormedCommRing α] → NonUnitalNormedCommRing (ULift.{u_5, u_2} α)
-- Mathlib.MeasureTheory.Integral.Lebesgue.Basic
MeasureTheory.lintegral_biUnion_finset : ∀ {α : Type u_1} {β : Type u_2} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} {s : Finset β} {t : β → Set α},
  (↑s).PairwiseDisjoint t →
    (∀ b ∈ s, MeasurableSet (t b)) →
      ∀ (f : α → ENNReal), ∫⁻ (a : α) in ⋃ b ∈ s, t b, f a ∂μ = ∑ b ∈ s, ∫⁻ (a : α) in t b, f a ∂μ
-- Std.Data.HashSet.Lemmas
Std.HashSet.size_toArray : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} {m : Std.HashSet α} [EquivBEq α] [LawfulHashable α],
  m.toArray.size = m.size
-- Mathlib.Combinatorics.Additive.Energy
Finset.mulEnergy_self_eq_zero_iff : ∀ {α : Type u_1} [inst : DecidableEq α] [inst_1 : Mul α] {s : Finset α}, s.mulEnergy s = 0 ↔ s = ∅
-- Mathlib.Topology.MetricSpace.Pseudo.Defs
PseudoMetricSpace.toDist : {α : Type u} → [self : PseudoMetricSpace α] → Dist α
-- Mathlib.Topology.Category.CompHausLike.Cartesian
/-- Explicit binary cofan in `CompHausLike P`, given that the predicate `P` is preserved under taking
type-theoretic sums.
 -/
CompHausLike.coproductCocone : {P : TopCat → Prop} →
  (X Y : CompHausLike P) → [CompHausLike.HasProp P (↑X.toTop ⊕ ↑Y.toTop)] → CategoryTheory.Limits.BinaryCofan X Y
-- Mathlib.Geometry.RingedSpace.PresheafedSpace.HasColimits
/-- Auxiliary definition for `AlgebraicGeometry.PresheafedSpace.instHasColimits`.
 -/
AlgebraicGeometry.PresheafedSpace.colimit : {J : Type u'} →
  [inst : CategoryTheory.Category.{v', u'} J] →
    {C : Type u} →
      [inst_1 : CategoryTheory.Category.{v, u} C] →
        [CategoryTheory.Limits.HasColimitsOfShape J TopCat] →
          [∀ (X : TopCat), CategoryTheory.Limits.HasLimitsOfShape Jᵒᵖ (TopCat.Presheaf C X)] →
            CategoryTheory.Functor J (AlgebraicGeometry.PresheafedSpace C) → AlgebraicGeometry.PresheafedSpace C
-- Mathlib.Order.ConditionallyCompleteLattice.Finset
Multiset.iSup_mem_map_of_ne_zero : ∀ {ι : Type u_1} {α : Type u_2} [inst : ConditionallyCompleteLinearOrderBot α] {s : Multiset ι} (f : ι → α),
  s ≠ 0 → ⨆ x ∈ s, f x ∈ Multiset.map f s