mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Topology.EMetricSpace.BoundedVariation
eVariationOn.eq_biSup_inter_Icc : ∀ {α : Type u_1} [inst : LinearOrder α] {E : Type u_2} [inst_1 : PseudoEMetricSpace E] {f : α → E} {s : Set α},
  eVariationOn f s = ⨆ p ∈ {p | p.1 ∈ s ∧ p.2 ∈ s ∧ p.1 ≤ p.2}, eVariationOn f (s ∩ Set.Icc p.1 p.2)
-- Mathlib.Tactic.Ring.Common
Mathlib.Tactic.Ring.Common.ExtractCoeff.mk : {e : Q(ℕ)} →
  (k e' : Q(ℕ)) →
    Mathlib.Tactic.Ring.Common.ExProdNat e' → Q(«$e» = «$e'» * «$k») → Mathlib.Tactic.Ring.Common.ExtractCoeff e
-- Mathlib.CategoryTheory.CommSq
CategoryTheory.CommSq.LiftStruct.ext : ∀ {C : Type u_1} {inst : CategoryTheory.Category.{v_1, u_1} C} {A B X Y : C} {f : A ⟶ X} {i : A ⟶ B} {p : X ⟶ Y}
  {g : B ⟶ Y} {sq : CategoryTheory.CommSq f i p g} {x y : sq.LiftStruct}, x.l = y.l → x = y
-- Mathlib.AlgebraicTopology.SimplicialSet.Homology.Basic
/-- The simplicial homology with coefficients in `R : C` in degree `n`
of a simplicial set `X`.  -/
SSet.homology : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    [CategoryTheory.Limits.HasCoproducts C] →
      [inst_2 : CategoryTheory.Preadditive C] → SSet → C → [CategoryTheory.CategoryWithHomology C] → ℕ → C
-- Mathlib.Probability.Independence.Basic
ProbabilityTheory.Indep_iff : ∀ {Ω : Type u_1} (m₁ m₂ : MeasurableSpace Ω) {_mΩ : MeasurableSpace Ω} (μ : MeasureTheory.Measure Ω),
  ProbabilityTheory.Indep m₁ m₂ μ ↔ ∀ (t1 t2 : Set Ω), MeasurableSet t1 → MeasurableSet t2 → μ (t1 ∩ t2) = μ t1 * μ t2
-- Mathlib.Order.Interval.Set.LinearOrder
Set.Iio_union_Ici : ∀ {α : Type u_1} [inst : LinearOrder α] {a : α}, Set.Iio a ∪ Set.Ici a = Set.univ
-- Mathlib.AlgebraicGeometry.Morphisms.ClosedImmersion
AlgebraicGeometry.IsClosedImmersion.iff_isPreimmersion : ∀ {X Y : AlgebraicGeometry.Scheme} {f : X ⟶ Y},
  AlgebraicGeometry.IsClosedImmersion f ↔ AlgebraicGeometry.IsPreimmersion f ∧ IsClosed (Set.range ⇑f)
-- Mathlib.RingTheory.Etale.Kaehler
KaehlerDifferential.tensorKaehlerEquivOfFormallyEtale.congr_simp : ∀ (R : Type u_1) (S : Type u_2) (T : Type u_3) [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : CommRing T]
  [inst_3 : Algebra R S] [inst_4 : Algebra R T] [inst_5 : Algebra S T] [inst_6 : IsScalarTower R S T]
  [inst_7 : Algebra.FormallyEtale S T],
  KaehlerDifferential.tensorKaehlerEquivOfFormallyEtale R S T =
    KaehlerDifferential.tensorKaehlerEquivOfFormallyEtale R S T
-- Mathlib.Topology.Separation.Basic
/-- In an R₁ space, the filters `coclosedCompact` and `cocompact` are equal.  -/
Filter.coclosedCompact_eq_cocompact : ∀ {X : Type u_1} [inst : TopologicalSpace X] [R1Space X], Filter.coclosedCompact X = Filter.cocompact X
-- Mathlib.NumberTheory.Chebyshev
/-- Least common multiple of `Icc 1 n`.  -/
Nat.lcmUpto : ℕ → ℕ
-- Mathlib.CategoryTheory.Monoidal.Grp
CategoryTheory.GrpObj.instTensorUnit.eq_1 : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.CartesianMonoidalCategory C],
  CategoryTheory.GrpObj.instTensorUnit =
    { toMonObj := CategoryTheory.MonObj.instTensorUnit,
      inv := CategoryTheory.CategoryStruct.id (CategoryTheory.MonoidalCategoryStruct.tensorUnit C), left_inv := ⋯,
      right_inv := ⋯ }
