mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Algebra.Module.Torsion.Basic
/-- Torsion by a set is torsion by the ideal generated by it.  -/
Submodule.torsionBySet_eq_torsionBySet_span : ∀ {R : Type u_1} {M : Type u_2} [inst : CommSemiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M] (s : Set R),
  Submodule.torsionBySet R M s = Submodule.torsionBySet R M ↑(Ideal.span s)
-- Std.Do.WP.Monad
_private.Std.Do.WP.Monad.0.Option.elim.match_1.splitter : {α : Type u_1} →
  {β : Sort u_3} →
    (motive : Option α → β → (α → β) → Sort u_2) →
      (x : Option α) →
        (x_1 : β) →
          (x_2 : α → β) →
            ((x : α) → (x_3 : β) → (f : α → β) → motive (some x) x_3 f) →
              ((y : β) → (x : α → β) → motive none y x) → motive x x_1 x_2
-- Mathlib.Analysis.SpecialFunctions.Pow.Real
Real.self_le_rpow_of_one_le : ∀ {x y : ℝ}, 1 ≤ x → 1 ≤ y → x ≤ x ^ y
-- Mathlib.Logic.Encodable.Basic
Encodable.decode_ge_two : ∀ (n : ℕ), 2 ≤ n → Encodable.decode n = none
-- Mathlib.Topology.Algebra.UniformConvergence
instAddCommMonoidUniformFun.eq_1 : ∀ {α : Type u_1} {β : Type u_2} [inst : AddCommMonoid β],
  instAddCommMonoidUniformFun = { toAddMonoid := instAddMonoidUniformFun, add_comm := ⋯ }
-- Mathlib.Topology.Algebra.Module.Complement
ContinuousLinearMap.ofIsTopCompl_apply_left : ∀ {R : Type u_1} [inst : Ring R] {E : Type u_2} {F : Type u_3} [inst_1 : TopologicalSpace E] [inst_2 : AddCommGroup E]
  [inst_3 : Module R E] [inst_4 : IsTopologicalAddGroup E] [inst_5 : TopologicalSpace F] [inst_6 : AddCommGroup F]
  [inst_7 : Module R F] [inst_8 : ContinuousAdd F] {p q : Submodule R E} (h : Submodule.IsTopCompl p q) (φ : ↥p →L[R] F)
  (ψ : ↥q →L[R] F) (x : ↥p), (ContinuousLinearMap.ofIsTopCompl h φ ψ) ↑x = φ x
