mathlib-initiative/mathlib-types huggingface dataset:
-- Std.Internal.Do.Triple.SpecLemmas
Std.Internal.Do.Spec.Iter.foldM_filter : ∀ {α β δ : Type w} {n : Type w → Type w'} {Pred EPred : Type w} [inst : Std.Iterator α Id β] [Std.Iterators.Finite α Id]
  [inst_2 : Monad n] [inst_3 : Std.Internal.Do.Assertion Pred] [inst_4 : Std.Internal.Do.Assertion EPred]
  [inst_5 : Std.Internal.Do.WPMonad n Pred EPred] [inst_6 : Std.IteratorLoop α Id n] [Std.LawfulIteratorLoop α Id n]
  {f : β → Bool} {g : δ → β → n δ} {init : δ} {it : Std.Iter β} {P : Pred} {Q : δ → Pred} {eQ : EPred},
  ⦃ P ⦄ Std.Iter.foldM (fun d b => if f b = true then g d b else pure d) init it ⦃ Q; eQ ⦄ →
    ⦃ P ⦄ Std.Iter.foldM g init (Std.Iter.filter f it) ⦃ Q; eQ ⦄
-- Std.Data.HashMap.Lemmas
Std.HashMap.size_insert : ∀ {α : Type u} {β : Type v} {x : BEq α} {x_1 : Hashable α} {m : Std.HashMap α β} [EquivBEq α] [LawfulHashable α] {k : α}
  {v : β}, (m.insert k v).size = if k ∈ m then m.size else m.size + 1
-- Mathlib.MeasureTheory.Function.StronglyMeasurable.Basic
/-- Compositional version of `Finset.stronglyMeasurable_sum` for use by `fun_prop`.  -/
MeasureTheory.StronglyMeasurable.Finset.stronglyMeasurable_sum_apply : ∀ {α : Type u_1} {β : Type u_2} {M : Type u_5} [inst : AddCommMonoid M] [inst_1 : TopologicalSpace M] [ContinuousAdd M]
  {m : MeasurableSpace α} {n : MeasurableSpace β} {ι : Type u_6} {f : ι → α → β → M} {g : α → β} {s : Finset ι},
  (∀ i ∈ s, MeasureTheory.StronglyMeasurable ↿(f i)) →
    Measurable g → MeasureTheory.StronglyMeasurable fun a => (∑ i ∈ s, f i a) (g a)
-- Mathlib.ModelTheory.Basic
FirstOrder.Language.Equiv.instEquivLike : {L : FirstOrder.Language} →
  {M : Type w} → {N : Type w'} → [inst : L.Structure M] → [inst_1 : L.Structure N] → EquivLike (L.Equiv M N) M N
-- Mathlib.Geometry.Euclidean.Sphere.Tangent
EuclideanGeometry.Sphere.IsIntTangentAt.mem_left : ∀ {V : Type u_1} {P : Type u_2} [inst : NormedAddCommGroup V] [inst_1 : InnerProductSpace ℝ V] [inst_2 : MetricSpace P]
  [inst_3 : NormedAddTorsor V P] {s₁ s₂ : EuclideanGeometry.Sphere P} {p : P}, s₁.IsIntTangentAt s₂ p → p ∈ s₁
-- Init.Data.Option.Lemmas
Option.ite_some_none_eq_some : ∀ {α : Type u_1} {p : Prop} {x : Decidable p} {a b : α}, (if p then some a else none) = some b ↔ p ∧ a = b
-- Mathlib.Algebra.Category.HopfAlgCat.Monoidal
HopfAlgCat.rightUnitor_def : ∀ (R : Type u) [inst : CommRing R] (X : HopfAlgCat R),
  CategoryTheory.MonoidalCategoryStruct.rightUnitor X = (Bialgebra.TensorProduct.rid R R X.carrier).toHopfAlgIso
-- Mathlib.Analysis.Convex.Segment
segment_subset_uIcc : ∀ {𝕜 : Type u_1} {E : Type u_2} [inst : Semiring 𝕜] [inst_1 : PartialOrder 𝕜] [inst_2 : AddCommMonoid E]
  [inst_3 : LinearOrder E] [IsOrderedAddMonoid E] [inst_5 : Module 𝕜 E] [PosSMulMono 𝕜 E] (x y : E),
  segment 𝕜 x y ⊆ Set.uIcc x y
-- Mathlib.RingTheory.PowerSeries.Evaluation
PowerSeries.eval₂.eq_1 : ∀ {R : Type u_1} [inst : CommRing R] {S : Type u_2} [inst_1 : CommRing S] (φ : R →+* S) (a : S)
  [inst_2 : UniformSpace R] [inst_3 : UniformSpace S], PowerSeries.eval₂ φ a = MvPowerSeries.eval₂ φ fun x => a
-- Mathlib.LinearAlgebra.RootSystem.Defs
RootPairing.IsOrthogonal.eq_1 : ∀ {ι : 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) (i j : ι),
  P.IsOrthogonal i j = (P.pairing i j = 0 ∧ P.pairing j i = 0)
-- Mathlib.Algebra.Group.Submonoid.Defs
AddSubmonoid.instPartialOrder.eq_1 : ∀ {M : Type u_1} [inst : AddZeroClass M], AddSubmonoid.instPartialOrder = PartialOrder.ofSetLike (AddSubmonoid M) M
-- Mathlib.Algebra.BigOperators.Ring.Finset
/-- If `f = g = h` everywhere but at `i`, where `f i = g i + h i`, then the product of `f` over `s`
is the sum of the products of `g` and `h`.  -/
Finset.prod_add_prod_eq : ∀ {ι : Type u_1} {R : Type u_4} [inst : CommSemiring R] {s : Finset ι} {i : ι} {f g h : ι → R},
  i ∈ s →
    g i + h i = f i →
      (∀ j ∈ s, j ≠ i → g j = f j) → (∀ j ∈ s, j ≠ i → h j = f j) → ∏ i ∈ s, g i + ∏ i ∈ s, h i = ∏ i ∈ s, f i
-- Lean.Compiler.LCNF.Basic
Lean.Compiler.LCNF.Code.oset : {pu : Lean.Compiler.LCNF.Purity} →
  Lean.FVarId →
    ℕ →
      Lean.Compiler.LCNF.Arg pu →
        Lean.Compiler.LCNF.Code pu →
          autoParam (pu = Lean.Compiler.LCNF.Purity.impure) Lean.Compiler.LCNF.Alt._auto_7 → Lean.Compiler.LCNF.Code pu
-- Mathlib.Algebra.Group.Submonoid.Membership
Submonoid.powers_one : ∀ {M : Type u_1} [inst : Monoid M], Submonoid.powers 1 = ⊥
-- Mathlib.CategoryTheory.Bicategory.Free
CategoryTheory.FreeBicategory.Rel.below.comp_whisker_left : ∀ {B : Type u} [inst : Quiver B]
  {motive :
    {a b : CategoryTheory.FreeBicategory B} →
      {f g : a ⟶ b} →
        (a_1 a_2 : CategoryTheory.FreeBicategory.Hom₂ f g) → CategoryTheory.FreeBicategory.Rel a_1 a_2 → Prop}
  {a b c d : B} (f : CategoryTheory.FreeBicategory.Hom a b) (g : CategoryTheory.FreeBicategory.Hom b c)
  {h h' : CategoryTheory.FreeBicategory.Hom c d} (η : CategoryTheory.FreeBicategory.Hom₂ h h'),
  CategoryTheory.FreeBicategory.Rel.below ⋯
-- Mathlib.Topology.Algebra.Module.Multilinear.Basic
ContinuousMultilinearMap.linearDeriv.eq_1 : ∀ {R : Type u} {ι : Type v} {M₁ : ι → Type w₁} {M₂ : Type w₂} [inst : Semiring R]
  [inst_1 : (i : ι) → AddCommMonoid (M₁ i)] [inst_2 : AddCommMonoid M₂] [inst_3 : (i : ι) → Module R (M₁ i)]
  [inst_4 : Module R M₂] [inst_5 : (i : ι) → TopologicalSpace (M₁ i)] [inst_6 : TopologicalSpace M₂]
  (f : ContinuousMultilinearMap R M₁ M₂) [inst_7 : ContinuousAdd M₂] [inst_8 : DecidableEq ι] [inst_9 : Fintype ι]
  (x : (i : ι) → M₁ i), f.linearDeriv x = ∑ i, f.toContinuousLinearMap x i ∘SL ContinuousLinearMap.proj i
-- Mathlib.Combinatorics.Matroid.Basic
Matroid.mk.sizeOf_spec : ∀ {α : Type u_1} [inst : SizeOf α] (E : Set α) (IsBase Indep : Set α → Prop)
  (indep_iff' : ∀ ⦃I : Set α⦄, Indep I ↔ ∃ B, IsBase B ∧ I ⊆ B) (exists_isBase : ∃ B, IsBase B)
  (isBase_exchange : Matroid.ExchangeProperty IsBase)
  (maximality : ∀ X ⊆ E, Matroid.ExistsMaximalSubsetProperty Indep X) (subset_ground : ∀ (B : Set α), IsBase B → B ⊆ E),
  sizeOf
      { E := E, IsBase := IsBase, Indep := Indep, indep_iff' := indep_iff', exists_isBase := exists_isBase,
        isBase_exchange := isBase_exchange, maximality := maximality, subset_ground := subset_ground } =
    1 + sizeOf exists_isBase
-- Mathlib.Combinatorics.SimpleGraph.DegreeSum
/-- The degree-sum formula only counting over the vertices that form edges.

See `SimpleGraph.sum_degrees_eq_twice_card_edges` for the general version.  -/
SimpleGraph.sum_degrees_support_eq_twice_card_edges : ∀ {V : Type u} (G : SimpleGraph V) [inst : Fintype V] [inst_1 : DecidableRel G.Adj],
  ∑ v ∈ G.support.toFinset, G.degree v = 2 * G.edgeFinset.card
-- Init.Data.List.Sort.Basic
_private.Init.Data.List.Sort.Basic.0.List.merge.match_1.eq_2 : ∀ {α : Type u_1} (motive : List α → List α → Sort u_2) (xs : List α) (h_1 : (ys : List α) → motive [] ys)
  (h_2 : (xs : List α) → motive xs [])
  (h_3 : (x : α) → (xs : List α) → (y : α) → (ys : List α) → motive (x :: xs) (y :: ys)),
  (xs = [] → False) →
    (match xs, [] with
      | [], ys => h_1 ys
      | xs, [] => h_2 xs
      | x :: xs, y :: ys => h_3 x xs y ys) =
      h_2 xs
-- Init.Data.Sum.Lemmas
Sum.lex_acc_inr : ∀ {α : Type u_1} {r : α → α → Prop} {β : Type u_2} {s : β → β → Prop},
  (∀ (a : α), Acc (Sum.Lex r s) (Sum.inl a)) → ∀ {b : β}, Acc s b → Acc (Sum.Lex r s) (Sum.inr b)
-- Mathlib.GroupTheory.MonoidLocalization.Away
/-- Given `x : A` and a Localization map `F : A →+ B` away from `x`, `neg_self` is `- (F x)`.  -/
AddSubmonoid.LocalizationMap.AwayMap.negSelf : {A : Type u_4} →
  [inst : AddCommMonoid A] →
    (x : A) → {B : Type u_5} → [inst_1 : AddCommMonoid B] → AddSubmonoid.LocalizationMap.AwayMap x B → B
-- Mathlib.CategoryTheory.Limits.Final
CategoryTheory.Functor.final_natIso_iff : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  {F F' : CategoryTheory.Functor C D} (i : F ≅ F'), F.Final ↔ F'.Final
-- Mathlib.AlgebraicTopology.DoldKan.Projections
AlgebraicTopology.DoldKan.HigherFacesVanish.comp_P_eq_self : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Preadditive C]
  {X : CategoryTheory.SimplicialObject C} {Y : C} {n q : ℕ} {φ : Y ⟶ X.obj (Opposite.op { len := n + 1 })},
  AlgebraicTopology.DoldKan.HigherFacesVanish q φ →
    CategoryTheory.CategoryStruct.comp φ ((AlgebraicTopology.DoldKan.P q).f (n + 1)) = φ
-- Lean.Meta.Tactic.Simp.BuiltinSimprocs.Char
Char.reduceToString : Lean.Meta.Simp.DSimproc
-- Mathlib.AlgebraicTopology.SingularHomology.Basic
/-- The zeroth singular homology of a totally disconnected space is the
free `R`-module generated by elements of `X`.  -/
AlgebraicTopology.singularHomologyFunctorZeroOfTotallyDisconnectedSpace : (C : Type u) →
  [inst : CategoryTheory.Category.{v, u} C] →
    [inst_1 : CategoryTheory.Limits.HasCoproducts C] →
      [inst_2 : CategoryTheory.Preadditive C] →
        (R : C) →
          (X : TopCat) →
            [TotallyDisconnectedSpace ↑X] →
              [inst_4 : CategoryTheory.CategoryWithHomology C] →
                ((AlgebraicTopology.singularHomologyFunctor C 0).obj R).obj X ≅ ∐ fun x => R
-- Std.Data.DTreeMap.Internal.Operations
/-- Transforms a list of mappings into a tree map.  -/
Std.DTreeMap.Internal.Impl.Const.unitOfArray : {α : Type u} → [Ord α] → Array α → Std.DTreeMap.Internal.Impl α fun x => Unit
-- Mathlib.Order.Nucleus
/-- A nucleus is increasing.

Do not use this directly. Instead use `NucleusClass.le_apply`.  -/
Nucleus.le_apply' : ∀ {X : Type u_2} [inst : SemilatticeInf X] (self : Nucleus X) (x : X), x ≤ self.toFun x
-- Mathlib.Algebra.Free
/-- Recursor for free additive semigroup using `of` and `+`.  -/
FreeAddSemigroup.recOnAdd : {α : Type u} →
  {C : FreeAddSemigroup α → Sort l} →
    (x : FreeAddSemigroup α) →
      ((x : α) → C (FreeAddSemigroup.of x)) →
        ((x : α) → (y : FreeAddSemigroup α) → C (FreeAddSemigroup.of x) → C y → C (FreeAddSemigroup.of x + y)) → C x
-- Mathlib.Analysis.Normed.Module.RCLike.Extend
StrongDual.extendRCLikeₗᵢ_apply : ∀ {𝕜 : Type u_1} {F : Type u_3} [inst : RCLike 𝕜] [inst_1 : SeminormedAddCommGroup F] [inst_2 : NormedSpace 𝕜 F]
  [inst_3 : NormedSpace ℝ F] [inst_4 : IsScalarTower ℝ 𝕜 F] (fr : StrongDual ℝ F),
  StrongDual.extendRCLikeₗᵢ fr = fr.extendRCLike
-- Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Rpow.Basic
CFC.isUnit_rpow_iff : ∀ {A : Type u_1} [inst : PartialOrder A] [inst_1 : Ring A] [inst_2 : StarRing A] [inst_3 : TopologicalSpace A]
  [inst_4 : StarOrderedRing A] [inst_5 : Algebra ℝ A] [inst_6 : ContinuousFunctionalCalculus ℝ A IsSelfAdjoint]
  [inst_7 : NonnegSpectrumClass ℝ A] (a : A) (y : ℝ),
  y ≠ 0 → autoParam (0 ≤ a) CFC.isUnit_rpow_iff._auto_1 → (IsUnit (a ^ y) ↔ IsUnit a)
-- Mathlib.CategoryTheory.Triangulated.TStructure.Basic
/-- The full subcategory consisting of `t`-bounded below objects.  -/
CategoryTheory.Triangulated.TStructure.plus : {C : Type u_1} →
  [inst : CategoryTheory.Category.{v_1, u_1} C] →
    [inst_1 : CategoryTheory.Preadditive C] →
      [inst_2 : CategoryTheory.Limits.HasZeroObject C] →
        [inst_3 : CategoryTheory.HasShift C ℤ] →
          [inst_4 : ∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive] →
            [inst_5 : CategoryTheory.Pretriangulated C] →
              CategoryTheory.Triangulated.TStructure C → CategoryTheory.ObjectProperty C
-- Mathlib.Algebra.Order.Interval.Finset.SuccPred
Finset.Ioi_sub_one_eq_Ici_of_not_isMin : ∀ {α : Type u_2} [inst : LinearOrder α] [inst_1 : One α] [inst_2 : LocallyFiniteOrderTop α] [inst_3 : Sub α]
  [PredSubOrder α] {a : α}, ¬IsMin a → Finset.Ioi (a - 1) = Finset.Ici a
-- Lean.Meta.Tactic.Grind.Arith.Linear.Types
/-- `LE` instance if available  -/
Lean.Meta.Grind.Arith.Linear.NatStruct.leInst? : Lean.Meta.Grind.Arith.Linear.NatStruct → Option Lean.Expr
-- Mathlib.MeasureTheory.Measure.Restrict
MeasureTheory.Measure.volume_subtype_coe_le_volume : ∀ {δ : Type u_4} {u : Set δ} [inst : MeasureTheory.MeasureSpace δ],
  MeasureTheory.NullMeasurableSet u MeasureTheory.volume →
    ∀ (t : Set ↑u), MeasureTheory.volume (Subtype.val '' t) ≤ MeasureTheory.volume t
-- Mathlib.NumberTheory.FactorisationProperties
Nat.Perfect.pseudoperfect : ∀ {n : ℕ}, n.Perfect → n.Pseudoperfect
-- Mathlib.RingTheory.LocalProperties.Basic
Ideal.mem_of_localization_maximal : ∀ {R : Type u_1} [inst : CommSemiring R] {r : R} {J : Ideal R},
  (∀ (P : Ideal R) (x : P.IsMaximal),
      (algebraMap R (Localization.AtPrime P)) r ∈ Ideal.map (algebraMap R (Localization.AtPrime P)) J) →
    r ∈ J
-- Mathlib.Algebra.Group.Defs
nsmul_add_comm : ∀ {M : Type u_2} [inst : AddMonoid M] (a : M) (m n : ℕ), m • a + n • a = n • a + m • a
-- Mathlib.Analysis.Calculus.ContDiff.Operations
iteratedFDerivWithin_fun_sum_apply : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type uE} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {F : Type uF} [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F] {s : Set E}
  {ι : Type u_3} {f : ι → E → F} {u : Finset ι} {i : ℕ} {x : E},
  UniqueDiffOn 𝕜 s →
    x ∈ s →
      (∀ j ∈ u, ContDiffWithinAt 𝕜 (↑i) (f j) s x) →
        iteratedFDerivWithin 𝕜 i (fun z => ∑ j ∈ u, f j z) s x = ∑ j ∈ u, iteratedFDerivWithin 𝕜 i (f j) s x
-- Mathlib.RingTheory.HahnSeries.PowerSeries
HahnSeries.ofPowerSeriesAlg_apply_coeff : ∀ (Γ : Type u_1) (R : Type u_2) [inst : CommSemiring R] {A : Type u_3} [inst_1 : Semiring A] [inst_2 : Algebra R A]
  [inst_3 : Semiring Γ] [inst_4 : PartialOrder Γ] [inst_5 : IsStrictOrderedRing Γ] (x : PowerSeries A) (b : Γ),
  ((HahnSeries.ofPowerSeriesAlg Γ R) x).coeff b =
    if h : b ∈ Nat.cast '' ((HahnSeries.toPowerSeriesAlg R).symm x).support then
      (PowerSeries.coeff (Classical.choose ⋯)) x
    else 0
-- Mathlib.CategoryTheory.LocallyCartesianClosed.Over
CategoryTheory.ChosenPullbacksAlong.Over.associator_hom_left_snd_snd : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.ChosenPullbacks C] {X : C}
  (R S T : CategoryTheory.Over X),
  CategoryTheory.CategoryStruct.comp
      (CategoryTheory.Over.Hom.left (CategoryTheory.MonoidalCategoryStruct.associator R S T).hom)
      (CategoryTheory.CategoryStruct.comp
        (CategoryTheory.ChosenPullbacksAlong.snd R.hom
          (CategoryTheory.CategoryStruct.comp (CategoryTheory.ChosenPullbacksAlong.snd S.hom T.hom) T.hom))
        (CategoryTheory.ChosenPullbacksAlong.snd S.hom T.hom)) =
    CategoryTheory.ChosenPullbacksAlong.snd (CategoryTheory.MonoidalCategoryStruct.tensorObj R S).hom T.hom