-- Mathlib.Analysis.Calculus.InverseFunctionTheorem.ApproximatesLinearOn
ApproximatesLinearOn.map_nhds_eq : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {F : Type u_3} [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F] {f : E → F}
  [CompleteSpace E] {s : Set E} {c : NNReal} {f' : E →L[𝕜] F},
  ApproximatesLinearOn f f' s c →
    ∀ (f'symm : f'.NonlinearRightInverse) {x : E},
      s ∈ nhds x → Subsingleton F ∨ c < f'symm.nnnorm⁻¹ → Filter.map f (nhds x) = nhds (f x)
-- Mathlib.Data.Num.Basic
numNatCoe : {α : Type u_1} → [One α] → [Add α] → [Zero α] → CoeHTCT Num α
-- Init.Grind.Ring.Field
Lean.Grind.Field.zpow_add_one : ∀ {α : Type u_1} [inst : Lean.Grind.Field α] {a : α}, a ≠ 0 → ∀ (n : ℤ), a ^ (n + 1) = a ^ n * a
-- Mathlib.CategoryTheory.Limits.Shapes.StrongEpi
/-- A strong epi category is a category in which every epimorphism is strong.  -/
CategoryTheory.StrongEpiCategory.strongEpi_of_epi : ∀ {C : Type u} {inst : CategoryTheory.Category.{v, u} C} [self : CategoryTheory.StrongEpiCategory C] {X Y : C}
  (f : X ⟶ Y) [CategoryTheory.Epi f], CategoryTheory.StrongEpi f
-- Aesop.Rule
Aesop.instBEqRegularRule.beq : Aesop.RegularRule → Aesop.RegularRule → Bool
-- Mathlib.Algebra.Homology.Double
/-- The isomorphism `(double f hi₀₁).X i₀ ≅ X₀`.  -/
HomologicalComplex.doubleXIso₀ : {C : Type u_1} →
  [inst : CategoryTheory.Category.{v_1, u_1} C] →
    [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C] →
      [inst_2 : CategoryTheory.Limits.HasZeroObject C] →
        {X₀ X₁ : C} →
          (f : X₀ ⟶ X₁) →
            {ι : Type u_2} →
              {c : ComplexShape ι} → {i₀ i₁ : ι} → (hi₀₁ : c.Rel i₀ i₁) → (HomologicalComplex.double f hi₀₁).X i₀ ≅ X₀
-- Mathlib.MeasureTheory.Measure.Typeclasses.Finite
MeasureTheory.abs_measureReal_sub_le_measureReal_symmDiff : ∀ {α : Type u_1} {m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} {s t : Set α} [MeasureTheory.IsFiniteMeasure μ],
  MeasureTheory.NullMeasurableSet s μ →
    MeasureTheory.NullMeasurableSet t μ → |μ.real s - μ.real t| ≤ μ.real (symmDiff s t)
-- Mathlib.Order.Minimal
Minimal.or : ∀ {α : Type u_2} {P Q : α → Prop} {x : α} [inst : LE α], Minimal (fun x => P x ∨ Q x) x → Minimal P x ∨ Minimal Q x
-- Mathlib.Probability.Kernel.Composition.IntegralCompProd
ProbabilityTheory.Kernel.integral_integral_sub' : ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} {E : Type u_4} {mα : MeasurableSpace α} {mβ : MeasurableSpace β}
  {mγ : MeasurableSpace γ} [inst : NormedAddCommGroup E] {a : α} {κ : ProbabilityTheory.Kernel α β}
  [ProbabilityTheory.IsSFiniteKernel κ] {η : ProbabilityTheory.Kernel (α × β) γ} [ProbabilityTheory.IsSFiniteKernel η]
  [inst_3 : NormedSpace ℝ E] ⦃f g : β × γ → E⦄,
  MeasureTheory.Integrable f ((κ.compProd η) a) →
    MeasureTheory.Integrable g ((κ.compProd η) a) →
      ∫ (x : β), ∫ (y : γ), (f - g) (x, y) ∂η (a, x) ∂κ a =
        ∫ (x : β), ∫ (y : γ), f (x, y) ∂η (a, x) ∂κ a - ∫ (x : β), ∫ (y : γ), g (x, y) ∂η (a, x) ∂κ a
-- Mathlib.Order.Category.BddLat
BddLat.hasForgetToLat : CategoryTheory.HasForget₂ BddLat Lat
-- Mathlib.NumberTheory.Pell
Pell.Solution₁.coe_mk : ∀ {d : ℤ} (x y : ℤ) (prop : x ^ 2 - d * y ^ 2 = 1), ↑(Pell.Solution₁.mk x y prop) = { re := x, im := y }
-- Mathlib.Topology.Category.LightProfinite.EffectiveEpi
LightProfinite.effectiveEpi_iff_surjective : ∀ {X Y : LightProfinite} (f : X ⟶ Y),
  CategoryTheory.EffectiveEpi f ↔ Function.Surjective ⇑(CategoryTheory.ConcreteCategory.hom f)
-- Init.Data.Vector.DecidableEq
Vector.instLawfulBEq : ∀ {α : Type u_1} {n : ℕ} [inst : BEq α] [LawfulBEq α], LawfulBEq (Vector α n)
-- Mathlib.Combinatorics.SimpleGraph.Paths
/-- **Alias** of `SimpleGraph.Walk.isPath_map_iff_of_injective`. -/
SimpleGraph.Walk.map_isPath_iff_of_injective : ∀ {V : Type u} {V' : Type v} {G : SimpleGraph V} {G' : SimpleGraph V'} {f : G →g G'} {u v : V} {p : G.Walk u v},
  Function.Injective ⇑f → ((SimpleGraph.Walk.map f p).IsPath ↔ p.IsPath)
-- Init.Data.Array.Lemmas
Array.getElem?_of_mem : ∀ {α : Type u_1} {a : α} {xs : Array α}, a ∈ xs → ∃ i, xs[i]? = some a
-- Mathlib.Topology.Algebra.IsUniformGroup.Basic
IsTopologicalGroup.tendstoUniformly_iff : ∀ {ι : Type u_1} {α : Type u_2} {G : Type u_3} [inst : Group G] [u : UniformSpace G] [inst_1 : IsTopologicalGroup G]
  (F : ι → α → G) (f : α → G) (p : Filter ι),
  IsTopologicalGroup.rightUniformSpace G = u →
    (TendstoUniformly F f p ↔ ∀ u_1 ∈ nhds 1, ∀ᶠ (i : ι) in p, ∀ (a : α), F i a / f a ∈ u_1)
-- Init.Data.String.Lemmas.Pattern.Basic
/-- Predicate stating that the region between the start of the slice `s` and the position
`pos` matches the pattern `pat`, and that there is no longer match starting at the
beginning of the slice. This is what a correct matcher should match.

In some cases, being a match and being a longest match will coincide, see
`String.Slice.Pattern.Model.NoPrefixPatternModel`.
 -/
String.Slice.Pattern.Model.IsLongestRevMatch : {ρ : Type} → (pat : ρ) → [String.Slice.Pattern.Model.PatternModel pat] → {s : String.Slice} → s.Pos → Prop
-- Mathlib.Algebra.Opposites
MulOpposite.unop_zero : ∀ {α : Type u_1} [inst : Zero α], MulOpposite.unop 0 = 0
-- Mathlib.RingTheory.Valuation.ValuationSubring
Valuation.valuationSubring.integers : ∀ {K : Type u} [inst : Field K] {Γ : Type u_1} [inst_1 : LinearOrderedCommGroupWithZero Γ] (v : Valuation K Γ),
  v.Integers ↥v.valuationSubring
-- Mathlib.LinearAlgebra.AffineSpace.Combination
/-- Given a set of points, together with a chosen base point in this set, if we affinely transport
all other members of the set along the line joining them to this base point, the affine span is
unchanged.  -/
affineSpan_eq_affineSpan_lineMap_units : ∀ {k : Type u_2} {V : Type u_3} {P : Type u_4} [inst : Ring k] [inst_1 : AddCommGroup V] [inst_2 : Module k V]
  [inst_3 : AddTorsor V P] [Nontrivial k] {s : Set P} {p : P},
  p ∈ s → ∀ (w : ↑s → kˣ), affineSpan k (Set.range fun q => (AffineMap.lineMap p ↑q) ↑(w q)) = affineSpan k s
-- Mathlib.Analysis.Normed.Module.Completion
UniformSpace.Completion.instNormedAlgebra : (𝕜 : Type u_1) →
  (A : Type u_3) →
    [inst : NormedField 𝕜] →
      [inst_1 : SeminormedCommRing A] → [NormedAlgebra 𝕜 A] → NormedAlgebra 𝕜 (UniformSpace.Completion A)
-- Mathlib.Probability.Kernel.Deterministic
ProbabilityTheory.Kernel.isDeterministic_iff_isZeroOneMeasure : ∀ {α : Type u_1} {β : Type u_2} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} (κ : ProbabilityTheory.Kernel α β)
  [ProbabilityTheory.IsFiniteKernel κ],
  ProbabilityTheory.IsDeterministic κ ↔ ∀ (a : α), MeasureTheory.IsZeroOneMeasure (κ a)