-- Lean.Meta.Sym.Pattern
_private.Lean.Meta.Sym.Pattern.0.Lean.Meta.Sym.pushLevelPending : Lean.Level → Lean.Level → Lean.Meta.Sym.UnifyM✝ Unit
-- Mathlib.CategoryTheory.Limits.Filtered
CategoryTheory.Limits.hasCofilteredLimitsOfSize_shrink : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C]
  [CategoryTheory.Limits.HasCofilteredLimitsOfSize.{max w' w₂', max w w₂, v, u} C],
  CategoryTheory.Limits.HasCofilteredLimitsOfSize.{w', w, v, u} C
-- Mathlib.MeasureTheory.MeasurableSpace.Instances
IterateMulAct.instMeasurableSpace.eq_1 : ∀ {α : Type u_1} {f : α → α}, IterateMulAct.instMeasurableSpace = ⊤
-- Init.Data.List.Basic
List.zip_nil_right : ∀ {α : Type u} {β : Type v} {l : List α}, l.zip [] = []
-- Mathlib.Algebra.Notation.Indicator
Set.indicator_const_preimage_eq_union : ∀ {α : Type u_1} {M : Type u_3} [inst : Zero M] (U : Set α) (s : Set M) (a : M) [inst_1 : Decidable (a ∈ s)]
  [inst_2 : Decidable (0 ∈ s)], (U.indicator fun x => a) ⁻¹' s = (if a ∈ s then U else ∅) ∪ if 0 ∈ s then Uᶜ else ∅
-- Mathlib.Algebra.Group.Invertible.Basic
IsUnit.nonempty_invertible : ∀ {α : Type u} [inst : Monoid α] {a : α}, IsUnit a → Nonempty (Invertible a)
-- Mathlib.Algebra.BigOperators.RingEquiv
/-- An isomorphism into the opposite ring acts on the product by acting on the reversed elements  -/
RingEquiv.unop_map_list_prod : ∀ {R : Type u_2} {S : Type u_3} [inst : Semiring R] [inst_1 : Semiring S] (f : R ≃+* Sᵐᵒᵖ) (l : List R),
  MulOpposite.unop (f l.prod) = (List.map (MulOpposite.unop ∘ ⇑f) l).reverse.prod
-- Mathlib.RingTheory.DedekindDomain.Different
differentIdeal_ne_bot : ∀ {A : Type u_1} {B : Type u_3} [inst : CommRing A] [inst_1 : CommRing B] [inst_2 : Algebra A B] [inst_3 : IsDomain A]
  [IsIntegrallyClosed A] [inst_5 : IsDedekindDomain B] [inst_6 : Module.IsTorsionFree A B] [Module.Finite A B]
  [Algebra.IsSeparable (FractionRing A) (FractionRing B)], differentIdeal A B ≠ ⊥
-- Init.Data.String.Lemmas.Pattern.Basic
String.Slice.Pattern.Model.NoPrefixPatternModel.of_length_toList_eq : ∀ {ρ : Type} {pat : ρ} [inst : String.Slice.Pattern.Model.PatternModel pat],
  (∀ (s t : String),
      String.Slice.Pattern.Model.PatternModel.Matches pat s →
        String.Slice.Pattern.Model.PatternModel.Matches pat t → s.toList.length = t.toList.length) →
    String.Slice.Pattern.Model.NoPrefixPatternModel pat
-- Mathlib.RingTheory.Ideal.Height
_private.Mathlib.RingTheory.Ideal.Height.0.Ideal.primeHeight_add_one_le_of_lt : ∀ {R : Type u_1} [inst : CommRing R] {I J : Ideal R} [inst_1 : I.IsPrime] [inst_2 : J.IsPrime],
  I < J → Ideal.primeHeight✝ I + 1 ≤ Ideal.primeHeight✝ J
-- Lean.Util.ReplaceLevel
Lean.Expr.ReplaceLevelImpl.ReplaceM : Type → Type
-- Lean.Data.Lsp.Internal
Lean.Lsp.RefIdent.instToJson : Lean.ToJson Lean.Lsp.RefIdent
-- Std.Data.TreeMap.Lemmas
Std.TreeMap.Equiv.beq_congr : ∀ {α : Type u} {cmp : α → α → Ordering} {β : Type v} {m₁ m₂ : Std.TreeMap α β cmp} [inst : BEq β] [Std.TransCmp cmp]
  {m₃ m₄ : Std.TreeMap α β cmp}, m₁.Equiv m₃ → m₂.Equiv m₄ → (m₁ == m₂) = (m₃ == m₄)
-- Mathlib.Order.Interval.Finset.Fin
Fin.map_natAddEmb_Ioo : ∀ {n : ℕ} (m : ℕ) (i j : Fin n),
  Finset.map (Fin.natAddEmb m) (Finset.Ioo i j) = Finset.Ioo (Fin.natAdd m i) (Fin.natAdd m j)
-- Mathlib.Data.Opposite
Opposite.op_injective : ∀ {α : Sort u}, Function.Injective Opposite.op
-- Mathlib.FieldTheory.Galois.NormalBasis
_private.Mathlib.FieldTheory.Galois.NormalBasis.0.IsGalois.normalBasis.eq_1 : ∀ (K : Type u_1) (L : Type u_2) [inst : Field K] [inst_1 : Field L] [inst_2 : Algebra K L]
  [inst_3 : FiniteDimensional K L] [inst_4 : IsGalois K L],
  IsGalois.normalBasis K L = basisOfLinearIndependentOfCardEqFinrank ⋯ ⋯
-- Mathlib.Topology.VectorBundle.Basic
Bundle.Pretrivialization.linearMapAt.congr_simp : ∀ (R : Type u_1) {B : Type u_2} {F : Type u_3} {E : B → Type u_4} [inst : Semiring R] [inst_1 : TopologicalSpace F]
  [inst_2 : TopologicalSpace B] [inst_3 : AddCommMonoid F] [inst_4 : Module R F]
  [inst_5 : (x : B) → AddCommMonoid (E x)] [inst_6 : (x : B) → Module R (E x)]
  (e e_1 : Bundle.Pretrivialization F Bundle.TotalSpace.proj) (e_e : e = e_1)
  [inst_7 : Bundle.Pretrivialization.IsLinear R e] (b : B),
  Bundle.Pretrivialization.linearMapAt R e b = Bundle.Pretrivialization.linearMapAt R e_1 b
-- Mathlib.Probability.Distributions.Poisson.Basic
ProbabilityTheory.poissonMeasure_conv_poissonMeasure : ∀ (r₁ r₂ : NNReal),
  (ProbabilityTheory.poissonMeasure r₁).conv (ProbabilityTheory.poissonMeasure r₂) =
    ProbabilityTheory.poissonMeasure (r₁ + r₂)
-- Mathlib.RingTheory.Lasker
/-- A `Finset` of submodules is a minimal primary decomposition of `N` if the submodules `Nᵢ`
intersect to `N`, are primary, the `√Ann(M/Nᵢ)` are distinct, and each `Nᵢ` is necessary.  -/
Submodule.IsMinimalPrimaryDecomposition : {R : Type u_1} →
  {M : Type u_2} →
    [inst : CommSemiring R] →
      [inst_1 : AddCommMonoid M] → [inst_2 : Module R M] → Submodule R M → Finset (Submodule R M) → Prop
-- Std.Data.Internal.List.Associative
Std.Internal.List.getValueCast!_insertEntry : ∀ {α : Type u} {β : α → Type v} [inst : BEq α] [inst_1 : LawfulBEq α] {l : List ((a : α) × β a)} {k a : α}
  [inst_2 : Inhabited (β a)] {v : β k},
  Std.Internal.List.getValueCast! a (Std.Internal.List.insertEntry k v l) =
    if h : (k == a) = true then cast ⋯ v else Std.Internal.List.getValueCast! a l
-- Std.Data.DTreeMap.Raw.Lemmas
Std.DTreeMap.Raw.maxKey?_alter_eq_self : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t : Std.DTreeMap.Raw α β cmp} [Std.TransCmp cmp]
  [inst : Std.LawfulEqCmp cmp],
  t.WF →
    ∀ {k : α} {f : Option (β k) → Option (β k)},
      (t.alter k f).maxKey? = some k ↔ (f (t.get? k)).isSome = true ∧ ∀ k' ∈ t, (cmp k' k).isLE = true