-- Mathlib.Order.Lattice
/-- **Alias** of the forward direction of `sup_eq_right`. -/
le_of_sup_eq : ∀ {α : Type u} [inst : SemilatticeSup α] {a b : α}, a ⊔ b = b → a ≤ b
-- Mathlib.RingTheory.Polynomial.UniversalFactorizationRing
/-- `MonicDegreeEq · n` is representable by `R[X₁,...,Xₙ]`,
with the universal element being `freeMonic`.  -/
MvPolynomial.mapEquivMonic : (R : Type u_1) →
  (S : Type u_2) →
    [inst : CommRing R] →
      [inst_1 : CommRing S] →
        [inst_2 : Algebra R S] → (n : ℕ) → (MvPolynomial (Fin n) R →ₐ[R] S) ≃ Polynomial.MonicDegreeEq S n
-- Mathlib.Order.Concept
/-- A set is an extent when either of the following equivalent definitions holds:

- The `lowerPolar` of its `upperPolar` is itself.
- The set is the `lowerPolar` of some other set.

The latter is used as a definition, but one can rewrite using the former via `IsExtent.eq`.
 -/
Order.IsExtent : {α : Type u_2} → {β : Type u_3} → (α → β → Prop) → Set α → Prop
-- Mathlib.GroupTheory.GroupAction.DomAct.Basic
DomAddAct.instNonAssocSemiringOfAddOpposite : {M : Type u_1} → [NonAssocSemiring Mᵃᵒᵖ] → NonAssocSemiring Mᵈᵃᵃ
-- Mathlib.Algebra.Order.Floor.Div
le_floorDiv_iff_smul_le : ∀ {α : Type u_2} {β : Type u_3} [inst : AddCommMonoid α] [inst_1 : PartialOrder α] [inst_2 : AddCommMonoid β]
  [inst_3 : PartialOrder β] [inst_4 : SMulZeroClass α β] [inst_5 : FloorDiv α β] {a : α} {b c : β},
  0 < a → (c ≤ b ⌊/⌋ a ↔ a • c ≤ b)