-- Mathlib.SetTheory.Ordinal.Notation
ONote.fundamentalSequence_has_prop : ∀ (o : ONote), o.FundamentalSequenceProp o.fundamentalSequence
-- Mathlib.SetTheory.Cardinal.Cofinality.Basic
/-- If the union of `s` is cofinal and `s` is smaller than the cofinality, then `s` has a cofinal
member.  -/
isCofinal_of_isCofinal_sUnion : ∀ {α : Type u_1} [inst : LinearOrder α] {s : Set (Set α)},
  IsCofinal (⋃₀ s) → Cardinal.mk ↑s < Order.cof α → ∃ x ∈ s, IsCofinal x
-- Mathlib.Algebra.GroupWithZero.Action.ConjAct
ConjAct.smulCommClass₀' : ∀ {α : Type u_1} {G₀ : Type u_2} [inst : GroupWithZero G₀] [inst_1 : SMul α G₀] [SMulCommClass G₀ α G₀]
  [IsScalarTower α G₀ G₀], SMulCommClass (ConjAct G₀) α G₀
-- Mathlib.NumberTheory.AbelSummation
summable_mul_of_bigO_atTop : ∀ {𝕜 : Type u_1} [inst : RCLike 𝕜] (c : ℕ → 𝕜) {f : ℝ → 𝕜},
  (∀ t ∈ Set.Ici 0, DifferentiableAt ℝ (fun x => ‖f x‖) t) →
    MeasureTheory.LocallyIntegrableOn (deriv fun t => ‖f t‖) (Set.Ici 0) MeasureTheory.volume →
      ((fun n => ‖f ↑n‖ * ∑ k ∈ Finset.Icc 0 n, ‖c k‖) =O[Filter.atTop] fun x => 1) →
        ∀ {g : ℝ → ℝ},
          (fun t => deriv (fun t => ‖f t‖) t * ∑ k ∈ Finset.Icc 0 ⌊t⌋₊, ‖c k‖) =O[Filter.atTop] g →
            MeasureTheory.IntegrableAtFilter g Filter.atTop MeasureTheory.volume → Summable fun n => f ↑n * c n