-- Mathlib.NumberTheory.ClassNumber.AdmissibleAbsoluteValue
AbsoluteValue.IsAdmissible.mk.sizeOf_spec : ∀ {R : Type u_1} [inst : EuclideanDomain R] {abv : AbsoluteValue R ℤ} [inst_1 : SizeOf R]
  (toIsEuclidean : abv.IsEuclidean) (card : ℝ → ℕ)
  (exists_partition' :
    ∀ (n : ℕ) {ε : ℝ},
      0 < ε →
        ∀ {b : R},
          b ≠ 0 → ∀ (A : Fin n → R), ∃ t, ∀ (i₀ i₁ : Fin n), t i₀ = t i₁ → ↑(abv (A i₁ % b - A i₀ % b)) < abv b • ε),
  sizeOf { toIsEuclidean := toIsEuclidean, card := card, exists_partition' := exists_partition' } =
    1 + sizeOf toIsEuclidean
-- Mathlib.RingTheory.HahnSeries.Valuation
/-- The additive valuation on `R⟦Γ⟧` returning the smallest index at which
a Hahn Series has a nonzero coefficient, or `⊤` for the 0 series.  -/
HahnSeries.addVal : (Γ : Type u_1) →
  (R : Type u_2) →
    [inst : AddCancelCommMonoid Γ] →
      [inst_1 : LinearOrder Γ] →
        [inst_2 : IsOrderedCancelAddMonoid Γ] →
          [inst_3 : Ring R] → [IsDomain R] → AddValuation (HahnSeries Γ R) (WithTop Γ)