-- Mathlib.NumberTheory.NumberField.CanonicalEmbedding.FundamentalCone
/-- For an integer `n`, The equivalence between the elements of `idealSet K` of norm `n` and
the product of the set of nonzero principal ideals of `K` divisible by `J` of norm `n` and the
torsion of `K`.  -/
NumberField.mixedEmbedding.fundamentalCone.idealSetEquivNorm : (K : Type u_1) →
  [inst : Field K] →
    [inst_1 : NumberField K] →
      (J : ↥(nonZeroDivisors (Ideal (NumberField.RingOfIntegers K)))) →
        (n : ℕ) →
          { a // NumberField.mixedEmbedding.norm ↑a = ↑n } ≃
            { I // ↑J ∣ ↑I ∧ Submodule.IsPrincipal ↑I ∧ Ideal.absNorm ↑I = n } × ↥(NumberField.Units.torsion K)
-- Mathlib.Computability.ContextFreeGrammar
ContextFreeRule.ext_iff : ∀ {T : Type u_1} {N : Type u_2} {x y : ContextFreeRule T N}, x = y ↔ x.input = y.input ∧ x.output = y.output
-- Aesop.Forward.State.ApplyGoalDiff
_private.Aesop.Forward.State.ApplyGoalDiff.0.Aesop.ForwardState.applyGoalDiff.eraseHyp : Lean.FVarId → Aesop.ForwardState → Aesop.BaseM Aesop.ForwardState
-- Mathlib.Topology.MetricSpace.Basic
PseudoMetricSpace.replaceDist_eq : ∀ {X : Type u_2} (m : PseudoMetricSpace X) (d : X → X → ℝ) (hd : d = dist), m.replaceDist d hd = m
-- Mathlib.Analysis.Analytic.Linear
ContinuousLinearMap.fpowerSeries_radius : ∀ {𝕜 : 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 →L[𝕜] F)
  (x : E), (f.fpowerSeries x).radius = ⊤
-- Mathlib.Algebra.SkewMonoidAlgebra.Support
SkewMonoidAlgebra.support_single_subset : ∀ {k : Type u_1} {G : Type u_2} [inst : AddCommMonoid k] {a : G} {b : k}, (SkewMonoidAlgebra.single a b).support ⊆ {a}
-- Mathlib.Analysis.SpecialFunctions.Exp
/-- `Real.exp (f x)` is bounded away from zero along a filter if and only if this filter is bounded
from below under `f`.  -/
Real.isBigO_one_exp_comp : ∀ {α : Type u_1} {l : Filter α} {f : α → ℝ},
  ((fun x => 1) =O[l] fun x => Real.exp (f x)) ↔ Filter.IsBoundedUnder (fun x1 x2 => x1 ≥ x2) l f
-- Mathlib.RingTheory.FractionalIdeal.Basic
FractionalIdeal.coe_mul : ∀ {R : Type u_1} [inst : CommRing R] {S : Submonoid R} {P : Type u_2} [inst_1 : CommRing P] [inst_2 : Algebra R P]
  (I J : FractionalIdeal S P), ↑(I * J) = ↑I * ↑J
-- Mathlib.Data.Finset.Lattice.Lemmas
Finset.union_singleton : ∀ {α : Type u_1} [inst : DecidableEq α] (x : α) (s : Finset α), s ∪ {x} = insert x s
-- Mathlib.NumberTheory.Padics.PadicIntegers
PadicInt.instIsAdicCompleteMaximalIdeal : ∀ {p : ℕ} [hp : Fact (Nat.Prime p)], IsAdicComplete (IsLocalRing.maximalIdeal ℤ_[p]) ℤ_[p]
-- Init.Data.String.Pattern.String
_private.Init.Data.String.Pattern.String.0.String.Slice.Pattern.ForwardSliceSearcher.toOption : {s : String.Slice} → String.Slice.Pattern.ForwardSliceSearcher s → Option (ℕ × ℕ)
-- Mathlib.RingTheory.PiTensorProduct
PiTensorProduct.instCommRing : {ι : Type u_1} →
  {R : Type u_3} →
    {A : ι → Type u_4} →
      [inst : CommRing R] →
        [inst_1 : (i : ι) → CommRing (A i)] →
          [inst_2 : (i : ι) → Algebra R (A i)] → CommRing (PiTensorProduct R fun i => A i)
-- Lean.Meta.CollectMVars
Lean.Meta.collectMVarsAtDecl : Lean.Declaration → StateRefT' IO.RealWorld Lean.CollectMVars.State Lean.MetaM Unit
-- Init.Data.String.Lemmas.Pattern.String.ForwardSearcher
_private.Init.Data.String.Lemmas.Pattern.String.ForwardSearcher.0.String.Slice.Pattern.Model.ForwardSliceSearcher.matchesAt_iff_partialMatch : ∀ {pat s : String.Slice},
  pat.isEmpty = false →
    ∀ {pos : s.Pos},
      String.Slice.Pattern.Model.MatchesAt pat pos ↔
        String.Slice.Pattern.Model.ForwardSliceSearcher.PartialMatch✝ pat.copy.toByteArray s.copy.toByteArray
          pat.copy.toByteArray.size (pos.offset.byteIdx + pat.copy.toByteArray.size)
-- Init.Data.Nat.Bitwise.Lemmas
Nat.instLawfulCommIdentityHXorOfNat : Std.LawfulCommIdentity (fun x1 x2 => x1 ^^^ x2) 0
-- Mathlib.InformationTheory.Coding.KraftMcMillan
/-- **Kraft-McMillan Inequality**: If `S` is a finite uniquely decodable code,
then `Σ D^{-|w|} ≤ 1`.  -/
InformationTheory.kraft_mcmillan_inequality : ∀ {α : Type u_1} {S : Finset (List α)} [inst : Fintype α] [Nonempty α],
  InformationTheory.UniquelyDecodable ↑S → ∑ w ∈ S, (1 / ↑(Fintype.card α)) ^ w.length ≤ 1
-- Mathlib.Data.Vector.Snoc
List.Vector.cons.eq_1 : ∀ {α : Type u_1} {n : ℕ} (x : α) (v : List α) (h : v.length = n), x ::ᵥ ⟨v, h⟩ = ⟨x :: v, ⋯⟩
-- Init.Data.AC
Lean.Data.AC.Variable.mk.inj : ∀ {α : Sort u} {op : α → α → α} {value : α} {neutral : Option (PLift (Std.LawfulIdentity op value))} {value_1 : α}
  {neutral_1 : Option (PLift (Std.LawfulIdentity op value_1))},
  { value := value, neutral := neutral } = { value := value_1, neutral := neutral_1 } →
    value = value_1 ∧ neutral ≍ neutral_1
-- Mathlib.LinearAlgebra.RootSystem.GeckConstruction.Basic
RootPairing.GeckConstruction.h_mem_lieAlgebra : ∀ {ι : 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}
  [inst_5 : P.IsCrystallographic] {b : P.Base} [inst_6 : Finite ι] [inst_7 : IsDomain R] [inst_8 : CharZero R]
  [inst_9 : Fintype ι] [inst_10 : DecidableEq ι] (i : ↥b.support),
  RootPairing.GeckConstruction.h i ∈ RootPairing.GeckConstruction.lieAlgebra b
-- Mathlib.GroupTheory.Index
AddSubgroup.finiteIndex_iff_finite_quotient : ∀ {G : Type u_1} [inst : AddGroup G] {H : AddSubgroup G}, H.FiniteIndex ↔ Finite (G ⧸ H)
-- Batteries.Data.Fin.Coding
Fin.decodeSigma_encodeSigma : ∀ {n : ℕ} (f : Fin n → ℕ) (x : (i : Fin n) × Fin (f i)), Fin.decodeSigma f (Fin.encodeSigma f x) = x
-- Mathlib.CategoryTheory.Pi.Basic
CategoryTheory.Equivalence.instIsEquivalenceForallPi : ∀ {I : Type w₀} {C : I → Type u₁} [inst : (i : I) → CategoryTheory.Category.{v₁, u₁} (C i)] {D : I → Type u₂}
  [inst_1 : (i : I) → CategoryTheory.Category.{v₂, u₂} (D i)] (F : (i : I) → CategoryTheory.Functor (C i) (D i))
  [∀ (i : I), (F i).IsEquivalence], (CategoryTheory.Functor.pi F).IsEquivalence
-- Mathlib.Topology.Algebra.UniformConvergence
UniformOnFun.toFun_smul : ∀ {α : Type u_1} {β : Type u_2} {𝔖 : Set (Set α)} {M : Type u_5} [inst : SMul M β] (c : M) (f : UniformOnFun α β 𝔖),
  (UniformOnFun.toFun 𝔖) (c • f) = c • (UniformOnFun.toFun 𝔖) f
-- Mathlib.CategoryTheory.Galois.EssSurj
_private.Mathlib.CategoryTheory.Galois.EssSurj.0.CategoryTheory.PreGaloisCategory.coconeQuotientDiag_pt : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{u₂, u₁} C] {F : CategoryTheory.Functor C FintypeCat}
  [inst_1 : CategoryTheory.GaloisCategory C] [inst_2 : CategoryTheory.PreGaloisCategory.FiberFunctor F]
  {V U : OpenSubgroup (CategoryTheory.Aut F)} (h : (↑U).Normal) {A : C}
  (u :
    (CategoryTheory.PreGaloisCategory.functorToAction F).obj A ≅
      Action.FintypeCat.ofMulAction (CategoryTheory.Aut F) (FintypeCat.of (CategoryTheory.Aut F ⧸ ↑U)))
  (hUinV : U ≤ V),
  (CategoryTheory.PreGaloisCategory.coconeQuotientDiag✝ h u hUinV).pt =
    Action.FintypeCat.ofMulAction (CategoryTheory.Aut F) (FintypeCat.of (CategoryTheory.Aut F ⧸ ↑V))
-- Mathlib.Algebra.Group.Submonoid.Membership
IsIdempotentElem.coe_powers : ∀ {M : Type u_1} [inst : Monoid M] {a : M}, IsIdempotentElem a → ↑(Submonoid.powers a) = {1, a}
-- Mathlib.CategoryTheory.Sites.IsSheafFor
CategoryTheory.Presieve.shrinkFunctor_ι_comp_eq_iff_isAmalgamation : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {X : C} {S : CategoryTheory.Sieve X}
  [inst_1 : CategoryTheory.LocallySmall.{w, v₁, u₁} C] (F : CategoryTheory.Functor Cᵒᵖ (Type w))
  (f : (CategoryTheory.Sieve.shrinkFunctor.{w, v₁, u₁} S).toFunctor ⟶ F)
  (g : CategoryTheory.shrinkYoneda.{w, v₁, u₁}.obj X ⟶ F),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.Sieve.shrinkFunctor.{w, v₁, u₁} S).ι g = f ↔
    (↑(CategoryTheory.Presieve.shrinkFunctorHomEquiv f)).IsAmalgamation (CategoryTheory.shrinkYonedaEquiv g)
-- Mathlib.Algebra.Order.Archimedean.Real.Basic
Real.sSup_def : ∀ (s : Set ℝ), sSup s = if h : s.Nonempty ∧ BddAbove s then Classical.choose ⋯ else 0
-- Mathlib.Tactic.DuplicateDecls
_private.Mathlib.Tactic.DuplicateDecls.0.Mathlib.Tactic.DuplicateDecls.isAlias.isConstBVarApp : Lean.Expr → Bool