-- Mathlib.Analysis.Convex.Between
wbtw_one_zero_iff : ∀ {R : Type u_1} [inst : Ring R] [inst_1 : PartialOrder R] [IsOrderedRing R] {x : R}, Wbtw R 1 x 0 ↔ x ∈ Set.Icc 0 1
-- Init.Prelude
Nat.succ_sub_succ_eq_sub : ∀ (n m : ℕ), n.succ - m.succ = n - m
-- Lean.Meta.Basic
/-- Function information cache. See `ParamInfo`.
 -/
Lean.Meta.FunInfo : Type
-- Init.System.Platform
/-- Is the current platform macOS?
 -/
System.Platform.isOSX : Bool
-- Mathlib.Probability.Distributions.Gaussian.IsGaussianProcess.Basic
ProbabilityTheory.IsGaussianProcess.restrict : ∀ {T : Type u_2} {Ω : Type u_3} {E : Type u_4} {mΩ : MeasurableSpace Ω} {P : MeasureTheory.Measure Ω} {X : T → Ω → E}
  [inst : NormedAddCommGroup E] [inst_1 : MeasurableSpace E] [BorelSpace E] [inst_3 : NormedSpace ℝ E]
  [SecondCountableTopology E],
  ProbabilityTheory.IsGaussianProcess X P → ∀ (s : Set T), ProbabilityTheory.IsGaussianProcess (fun t => X ↑t) P