-- Mathlib.RingTheory.Valuation.Basic
AddValuation.IsEquiv.val_eq : ∀ {R : Type u_3} {Γ₀ : Type u_4} {Γ'₀ : Type u_5} [inst : LinearOrderedAddCommMonoidWithTop Γ₀]
  [inst_1 : LinearOrderedAddCommMonoidWithTop Γ'₀] [inst_2 : Ring R] {v₁ : AddValuation R Γ₀} {v₂ : AddValuation R Γ'₀},
  v₁.IsEquiv v₂ → ∀ {r s : R}, v₁ r = v₁ s ↔ v₂ r = v₂ s
-- Std.Data.DTreeMap.Internal.Lemmas
Std.DTreeMap.Internal.Impl.Const.mem_toArray_iff_get?_eq_some : ∀ {α : Type u} {instOrd : Ord α} {β : Type v} {t : Std.DTreeMap.Internal.Impl α fun x => β} [Std.TransOrd α]
  [Std.LawfulEqOrd α] {k : α} {v : β},
  t.WF → ((k, v) ∈ Std.DTreeMap.Internal.Impl.Const.toArray t ↔ Std.DTreeMap.Internal.Impl.Const.get? t k = some v)
-- Mathlib.Algebra.Order.CauSeq.Completion
/-- The Cauchy completion forms a division ring.  -/
CauSeq.Completion.Cauchy.divisionRing : {α : Type u_1} →
  [inst : Field α] →
    [inst_1 : LinearOrder α] →
      [inst_2 : IsStrictOrderedRing α] →
        {β : Type u_2} →
          [inst_3 : DivisionRing β] →
            {abv : β → α} → [inst_4 : IsAbsoluteValue abv] → DivisionRing (CauSeq.Completion.Cauchy abv)
-- Std.Data.TreeMap.Lemmas
Std.TreeMap.getKey?_unitOfList_of_mem : ∀ {α : Type u} {cmp : α → α → Ordering} [Std.TransCmp cmp] {l : List α} {k k' : α},
  cmp k k' = Ordering.eq →
    List.Pairwise (fun a b => ¬cmp a b = Ordering.eq) l → k ∈ l → (Std.TreeMap.unitOfList l cmp).getKey? k' = some k
-- Init.Data.Rat.Lemmas
/-- Define a (dependent) function or prove `∀ r : Rat, p r` by dealing with rational
numbers of the form `n /. d` with `d ≠ 0`.  -/
Rat.numDenCasesOn' : {C : ℚ → Sort u} → (a : ℚ) → ((n : ℤ) → (d : ℕ) → d ≠ 0 → C (Rat.divInt n ↑d)) → C a
-- Init.Data.Iterators.Consumers.Partial
/-- For an iterator `it`, `it.allowNontermination` provides potentially nonterminating variants of
consumers such as `toList`. They can be used without any proof of termination such as `Finite`
or `Productive`, but as they are implemented with the `partial` declaration modifier, they are
opaque for the kernel and it is impossible to prove anything about them.
 -/
Std.Iter.allowNontermination : {α β : Type w} → Std.Iter β → Std.Iter.Partial β
-- Mathlib.AlgebraicTopology.ModelCategory.BrownLemma
HomotopicalAlgebra.CofibrantBrownFactorization.mk : {C : Type u_1} →
  [inst : CategoryTheory.Category.{v_1, u_1} C] →
    [inst_1 : HomotopicalAlgebra.ModelCategory C] →
      {X Y : C} →
        {f : X ⟶ Y} →
          (toMapFactorizationData :
              (HomotopicalAlgebra.cofibrations C).MapFactorizationData (HomotopicalAlgebra.trivialFibrations C) f) →
            (s : Y ⟶ toMapFactorizationData.Z) →
              autoParam
                  (CategoryTheory.CategoryStruct.comp s toMapFactorizationData.p = CategoryTheory.CategoryStruct.id Y)
                  HomotopicalAlgebra.CofibrantBrownFactorization.s_p._autoParam →
                autoParam (HomotopicalAlgebra.Cofibration s)
                    HomotopicalAlgebra.CofibrantBrownFactorization.cofibration_s._autoParam →
                  HomotopicalAlgebra.CofibrantBrownFactorization f
-- Mathlib.Tactic.Ring.Common
Mathlib.Tactic.Ring.Common.add_pos_right : ∀ {a₂ : ℕ} (a₁ : ℕ), 0 < a₂ → 0 < a₁ + a₂
-- Mathlib.Data.Finset.Powerset
Finset.powersetCard_empty_subsingleton : ∀ {α : Type u_1} (n : ℕ), (↑(Finset.powersetCard n ∅)).Subsingleton
-- Mathlib.Computability.Partrec
Computable.to₂ : ∀ {α : Type u_1} {β : Type u_2} {σ : Type u_4} [inst : Primcodable α] [inst_1 : Primcodable β] [inst_2 : Primcodable σ]
  {f : α × β → σ}, Computable f → Computable₂ fun a b => f (a, b)
-- Init.Data.Iterators.Basic
Std.IterStep.mapIterator_comp : ∀ {α : Type u} {β : Type w} {α' : Type u'} {α'' : Type u''} {f : α → α'} {g : α' → α''},
  Std.IterStep.mapIterator (g ∘ f) = Std.IterStep.mapIterator g ∘ Std.IterStep.mapIterator f
-- Std.Data.DHashMap.RawLemmas
Std.DHashMap.Raw.toList_empty : ∀ {α : Type u} {β : α → Type v}, ∅.toList = []
-- Init.Data.Vector.Lemmas
Vector.forall_mem_iff_forall_getElem : ∀ {α : Type u_1} {n : ℕ} {P : α → Prop} {xs : Vector α n}, (∀ x ∈ xs, P x) ↔ ∀ (i : ℕ) (hi : i < n), P xs[i]
-- Mathlib.Topology.ClusterPt
mapClusterPt_id_iff : ∀ {α : Type u_1} {F : Filter α} [inst : TopologicalSpace α] {a : α}, MapClusterPt a F id ↔ ClusterPt a F
-- Mathlib.Analysis.Calculus.VectorField
VectorField.pullback_eq_of_not_isInvertible : ∀ {𝕜 : 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}
  {x : E}, ¬(fderiv 𝕜 f x).IsInvertible → ∀ (V : F → F), VectorField.pullback 𝕜 f V x = 0
-- Lean.Message
Lean.MessageLog.forM : {m : Type → Type} → [Monad m] → Lean.MessageLog → (Lean.Message → m Unit) → m Unit
-- Mathlib.Topology.Homotopy.Equiv
/-- Any topological space is homotopy equivalent to itself.
 -/
ContinuousMap.HomotopyEquiv.refl : (X : Type u) → [inst : TopologicalSpace X] → ContinuousMap.HomotopyEquiv X X
-- Mathlib.CategoryTheory.Subfunctor.OfSection
/-- The subpresheaf of `F : Cᵒᵖ ⥤ Type w` that is generated
by a section `x : F.obj X`.  -/
CategoryTheory.Subfunctor.ofSection : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    {F : CategoryTheory.Functor Cᵒᵖ (Type w)} → {X : Cᵒᵖ} → F.obj X → CategoryTheory.Subfunctor F
-- Mathlib.RingTheory.PowerSeries.Basic
PowerSeries.coeff_mul_C : ∀ {R : Type u_1} [inst : Semiring R] (n : ℕ) (φ : PowerSeries R) (a : R),
  (PowerSeries.coeff n) (φ * PowerSeries.C a) = (PowerSeries.coeff n) φ * a
-- Mathlib.Analysis.Complex.Circle
/-- The additive character from `ℝ` onto the circle, given by `fun x ↦ exp (x * I)`. This uses the
probabilist convention that there is no `2 * π` in the exponent.  -/
Real.probChar : AddChar ℝ Circle
-- Mathlib.Algebra.Order.Monoid.Unbundled.Units
Units.one_le_inv_mul : ∀ {M : Type u_1} [inst : Monoid M] [inst_1 : LE M] [MulLeftMono M] (u : Mˣ) {a : M}, 1 ≤ ↑u⁻¹ * a ↔ ↑u ≤ a
-- Mathlib.RingTheory.Artinian.Module
IsArtinianRing.quotNilradicalPowEquivPi_apply : ∀ (R : Type u_1) [inst : CommRing R] [inst_1 : IsArtinianRing R] (n : ℕ) (a : R ⧸ nilradical R ^ n)
  (I : MaximalSpectrum R),
  (IsArtinianRing.quotNilradicalPowEquivPi R n) a I =
    (Ideal.quotientInfRingEquivPiQuotient (fun I => I.asIdeal ^ n) ⋯) ((Ideal.quotientEquivAlgOfEq R ⋯) a) I
-- Mathlib.Analysis.Normed.Operator.Bilinear
ContinuousLinearMap.flip_flip : ∀ {𝕜 : Type u_1} {𝕜₂ : Type u_2} {𝕜₃ : Type u_3} {E : Type u_4} {F : Type u_6} {G : Type u_8}
  [inst : SeminormedAddCommGroup E] [inst_1 : SeminormedAddCommGroup F] [inst_2 : SeminormedAddCommGroup G]
  [inst_3 : NontriviallyNormedField 𝕜] [inst_4 : NontriviallyNormedField 𝕜₂] [inst_5 : NontriviallyNormedField 𝕜₃]
  [inst_6 : NormedSpace 𝕜 E] [inst_7 : NormedSpace 𝕜₂ F] [inst_8 : NormedSpace 𝕜₃ G] {σ₂₃ : 𝕜₂ →+* 𝕜₃} {σ₁₃ : 𝕜 →+* 𝕜₃}
  [inst_9 : RingHomIsometric σ₂₃] [inst_10 : RingHomIsometric σ₁₃] (f : E →SL[σ₁₃] F →SL[σ₂₃] G), f.flip.flip = f
-- Lean.Compiler.IR.CompilerM
_private.Lean.Compiler.IR.CompilerM.0.Lean.IR.logDeclsAux : Lean.Name → Lean.Name → Array Lean.IR.Decl → Lean.IR.CompilerM Unit
-- Init.Data.Hashable
instHashableList : {α : Type u_1} → [Hashable α] → Hashable (List α)
-- Mathlib.GroupTheory.Perm.Cycle.Type
Equiv.Perm.IsThreeCycle.eq_swap_mul_swap_iff_mem_support : ∀ {α : Type u_1} [inst : Fintype α] [inst_1 : DecidableEq α] {g : Equiv.Perm α} {a : α},
  g.IsThreeCycle → (g = Equiv.swap a (g a) * Equiv.swap (g a) (g (g a)) ↔ a ∈ g.support)
-- Mathlib.Algebra.Order.Monoid.Unbundled.Defs
/-- Do not use this. Use `le_of_mul_le_mul_left'` instead.  -/
MulLeftReflectLE.le_of_mul_le_mul_left' : ∀ {M : Type u_1} {inst : Mul M} {inst_1 : LE M} [self : MulLeftReflectLE M] {a b₁ b₂ : M}, a * b₁ ≤ a * b₂ → b₁ ≤ b₂
-- Mathlib.CategoryTheory.GradedObject
CategoryTheory.GradedObject.comapEquiv_unitIso : ∀ (C : Type u) [inst : CategoryTheory.Category.{v, u} C] {β γ : Type w} (e : β ≃ γ),
  (CategoryTheory.GradedObject.comapEquiv C e).unitIso =
    CategoryTheory.GradedObject.comapEq C ⋯ ≪≫ (CategoryTheory.Pi.comapComp (fun x => C) ⇑e ⇑e.symm).symm
-- Mathlib.RingTheory.MvPowerSeries.Rename
MvPowerSeries.killCompl_monomial_eq_zero : ∀ {σ : Type u_1} {τ : Type u_2} {R : Type u_4} [inst : CommSemiring R] {e : σ ↪ τ} {x : τ →₀ ℕ} (r : R),
  x ∉ Set.range (Finsupp.embDomain e) → (MvPowerSeries.killCompl e) ((MvPowerSeries.monomial x) r) = 0
-- Mathlib.Data.Sym.NatCard
Sym2.ncard_diagSet : ∀ (α : Type u_1), Sym2.diagSet.ncard = Nat.card α
-- Std.Data.DHashMap.Lemmas
Std.DHashMap.size_filter_eq_size_iff : ∀ {α : Type u} {β : α → Type v} {x : BEq α} {x_1 : Hashable α} {m : Std.DHashMap α β} [inst : LawfulBEq α]
  {f : (a : α) → β a → Bool}, (Std.DHashMap.filter f m).size = m.size ↔ ∀ (k : α) (h : k ∈ m), f k (m.get k h) = true
-- Std.Net.Addr
Std.Net.SocketAddressV6.mk.inj : ∀ {addr : Std.Net.IPv6Addr} {port : UInt16} {addr_1 : Std.Net.IPv6Addr} {port_1 : UInt16},
  { addr := addr, port := port } = { addr := addr_1, port := port_1 } → addr = addr_1 ∧ port = port_1
-- Mathlib.Algebra.Order.Interval.Set.Instances
Set.Ioc.instSemigroup : {R : Type u_1} → [inst : Semiring R] → [inst_1 : PartialOrder R] → [IsStrictOrderedRing R] → Semigroup ↑(Set.Ioc 0 1)
-- Init.Data.UInt.Lemmas
UInt16.toUInt32_toUInt64 : ∀ (n : UInt16), n.toUInt64.toUInt32 = n.toUInt32
-- Mathlib.Analysis.InnerProductSpace.LinearMap
/-- A linear equivalence that preserves the inner product is a linear isometric equivalence.  -/
LinearEquiv.isometryOfInner : {𝕜 : Type u_1} →
  {E : Type u_2} →
    [inst : RCLike 𝕜] →
      [inst_1 : SeminormedAddCommGroup E] →
        [inst_2 : InnerProductSpace 𝕜 E] →
          {E' : Type u_7} →
            [inst_3 : SeminormedAddCommGroup E'] →
              [inst_4 : InnerProductSpace 𝕜 E'] →
                (f : E ≃ₗ[𝕜] E') → (∀ (x y : E), inner 𝕜 (f x) (f y) = inner 𝕜 x y) → E ≃ₗᵢ[𝕜] E'
-- Mathlib.CategoryTheory.Limits.Shapes.Pullback.IsPullback.Basic
CategoryTheory.Functor.map_isPushout : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  (F : CategoryTheory.Functor C D) {W X Y Z : C} {f : W ⟶ X} {g : W ⟶ Y} {h : X ⟶ Z} {i : Y ⟶ Z}
  [CategoryTheory.Limits.PreservesColimit (CategoryTheory.Limits.span f g) F],
  CategoryTheory.IsPushout f g h i → CategoryTheory.IsPushout (F.map f) (F.map g) (F.map h) (F.map i)
-- Mathlib.SetTheory.ZFC.Basic
ZFSet.instWellFoundedRelation : WellFoundedRelation ZFSet.{u_1}
-- Mathlib.GroupTheory.Perm.Cycle.Basic
Equiv.Perm.sameCycle_subtypePerm : ∀ {α : Type u_2} {f : Equiv.Perm α} {p : α → Prop} {h : ∀ (x : α), p (f x) ↔ p x} {x y : { x // p x }},
  (f.subtypePerm h).SameCycle x y ↔ f.SameCycle ↑x ↑y
-- Mathlib.Algebra.Lie.OfAssociative
LieAlgebra.ad_eq_lmul_left_sub_lmul_right : ∀ {R : Type u} [inst : CommRing R] (A : Type v) [inst_1 : Ring A] [inst_2 : Algebra R A],
  ⇑(LieAlgebra.ad R A) = LinearMap.mulLeft R - LinearMap.mulRight R
-- Mathlib.Tactic.ComputeAsymptotics.Multiseries.Basic
_private.Mathlib.Tactic.ComputeAsymptotics.Multiseries.Basic.0.Tactic.ComputeAsymptotics.MultiseriesExpansion.Multiseries.monomialRpow.match_1.eq_2 : ∀ (motive : ℕ → Sort u_1) (m : ℕ) (h_1 : Unit → motive 0) (h_2 : (m : ℕ) → motive m.succ),
  (match m.succ with
    | 0 => h_1 ()
    | m.succ => h_2 m) =
    h_2 m
-- Mathlib.CategoryTheory.Sites.Continuous
CategoryTheory.PreOneHypercover.map_p₁ : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  {X : C} (E : CategoryTheory.PreOneHypercover X) (F : CategoryTheory.Functor C D)
  (x x_1 : (CategoryTheory.PreZeroHypercover.map F E.toPreZeroHypercover).I₀) (j : E.I₁ x x_1),
  (E.map F).p₁ j = F.map (E.p₁ j)
-- Mathlib.Topology.Compactness.Lindelof
/-- A set `s` is Lindelöf if for every family of closed sets whose intersection avoids `s`,
there exists a countable subfamily whose intersection avoids `s`.  -/
isLindelof_of_countable_subfamily_closed : ∀ {X : Type u} [inst : TopologicalSpace X] {s : Set X},
  (∀ {ι : Type u} (t : ι → Set X),
      (∀ (i : ι), IsClosed (t i)) → s ∩ ⋂ i, t i = ∅ → ∃ u, u.Countable ∧ s ∩ ⋂ i ∈ u, t i = ∅) →
    IsLindelof s
-- Mathlib.AlgebraicTopology.SimplicialSet.HomotopyCat
SSet.OneTruncation₂.ofNerve₂.natIso_inv_app_map : ∀ (X : CategoryTheory.Cat) {X_1 Y : ↑(CategoryTheory.Quiv.of ↑X)} (f : X_1 ⟶ Y),
  (SSet.OneTruncation₂.ofNerve₂.natIso.inv.app X).map f = SSet.OneTruncation₂.nerveHomEquiv.symm f
-- Std.Data.DHashMap.Internal.AssocList.Iterator
/-- Internal implementation detail of the hash map  -/
Std.DHashMap.Internal.AssocList.AssocListIterator : (α : Type u) → (α → Type v) → Type (max u v)
-- Mathlib.Probability.Kernel.Composition.MeasureCompProd
MeasureTheory.Measure.compProd_congr : ∀ {α : Type u_1} {β : Type u_2} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} {μ : MeasureTheory.Measure α}
  {κ η : ProbabilityTheory.Kernel α β} [ProbabilityTheory.IsSFiniteKernel κ] [ProbabilityTheory.IsSFiniteKernel η],
  ⇑κ =ᵐ[μ] ⇑η → μ.compProd κ = μ.compProd η
-- Mathlib.Data.Set.Function
Set.BijOn.insert_iff : ∀ {α : Type u_1} {β : Type u_2} {s : Set α} {t : Set β} {f : α → β} {a : α},
  a ∉ s → f a ∉ t → (Set.BijOn f (insert a s) (insert (f a) t) ↔ Set.BijOn f s t)
-- Std.Data.TreeMap.Basic
/-- Tries to retrieve the smallest key that is greater than the given key,
returning `fallback` if no such key exists.
 -/
Std.TreeMap.getKeyGTD : {α : Type u} → {β : Type v} → {cmp : α → α → Ordering} → Std.TreeMap α β cmp → α → α → α
-- Mathlib.Analysis.SpecialFunctions.Trigonometric.Deriv
Complex.deriv_cos : ∀ {x : ℂ}, deriv Complex.cos x = -Complex.sin x
-- Mathlib.Combinatorics.Matroid.Circuit
Matroid.fundCircuit_restrict : ∀ {α : Type u_1} {M : Matroid α} {I : Set α} {e : α} {R : Set α},
  I ⊆ R → e ∈ R → R ⊆ M.E → (M.restrict R).fundCircuit e I = M.fundCircuit e I
-- Mathlib.RingTheory.PowerSeries.Basic
/-- First coefficient of the product of two power series.  -/
PowerSeries.coeff_one_mul : ∀ {R : Type u_2} [inst : CommSemiring R] (φ ψ : PowerSeries R),
  (PowerSeries.coeff 1) (φ * ψ) =
    (PowerSeries.coeff 1) φ * PowerSeries.constantCoeff ψ + (PowerSeries.coeff 1) ψ * PowerSeries.constantCoeff φ
-- Mathlib.CategoryTheory.Limits.Constructions.LimitsOfProductsAndEqualizers
/-- If a functor creates terminal objects and pullbacks, it creates finite limits.

We additionally require the rather strong condition that the functor reflects isomorphisms. It is
unclear whether the statement remains true without this condition. There are various definitions of
"creating limits" in the literature, and whether or not the condition can be dropped seems to depend
on the specific definition that is used.  -/
CategoryTheory.Limits.createsFiniteLimitsOfCreatesTerminalAndPullbacks : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    {D : Type u₂} →
      [inst_1 : CategoryTheory.Category.{v₂, u₂} D] →
        [CategoryTheory.Limits.HasTerminal D] →
          [CategoryTheory.Limits.HasPullbacks D] →
            (G : CategoryTheory.Functor C D) →
              [G.ReflectsIsomorphisms] →
                [CategoryTheory.CreatesLimitsOfShape (CategoryTheory.Discrete PEmpty.{1}) G] →
                  [CategoryTheory.CreatesLimitsOfShape CategoryTheory.Limits.WalkingCospan G] →
                    CategoryTheory.Limits.CreatesFiniteLimits G
-- Init.Grind.Module.Envelope
_private.Init.Grind.Module.Envelope.0.Lean.Grind.IntModule.OfNatModule.r.eq_1 : ∀ (α : Type u) [inst : Lean.Grind.NatModule α] (a b c d : α),
  Lean.Grind.IntModule.OfNatModule.r α (a, b) (c, d) = ∃ k, a + d + k = b + c + k
-- Std.Time.Time.Unit.Hour
Std.Time.Hour.instLEOrdinal : LE Std.Time.Hour.Ordinal
-- Mathlib.Topology.VectorBundle.Riemannian
/-- The inner product along the fibers of the bundle.  -/
Bundle.RiemannianMetric.inner : {B : Type u_4} →
  {E : B → Type u_6} →
    [inst : (b : B) → TopologicalSpace (E b)] →
      [inst_1 : (b : B) → AddCommGroup (E b)] →
        [inst_2 : (b : B) → Module ℝ (E b)] → Bundle.RiemannianMetric E → (b : B) → E b →L[ℝ] E b →L[ℝ] ℝ