-- Mathlib.CategoryTheory.Limits.Types.Coproducts
CategoryTheory.Limits.CofanTypes.isColimit_iff_bijective_fromSigma : ∀ {C : Type u} {F : C → Type v} (c : CategoryTheory.Limits.CofanTypes F),
  CategoryTheory.Functor.CoconeTypes.IsColimit c ↔ Function.Bijective (CategoryTheory.Limits.CofanTypes.fromSigma F c)
-- Init.Data.SInt.Lemmas
Int8.mul_comm : ∀ (a b : Int8), a * b = b * a
-- Mathlib.Order.Bounds.Image
AntitoneOn.image_lowerBounds_subset_upperBounds_image : ∀ {α : Type u} {β : Type v} [inst : Preorder α] [inst_1 : Preorder β] {f : α → β} {s t : Set α},
  AntitoneOn f t → s ⊆ t → f '' (lowerBounds s ∩ t) ⊆ upperBounds (f '' s)
-- Mathlib.Order.RelSeries
/-- Start of a series, i.e. for `a₀ -r→ a₁ -r→ ... -r→ aₙ`, its head is `a₀`.

Since a relation series is assumed to be non-empty, this is well defined.  -/
RelSeries.head : {α : Type u_1} → {r : SetRel α α} → RelSeries r → α
-- Std.Data.DTreeMap.Raw.Basic
/-- Erases multiple mappings from the tree map by iterating over the given collection and calling
`erase`.
 -/
Std.DTreeMap.Raw.eraseMany : {α : Type u} →
  {β : α → Type v} →
    {cmp : α → α → Ordering} → {ρ : Type u_1} → [ForIn Id ρ α] → Std.DTreeMap.Raw α β cmp → ρ → Std.DTreeMap.Raw α β cmp
-- Mathlib.CategoryTheory.Monoidal.Mon
CategoryTheory.MonObj.mul_one_assoc : ∀ {C : Type u₁} {inst : CategoryTheory.Category.{v₁, u₁} C} {inst_1 : CategoryTheory.MonoidalCategory C} (X : C)
  [self : CategoryTheory.MonObj X] {Z : C} (h : X ⟶ Z),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerLeft X CategoryTheory.MonObj.one)
      (CategoryTheory.CategoryStruct.comp CategoryTheory.MonObj.mul h) =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.rightUnitor X).hom h
-- Std.Data.DHashMap.Internal.WF
Std.DHashMap.Internal.Raw₀.get?ₘ_eq_getValueCast? : ∀ {α : Type u} {β : α → Type v} [inst : BEq α] [inst_1 : Hashable α] [inst_2 : LawfulBEq α]
  {m : Std.DHashMap.Internal.Raw₀ α β},
  Std.DHashMap.Internal.Raw.WFImp ↑m →
    ∀ {a : α}, m.get?ₘ a = Std.Internal.List.getValueCast? a (Std.DHashMap.Internal.toListModel (↑m).buckets)
-- Mathlib.AlgebraicTopology.ModelCategory.BifibrantObjectHomotopy
HomotopicalAlgebra.CofibrantObject.HoCat.bifibrantResolution_obj : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : HomotopicalAlgebra.ModelCategory C]
  (X : HomotopicalAlgebra.CofibrantObject C),
  HomotopicalAlgebra.CofibrantObject.HoCat.bifibrantResolution.obj (HomotopicalAlgebra.CofibrantObject.toHoCat.obj X) =
    HomotopicalAlgebra.BifibrantObject.toHoCat.obj X.bifibrantResolutionObj
-- Mathlib.Algebra.Lie.Basic
LieModuleHom.coe_neg : ∀ {R : Type u} {L : Type v} {M : Type w} {N : Type w₁} [inst : CommRing R] [inst_1 : LieRing L]
  [inst_2 : AddCommGroup M] [inst_3 : AddCommGroup N] [inst_4 : Module R M] [inst_5 : Module R N]
  [inst_6 : LieRingModule L M] [inst_7 : LieRingModule L N] (f : M →ₗ⁅R,L⁆ N), ⇑(-f) = -⇑f
-- Mathlib.NumberTheory.LegendreSymbol.QuadraticChar.Basic
/-- Define the quadratic character with values in ℤ on a monoid with zero `α`.
It takes the value zero at zero; for non-zero argument `a : α`, it is `1`
if `a` is a square, otherwise it is `-1`.

This only deserves the name "character" when it is multiplicative,
e.g., when `α` is a finite field. See `quadraticCharFun_mul`.

We will later define `quadraticChar` to be a multiplicative character
of type `MulChar F ℤ`, when the domain is a finite field `F`.
 -/
quadraticCharFun : (α : Type u_1) → [inst : MonoidWithZero α] → [DecidableEq α] → [DecidablePred IsSquare] → α → ℤ
-- Mathlib.Analysis.Complex.Trigonometric
Complex.tan_ofReal_re : ∀ (x : ℝ), (Complex.tan ↑x).re = Real.tan x
-- Init.Meta.Defs
Lean.Syntax.getSepArgs : Lean.Syntax → Array Lean.Syntax
-- Mathlib.Logic.Function.Defs
Function.fst_comp_prod : ∀ {α : Type u_1} {β : Type u_2} {ι : Sort u_3} (f : ι → α) (g : ι → β), Prod.fst ∘ Function.prod f g = f
-- Mathlib.Data.Ordmap.Ordset
/-- O(n). Map a function across a tree, without changing the structure.  -/
Ordset.map : {α : Type u_1} →
  [inst : Preorder α] → {β : Type u_2} → [inst_1 : Preorder β] → (f : α → β) → StrictMono f → Ordset α → Ordset β
-- Mathlib.Tactic.FieldSimp
/-- Build a transparent expression for the product of powers represented by `l : qNF M`.  -/
Mathlib.Tactic.FieldSimp.qNF.evalPrettyMonomial : {v : Lean.Level} →
  {M : Q(Type v)} →
    (iM : Q(GroupWithZero «$M»)) →
      (r : ℤ) → (x : Q(«$M»)) → Lean.MetaM ((e : Q(«$M»)) × Q(Mathlib.Tactic.FieldSimp.zpow' «$x» «$r» = «$e»))
-- Std.Data.DTreeMap.Internal.Lemmas
Std.DTreeMap.Internal.Impl.Const.get?_diff_of_contains_eq_false_left : ∀ {α : Type u} {instOrd : Ord α} {β : Type v} {m₁ m₂ : Std.DTreeMap.Internal.Impl α fun x => β} [Std.TransOrd α]
  (h₁ : m₁.WF),
  m₂.WF →
    ∀ {k : α},
      Std.DTreeMap.Internal.Impl.contains k m₁ = false → Std.DTreeMap.Internal.Impl.Const.get? (m₁.diff m₂ ⋯) k = none
-- Mathlib.RingTheory.Multiplicity
emultiplicity_eq_top : ∀ {α : Type u_1} [inst : Monoid α] {a b : α}, emultiplicity a b = ⊤ ↔ ¬FiniteMultiplicity a b
-- Mathlib.GroupTheory.Perm.Cycle.Type
Equiv.Perm.cycleType_of_card_le_mem_cycleType_add_two : ∀ {α : Type u_1} [inst : Fintype α] [inst_1 : DecidableEq α] {n : ℕ} {g : Equiv.Perm α},
  Fintype.card α < n + 2 → n ∈ g.cycleType → g.cycleType = {n}
-- Mathlib.GroupTheory.GroupAction.Blocks
/-- **Alias** of the forward direction of `MulAction.isBlock_iff_smul_eq_of_nonempty`. -/
MulAction.IsBlock.smul_eq_of_nonempty : ∀ {G : Type u_1} [inst : Group G] {X : Type u_2} [inst_1 : MulAction G X] {B : Set X},
  MulAction.IsBlock G B → ∀ ⦃g : G⦄, (g • B ∩ B).Nonempty → g • B = B
-- Mathlib.Data.Sum.Interval
Sum.instLocallyFiniteOrder : {α : Type u_1} →
  {β : Type u_2} →
    [inst : Preorder α] →
      [inst_1 : Preorder β] → [LocallyFiniteOrder α] → [LocallyFiniteOrder β] → LocallyFiniteOrder (α ⊕ β)
-- Std.Data.DTreeMap.Internal.Lemmas
Std.DTreeMap.Internal.Impl.le_maxKey?_of_mem : ∀ {α : Type u} {β : α → Type v} {instOrd : Ord α} {t : Std.DTreeMap.Internal.Impl α β} [inst : Std.TransOrd α]
  (h : t.WF) {k km : α} (hc : k ∈ t), t.maxKey?.get ⋯ = km → (compare k km).isLE = true
-- Mathlib.NumberTheory.LSeries.PrimesInAP
/-- The auxiliary function agrees on `re s > 1` with the L-series of the von Mangoldt function
restricted to the residue class `a : ZMod q` minus the principal part `(q.totient)⁻¹/(s-1)`
of its pole at `s = 1`.  -/
ArithmeticFunction.vonMangoldt.eqOn_LFunctionResidueClassAux : ∀ {q : ℕ} {a : ZMod q} [inst : NeZero q],
  IsUnit a →
    Set.EqOn (ArithmeticFunction.vonMangoldt.LFunctionResidueClassAux a)
      (fun s => LSeries (fun n => ↑(ArithmeticFunction.vonMangoldt.residueClass a n)) s - (↑q.totient)⁻¹ / (s - 1))
      {s | 1 < s.re}
-- Init.Data.String.Lemmas.Pattern.String.ForwardPattern
_private.Init.Data.String.Lemmas.Pattern.String.ForwardPattern.0.String.Slice.Pattern.BackwardSliceSearcher.skipSuffix?.eq_def : ∀ (pat s : String.Slice),
  String.Slice.Pattern.BackwardSliceSearcher.skipSuffix? pat s =
    if String.Slice.Pattern.BackwardSliceSearcher.endsWith pat s = true then
      some (s.pos! (s.endPos.offset.unoffsetBy pat.rawEndPos))
    else none
-- Std.Data.Iterators.Lemmas.Equivalence.Basic
/-- Equivalence relation on bundled iterators.

Two bundled iterators are equivalent if they have the same `Iterator.IsPlausibleStep` relation
and their step functions are the same *up to equivalence of the successor iterators*. This
coinductive definition captures the idea that the only relevant feature of an iterator is its step
function. Other information retrievable from the iterator -- for example, whether it is a list
iterator or an array iterator -- is totally irrelevant for the equivalence judgement.
 -/
Std.BundledIterM.Equiv : (m : Type w → Type w') →
  (β : Type w) → [inst : Monad m] → [LawfulMonad m] → Std.BundledIterM m β → Std.BundledIterM m β → Prop
-- Mathlib.Algebra.Order.Module.Defs
PosSMulReflectLT.lift : ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} [inst : Preorder α] [inst_1 : Preorder β] [inst_2 : Preorder γ]
  [inst_3 : SMul α β] [inst_4 : SMul α γ] (f : β → γ) [inst_5 : Zero α] [PosSMulReflectLT α γ],
  (∀ {b₁ b₂ : β}, f b₁ ≤ f b₂ ↔ b₁ ≤ b₂) → (∀ (a : α) (b : β), f (a • b) = a • f b) → PosSMulReflectLT α β
-- Mathlib.Topology.ContinuousOn
ContinuousAt.comp₂_continuousWithinAt_of_eq : ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} {δ : Type u_4} [inst : TopologicalSpace α] [inst_1 : TopologicalSpace β]
  [inst_2 : TopologicalSpace γ] [inst_3 : TopologicalSpace δ] {f : β × γ → δ} {g : α → β} {h : α → γ} {x : α}
  {s : Set α} {y : β × γ},
  ContinuousAt f y →
    ContinuousWithinAt g s x →
      ContinuousWithinAt h s x → (g x, h x) = y → ContinuousWithinAt (fun x => f (g x, h x)) s x
-- Lean.Elab.PreDefinition.TerminationHint
/-- Checks that `termination_by` binds at most as many variables are present in the outermost
lambda of `value`, and throws appropriate errors.
 -/
Lean.Elab.TerminationBy.checkVars : Lean.Name → ℕ → Lean.Elab.TerminationBy → Lean.MetaM Unit
-- Mathlib.Probability.StrongLaw
/-- The expectation of the truncated version of `Xᵢ` behaves asymptotically like the whole
expectation. This follows from convergence and Cesàro averaging.  -/
ProbabilityTheory.strong_law_aux3 : ∀ {Ω : Type u_1} [inst : MeasureTheory.MeasureSpace Ω] [MeasureTheory.IsProbabilityMeasure MeasureTheory.volume]
  (X : ℕ → Ω → ℝ),
  MeasureTheory.Integrable (X 0) MeasureTheory.volume →
    (∀ (i : ℕ), ProbabilityTheory.IdentDistrib (X i) (X 0) MeasureTheory.volume MeasureTheory.volume) →
      (fun n =>
          (∫ (a : Ω), (∑ i ∈ Finset.range n, ProbabilityTheory.truncation (X i) ↑i) a) -
            ↑n * ∫ (a : Ω), X 0 a) =o[Filter.atTop]
        Nat.cast
-- Init.Data.Iterators.Basic
Std.Iter.mk.inj : ∀ {α β : Type w} {internalState internalState_1 : α},
  { internalState := internalState } = { internalState := internalState_1 } → internalState = internalState_1
-- Mathlib.Analysis.Convex.Star
/-- If `x < y`, then `(Set.Iic x)ᶜ` is star convex at `y`.  -/
starConvex_compl_Iic : ∀ {𝕜 : Type u_1} {E : Type u_2} [inst : Ring 𝕜] [inst_1 : PartialOrder 𝕜] [inst_2 : AddCommGroup E]
  [inst_3 : PartialOrder E] [IsOrderedAddMonoid E] [inst_5 : Module 𝕜 E] [IsStrictOrderedModule 𝕜 E]
  [PosSMulReflectLT 𝕜 E] {x y : E}, x < y → StarConvex 𝕜 y (Set.Iic x)ᶜ
-- Mathlib.Algebra.Group.Submonoid.Operations
Submonoid.comap_map_comap : ∀ {M : Type u_1} {N : Type u_2} [inst : MulOneClass M] [inst_1 : MulOneClass N] {F : Type u_4} [inst_2 : FunLike F M N]
  [mc : MonoidHomClass F M N] {S : Submonoid N} {f : F},
  Submonoid.comap f (Submonoid.map f (Submonoid.comap f S)) = Submonoid.comap f S
-- Mathlib.CategoryTheory.Limits.Shapes.Pullback.HasPullback
/-- Given such a diagram, then there is a natural morphism `W ×ₛ X ⟶ Y ×ₜ Z`.

```
W ⟶ Y
  ↘   ↘
  S ⟶ T
  ↗   ↗
X ⟶ Z
```
 -/
CategoryTheory.Limits.pullback.map : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    {W X Y Z S T : C} →
      (f₁ : W ⟶ S) →
        (f₂ : X ⟶ S) →
          [inst_1 : CategoryTheory.Limits.HasPullback f₁ f₂] →
            (g₁ : Y ⟶ T) →
              (g₂ : Z ⟶ T) →
                [inst_2 : CategoryTheory.Limits.HasPullback g₁ g₂] →
                  (i₁ : W ⟶ Y) →
                    (i₂ : X ⟶ Z) →
                      (i₃ : S ⟶ T) →
                        CategoryTheory.CategoryStruct.comp f₁ i₃ = CategoryTheory.CategoryStruct.comp i₁ g₁ →
                          CategoryTheory.CategoryStruct.comp f₂ i₃ = CategoryTheory.CategoryStruct.comp i₂ g₂ →
                            (CategoryTheory.Limits.pullback f₁ f₂ ⟶ CategoryTheory.Limits.pullback g₁ g₂)
-- Mathlib.Algebra.Star.NonUnitalSubalgebra
NonUnitalStarAlgebra.mem_sInf : ∀ {R : Type u} {A : Type v} [inst : CommSemiring R] [inst_1 : StarRing R] [inst_2 : NonUnitalSemiring A]
  [inst_3 : StarRing A] [inst_4 : Module R A] [inst_5 : IsScalarTower R A A] [inst_6 : SMulCommClass R A A]
  [inst_7 : StarModule R A] {S : Set (NonUnitalStarSubalgebra R A)} {x : A}, x ∈ sInf S ↔ ∀ p ∈ S, x ∈ p