mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Topology.Algebra.Module.FiniteDimension
LinearEquiv.toLinearEquiv_toContinuousLinearEquiv : ∀ {𝕜 : Type u} [hnorm : NontriviallyNormedField 𝕜] {E : Type v} [inst : AddCommGroup E] [inst_1 : Module 𝕜 E]
  [inst_2 : TopologicalSpace E] [inst_3 : IsTopologicalAddGroup E] [inst_4 : ContinuousSMul 𝕜 E] {F : Type w}
  [inst_5 : AddCommGroup F] [inst_6 : Module 𝕜 F] [inst_7 : TopologicalSpace F] [inst_8 : IsTopologicalAddGroup F]
  [inst_9 : ContinuousSMul 𝕜 F] [inst_10 : CompleteSpace 𝕜] [inst_11 : T2Space E] [inst_12 : T2Space F]
  [inst_13 : FiniteDimensional 𝕜 E] (e : E ≃ₗ[𝕜] F), ↑e.toContinuousLinearEquiv = e
-- Mathlib.CategoryTheory.ComposableArrows.Basic
CategoryTheory.ComposableArrows.isoMk₁_hom_app : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] {F G : CategoryTheory.ComposableArrows C 1}
  (left :
    F.obj' 0 CategoryTheory.ComposableArrows.homMk₁._proof_4 ≅ G.obj' 0 CategoryTheory.ComposableArrows.homMk₁._proof_4)
  (right :
    F.obj' 1 CategoryTheory.ComposableArrows.homMk₁._proof_5 ≅ G.obj' 1 CategoryTheory.ComposableArrows.homMk₁._proof_5)
  (w :
    autoParam
      (CategoryTheory.CategoryStruct.comp
          (F.map' 0 1 CategoryTheory.ComposableArrows.homMk₁._proof_4 CategoryTheory.ComposableArrows.homMk₁._proof_5)
          right.hom =
        CategoryTheory.CategoryStruct.comp left.hom
          (G.map' 0 1 CategoryTheory.ComposableArrows.homMk₁._proof_4 CategoryTheory.ComposableArrows.homMk₁._proof_5))
      CategoryTheory.ComposableArrows.isoMk₁._auto_1)
  (i : Fin (1 + 1)),
  (CategoryTheory.ComposableArrows.isoMk₁ left right w).hom.app i =
    match i with
    | ⟨0, isLt⟩ => left.hom
    | ⟨1, isLt⟩ => right.hom
-- Mathlib.Geometry.Euclidean.Angle.Oriented.Affine
/-- Rotating the points in an oriented angle does not change the sign of that angle.  -/
EuclideanGeometry.oangle_rotate_sign : ∀ {V : Type u_1} {P : Type u_2} [inst : NormedAddCommGroup V] [inst_1 : InnerProductSpace ℝ V] [inst_2 : MetricSpace P]
  [inst_3 : NormedAddTorsor V P] [hd2 : Fact (Module.finrank ℝ V = 2)] [inst_4 : Module.Oriented ℝ V (Fin 2)]
  (p₁ p₂ p₃ : P), (EuclideanGeometry.oangle p₂ p₃ p₁).sign = (EuclideanGeometry.oangle p₁ p₂ p₃).sign
-- Mathlib.RingTheory.MvPolynomial.MonomialOrder
MonomialOrder.degree_ne_zero_of_sub_leadingTerm_ne_zero : ∀ {σ : Type u_1} {m : MonomialOrder σ} {R : Type u_2} [inst : CommRing R] {f : MvPolynomial σ R},
  f - m.leadingTerm f ≠ 0 → m.degree f ≠ 0
-- Mathlib.Data.Set.Prod
Set.graphOn_nonempty : ∀ {α : Type u_1} {β : Type u_2} {s : Set α} {f : α → β}, (Set.graphOn f s).Nonempty ↔ s.Nonempty
-- Std.Data.HashMap.Lemmas
Std.HashMap.getElem!_diff_of_not_mem_right : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} {β : Type v} {m₁ m₂ : Std.HashMap α β} [EquivBEq α] [LawfulHashable α]
  {k : α} [inst : Inhabited β], k ∉ m₂ → (m₁ \ m₂)[k]! = m₁[k]!
-- Mathlib.Algebra.Order.IsBotOne
min_eq_one : ∀ {α : Type u_1} [inst : LinearOrder α] [inst_1 : One α] [IsBotOneClass α] {a b : α}, min a b = 1 ↔ a = 1 ∨ b = 1
-- Mathlib.Algebra.Homology.Embedding.TruncGE
HomologicalComplex.instEpiFπTruncGE : ∀ {ι : Type u_1} {ι' : Type u_2} {c : ComplexShape ι} {c' : ComplexShape ι'} {C : Type u_3}
  [inst : CategoryTheory.Category.{v_1, u_3} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  (K : HomologicalComplex C c') (e : c.Embedding c') [inst_2 : e.IsTruncGE] [inst_3 : ∀ (i' : ι'), K.HasHomology i']
  [inst_4 : CategoryTheory.Limits.HasZeroObject C] (i' : ι'), CategoryTheory.Epi ((K.πTruncGE e).f i')
-- Mathlib.RingTheory.GradedAlgebra.RingHom
/-- Copy of a `GradedRingHom` with a new `toFun` equal to the old one. Useful to fix definitional
equalities.  -/
GradedRingHom.copy : {ι : Type u_1} →
  {A : Type u_2} →
    {B : Type u_3} →
      {σ : Type u_6} →
        {τ : Type u_7} →
          [inst : Semiring A] →
            [inst_1 : Semiring B] →
              [inst_2 : SetLike σ A] →
                [inst_3 : SetLike τ B] → {𝒜 : ι → σ} → {ℬ : ι → τ} → (f : 𝒜 →+*ᵍ ℬ) → (f' : A → B) → f' = ⇑f → 𝒜 →+*ᵍ ℬ
-- Mathlib.Algebra.TrivSqZeroExt.Basic
TrivSqZeroExt.isCentralScalar : ∀ {S : Type u_2} {R : Type u} {M : Type v} [inst : SMul S R] [inst_1 : SMul S M] [inst_2 : SMul Sᵐᵒᵖ R]
  [inst_3 : SMul Sᵐᵒᵖ M] [IsCentralScalar S R] [IsCentralScalar S M], IsCentralScalar S (TrivSqZeroExt R M)
-- Mathlib.RingTheory.DedekindDomain.Ideal.Lemmas
IsDedekindDomain.HeightOneSpectrum.ext_iff : ∀ {R : Type u_1} {inst : CommRing R} {x y : IsDedekindDomain.HeightOneSpectrum R}, x = y ↔ x.asIdeal = y.asIdeal
-- Init.System.IO
IO.FS.SystemTime.mk.sizeOf_spec : ∀ (sec : ℤ) (nsec : UInt32), sizeOf { sec := sec, nsec := nsec } = 1 + sizeOf sec + sizeOf nsec
-- Mathlib.NumberTheory.ArithmeticFunction.Defs
ArithmeticFunction.instCommSemiring : {R : Type u_1} → [inst : CommSemiring R] → CommSemiring (ArithmeticFunction R)
-- Mathlib.CategoryTheory.Limits.Shapes.Biproducts
CategoryTheory.Limits.biproduct.ι_fromSubtype_assoc : ∀ {J : Type w} {C : Type u} [inst : CategoryTheory.Category.{v, u} C]
  [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C] (f : J → C) [inst_2 : CategoryTheory.Limits.HasBiproduct f]
  (p : J → Prop) [inst_3 : CategoryTheory.Limits.HasBiproduct (Subtype.restrict p f)] (j : Subtype p) {Z : C}
  (h : ⨁ f ⟶ Z),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.biproduct.ι (Subtype.restrict p f) j)
      (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.biproduct.fromSubtype f p) h) =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.biproduct.ι f ↑j) h
-- Mathlib.GroupTheory.CoprodI
Monoid.CoprodI.Word.smul_eq_of_smul : ∀ {ι : Type u_1} {M : ι → Type u_2} [inst : (i : ι) → Monoid (M i)] [inst_1 : DecidableEq ι]
  [inst_2 : (i : ι) → DecidableEq (M i)] {i : ι} (m : M i) (w : Monoid.CoprodI.Word M), m • w = Monoid.CoprodI.of m • w
-- Mathlib.CategoryTheory.Functor.KanExtension.Preserves
CategoryTheory.Functor.leftKanExtensionCompIsoOfPreserves_hom_fac_app_assoc : ∀ {A : Type u_1} {B : Type u_2} {C : Type u_3} {D : Type u_4} [inst : CategoryTheory.Category.{v_1, u_1} A]
  [inst_1 : CategoryTheory.Category.{v_2, u_2} B] [inst_2 : CategoryTheory.Category.{v_3, u_3} C]
  [inst_3 : CategoryTheory.Category.{v_4, u_4} D] (G : CategoryTheory.Functor B D) (F : CategoryTheory.Functor A B)
  (L : CategoryTheory.Functor A C) [inst_4 : G.PreservesLeftKanExtension F L] [inst_5 : L.HasLeftKanExtension F] (a : A)
  {Z : D} (h : (L.leftKanExtension (F.comp G)).obj (L.obj a) ⟶ Z),
  CategoryTheory.CategoryStruct.comp (G.map ((L.leftKanExtensionUnit F).app a))
      (CategoryTheory.CategoryStruct.comp ((G.leftKanExtensionCompIsoOfPreserves F L).hom.app (L.obj a)) h) =
    CategoryTheory.CategoryStruct.comp ((L.leftKanExtensionUnit (F.comp G)).app a) h
-- Batteries.Data.AssocList
Batteries.AssocList.toList_modify : ∀ {α : Type u_1} {β : Type u_2} {f : α → β → β} [inst : BEq α] (a : α) (l : Batteries.AssocList α β),
  (Batteries.AssocList.modify a f l).toList =
    List.replaceF
      (fun x =>
        match x with
        | (k, v) => bif k == a then some (a, f k v) else none)
      l.toList
-- Mathlib.CategoryTheory.Preadditive.Injective.Basic
/-- The axiom of choice says that every nonempty type is an injective object in `Type`.  -/
CategoryTheory.Injective.instOfNonempty : ∀ (X : Type u₁) [Nonempty X], CategoryTheory.Injective X
-- Init.Data.Nat.Lemmas
Nat.pow_eq : ∀ {m n : ℕ}, m.pow n = m ^ n
-- Mathlib.Algebra.Group.Submonoid.Operations
Submonoid.map_bot : ∀ {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] (f : F), Submonoid.map f ⊥ = ⊥
-- Mathlib.Analysis.SpecialFunctions.Trigonometric.ArctanDeriv
Real.deriv_tan : ∀ (x : ℝ), deriv Real.tan x = 1 / Real.cos x ^ 2
-- Mathlib.Combinatorics.SimpleGraph.Regularity.Uniform
SimpleGraph.nonuniformWitness_subset : ∀ {α : Type u_1} {𝕜 : Type u_2} [inst : Field 𝕜] [inst_1 : LinearOrder 𝕜] [inst_2 : IsStrictOrderedRing 𝕜]
  (G : SimpleGraph α) [inst_3 : DecidableRel G.Adj] {ε : 𝕜} {s t : Finset α},
  ¬G.IsUniform ε s t → G.nonuniformWitness ε s t ⊆ s
-- Mathlib.Order.Filter.AtTopBot.Map
OrderIso.map_atTop : ∀ {α : Type u_3} {β : Type u_4} [inst : Preorder α] [inst_1 : Preorder β] (e : α ≃o β),
  Filter.map (⇑e) Filter.atTop = Filter.atTop
-- Mathlib.Algebra.Order.Group.Unbundled.Basic
inv_mul_lt_one_iff_lt : ∀ {α : Type u} [inst : Group α] [inst_1 : LT α] [MulRightStrictMono α] {a b : α}, a * b⁻¹ < 1 ↔ a < b
-- Mathlib.RingTheory.Polynomial.Cyclotomic.Basic
Polynomial.squarefree_cyclotomic : ∀ (n : ℕ) (K : Type u_2) [inst : Field K] [NeZero ↑n], Squarefree (Polynomial.cyclotomic n K)
-- Mathlib.Topology.Sheaves.Skyscraper
/-- The cocone at `*` for the stalk functor of `skyscraperPresheaf p₀ A` when `y ∉ closure {p₀}`
 -/
skyscraperPresheafCocone : {X : TopCat} →
  (p₀ : ↑X) →
    [inst : (U : TopologicalSpace.Opens ↑X) → Decidable (p₀ ∈ U)] →
      {C : Type v} →
        [inst_1 : CategoryTheory.Category.{u, v} C] →
          (A : C) →
            [inst_2 : CategoryTheory.Limits.HasTerminal C] →
              (y : ↑X) →
                CategoryTheory.Limits.Cocone ((TopologicalSpace.OpenNhds.inclusion y).op.comp (skyscraperPresheaf p₀ A))
-- Mathlib.Order.Fin.Basic
Fin.addNat_inj : ∀ {n : ℕ} (m : ℕ) {i j : Fin n}, i.addNat m = j.addNat m ↔ i = j
-- Lean.Data.FuzzyMatching
Lean.FuzzyMatching.instInhabitedCharRole.default : Lean.FuzzyMatching.CharRole
-- Lean.Elab.Coinductive
/-- Declaration Id from the original `InductiveView`  -/
Lean.Elab.Command.CoinductiveElabData.declId : Lean.Elab.Command.CoinductiveElabData → Lean.Syntax
-- Init.Data.Array.Range
Array.le_snd_of_mem_zipIdx : ∀ {α : Type u_1} {x : α × ℕ} {k : ℕ} {xs : Array α}, x ∈ xs.zipIdx k → k ≤ x.2
-- Mathlib.ModelTheory.Syntax
/-- `exClosure φ` is the sentence asserting that there exist values for all free variables of `φ`
such that `φ` holds.  -/
FirstOrder.Language.Formula.exClosure : {L : FirstOrder.Language} → {α : Type u'} → [DecidableEq α] → L.Formula α → L.Sentence
-- Lean.Meta.Tactic.Grind.AC.Types
Lean.Meta.Grind.AC.EqCnstrProof.superpose_tail_idempotent.injEq : ∀ (x : Lean.Grind.AC.Var) (c₁ : Lean.Meta.Grind.AC.EqCnstr) (x_1 : Lean.Grind.AC.Var)
  (c₁_1 : Lean.Meta.Grind.AC.EqCnstr),
  (Lean.Meta.Grind.AC.EqCnstrProof.superpose_tail_idempotent x c₁ =
      Lean.Meta.Grind.AC.EqCnstrProof.superpose_tail_idempotent x_1 c₁_1) =
    (x = x_1 ∧ c₁ = c₁_1)
-- Std.Tactic.BVDecide.LRAT.Internal.Formula.Lemmas
Std.Tactic.BVDecide.LRAT.Internal.DefaultFormula.deleteOne_preserves_ratUnits : ∀ {n : ℕ} (f : Std.Tactic.BVDecide.LRAT.Internal.DefaultFormula n) (id : ℕ), (f.deleteOne id).ratUnits = f.ratUnits
-- Mathlib.Topology.CantorBendixson
CantorBendixson.iteratedDerivedSet_mem_fixedPoints : ∀ {X : Type u} [inst : TopologicalSpace X] (s : Set X),
  ∃ a, CantorBendixson.iteratedDerivedSet s a ∈ Function.fixedPoints ⇑relDerivedSet
-- Std.Data.TreeMap.Lemmas
Std.TreeMap.getElem?_insert : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Std.TreeMap α β cmp} [Std.TransCmp cmp] {a k : α} {v : β},
  (t.insert k v)[a]? = if cmp k a = Ordering.eq then some v else t[a]?
-- Mathlib.Analysis.Normed.Group.Ultra
/-- A commutative additive group with an ultrametric group seminorm is nonarchimedean
(as a topological group, i.e. every neighborhood of 0 contains an open subgroup).  -/
IsUltrametricDist.nonarchimedeanAddGroup : ∀ {M : Type u_1} [inst : SeminormedAddCommGroup M] [IsUltrametricDist M], NonarchimedeanAddGroup M
-- Mathlib.Algebra.Polynomial.Degree.Lemmas
Polynomial.natDegree_map_eq_of_isUnit_leadingCoeff : ∀ {R : Type u} {S : Type v} [inst : Semiring R] {p : Polynomial R} [inst_1 : Semiring S] [Nontrivial S] (f : R →+* S),
  IsUnit p.leadingCoeff → (Polynomial.map f p).natDegree = p.natDegree
-- Mathlib.GroupTheory.Commutator.Basic
AddSubgroup.addCommutator_top_right_le_iff : ∀ {G : Type u_1} [inst : AddGroup G] {H : AddSubgroup G}, ⁅H, ⊤⁆ ≤ H ↔ H.Normal
-- Mathlib.Order.Interval.Finset.Fin
Fin.map_succEmb_Iic : ∀ {n : ℕ} (i : Fin n), Finset.map (Fin.succEmb n) (Finset.Iic i) = Finset.Ioc 0 i.succ
-- Mathlib.Algebra.Lie.Basis.Prod
/-- A distinguished subalgebra of the Lie algebra defined by `LieAlgebra.Basis.prod`.

Subject to the assumtions demanded by `LieAlgebra.Basis.isCartanSubalgebra` this will be a Cartan
subalgebra of `LieAlgebra.Basis.prod`.  -/
_private.Mathlib.Algebra.Lie.Basis.Prod.0.LieAlgebra.Basis.prodCartan : {ι₁ : Type u_1} →
  {ι₂ : Type u_2} →
    {L₁ : Type u_3} →
      {L₂ : Type u_4} →
        [inst : Finite ι₁] →
          [inst_1 : Finite ι₂] →
            (eι : ι₁ ≃ ι₂) →
              [inst_2 : LieRing L₁] →
                [inst_3 : LieRing L₂] →
                  {R : Type u_5} →
                    [inst_4 : CommRing R] →
                      [inst_5 : LieAlgebra R L₁] →
                        {H₁ : LieSubalgebra R L₁} →
                          (b₁ : LieAlgebra.Basis ι₁ H₁) →
                            [inst_6 : LieAlgebra R L₂] →
                              {H₂ : LieSubalgebra R L₂} →
                                (b₂ : LieAlgebra.Basis ι₂ H₂) → LieSubalgebra R ↥(LieAlgebra.Basis.prod✝ eι b₁ b₂)
-- Init.Grind.Offset
Lean.Grind.Nat.lo_ro_1 : ∀ (u w v k₁ k₂ : ℕ), Lean.Grind.isLt k₂ k₁ = true → u + k₁ ≤ w → w ≤ v + k₂ → u + (k₁ - k₂) ≤ v
-- Mathlib.Topology.ContinuousMap.ZeroAtInfty
/-- `C₀(α, β)` is the type of continuous functions `α → β` which vanish at infinity from a
topological space to a metric space with a zero element.

When possible, instead of parametrizing results over `(f : C₀(α, β))`,
you should parametrize over `(F : Type*) [ZeroAtInftyContinuousMapClass F α β] (f : F)`.

When you extend this structure, make sure to extend `ZeroAtInftyContinuousMapClass`.  -/
ZeroAtInftyContinuousMap : (α : Type u) → (β : Type v) → [TopologicalSpace α] → [Zero β] → [TopologicalSpace β] → Type (max u v)
-- Lean.Log
/-- Log a named error message using the given message data. The position is provided by `ref`.

Note: Use the macro `logNamedErrorAt`, which validates error names, instead of calling this function
directly.
 -/
Lean.logNamedErrorAt : {m : Type → Type} →
  [Monad m] →
    [Lean.MonadLog m] →
      [Lean.AddMessageContext m] → [Lean.MonadOptions m] → Lean.Syntax → Lean.Name → Lean.MessageData → m Unit
-- Mathlib.Algebra.Group.NatPowAssoc
Nat.cast_npow : ∀ (R : Type u_2) [inst : NonAssocSemiring R] [inst_1 : Pow R ℕ] [NatPowAssoc R] (n m : ℕ), ↑(n ^ m) = ↑n ^ m
-- Std.Internal.Do.PredTrans
Std.Internal.Do.PredTrans.mk.injEq : ∀ {Pred : Type u} {EPred : Type v} {α : Type w} (apply apply_1 : (α → Pred) → EPred → Pred),
  ({ apply := apply } = { apply := apply_1 }) = (apply = apply_1)
-- Mathlib.AlgebraicTopology.SimplicialSet.RelativeMorphism
SSet.RelativeMorphism.precomp_homotopyClass : ∀ {X Y Z : SSet} {A : X.Subcomplex} {B : Y.Subcomplex} {φ : A.toSSet ⟶ B.toSSet} {C : Z.Subcomplex}
  {ψ : B.toSSet ⟶ C.toSSet} (f : SSet.RelativeMorphism A B φ) (f' : SSet.RelativeMorphism B C ψ)
  {φψ : A.toSSet ⟶ C.toSSet} (fac : CategoryTheory.CategoryStruct.comp φ ψ = φψ),
  f'.homotopyClass.precomp f fac = (f.comp f' fac).homotopyClass
-- Mathlib.NumberTheory.RamificationInertia.Inertia
/-- **Alias** of `Ideal.inertiaDeg'_le_inertiaDeg'`. -/
Ideal.inertiaDeg_le_inertiaDeg : ∀ {R : Type u} [inst : CommRing R] {S : Type v} [inst_1 : CommRing S] [inst_2 : Algebra R S] (p : Ideal R) (P : Ideal S)
  {T : Type u_2} [inst_3 : CommRing T] [inst_4 : Algebra R T] [inst_5 : Algebra S T] [IsScalarTower R S T]
  [Module.Finite R T] (Q : Ideal T) [P.LiesOver p] [Q.LiesOver P] [p.IsPrime], P.inertiaDeg' Q ≤ p.inertiaDeg' Q
-- Lean.Meta.Tactic.Simp.BuiltinSimprocs.Fin
/-- Simplification procedure for ensuring `Fin n` literals are normalized.  -/
Fin.isValue : Lean.Meta.Simp.DSimproc
-- Mathlib.Topology.Algebra.MulAction
/-- Suppose that `N` additively acts on `X` and `M` continuously additively acts on `Y`.
Suppose that `g : Y → X` is an additive action homomorphism in the following sense:
there exists a continuous function `f : N → M` such that `g (c +ᵥ x) = f c +ᵥ g x`.
Then the action of `N` on `X` is continuous as well.

In many cases, `f = id` so that `g` is an action homomorphism in the sense of `AddActionHom`.
However, this version also works for `f = AddUnits.val`.  -/
Topology.IsInducing.continuousVAdd : ∀ {M : Type u_1} {X : Type u_2} {Y : Type u_3} [inst : TopologicalSpace M] [inst_1 : TopologicalSpace X]
  [inst_2 : TopologicalSpace Y] [inst_3 : VAdd M X] [ContinuousVAdd M X] {g : Y → X} {N : Type u_5} [inst_5 : VAdd N Y]
  [inst_6 : TopologicalSpace N] {f : N → M},
  Topology.IsInducing g → Continuous f → (∀ {c : N} {x : Y}, g (c +ᵥ x) = f c +ᵥ g x) → ContinuousVAdd N Y
-- Mathlib.CategoryTheory.Bicategory.Functor.Cat.ObjectProperty
/-- If `P` is a property of objects for a pseudofunctor `F` to `Cat`,
this is the condition that `P` is preserved by the application of the functors `F.map`.  -/
CategoryTheory.Pseudofunctor.ObjectProperty.IsClosedUnderMapObj : {B : Type u} →
  [inst : CategoryTheory.Bicategory B] →
    {F : CategoryTheory.Pseudofunctor B CategoryTheory.Cat} → F.ObjectProperty → Prop
-- Std.Time.Format.Modifier
Std.Time.Number.mk.injEq : ∀ (padding padding_1 : ℕ), ({ padding := padding } = { padding := padding_1 }) = (padding = padding_1)
-- Std.Data.Iterators.Lemmas.Producers.Array
Array.iter_equiv_iter_toList : ∀ {α : Type w} {array : Array α}, array.iter.Equiv array.toList.iter
-- Mathlib.AlgebraicGeometry.Geometrically.Basic
AlgebraicGeometry.pullback_of_geometrically' : ∀ {P : CategoryTheory.ObjectProperty AlgebraicGeometry.Scheme} {X Y : AlgebraicGeometry.Scheme} {f : X ⟶ Y},
  AlgebraicGeometry.geometrically P f →
    ∀ (K : Type u) [inst : Field K] (y : AlgebraicGeometry.Spec (CommRingCat.of K) ⟶ Y),
      P (CategoryTheory.Limits.pullback y f)
-- Mathlib.Topology.Constructible
IsRetrocompact.univ : ∀ {X : Type u_2} [inst : TopologicalSpace X], IsRetrocompact Set.univ
-- Mathlib.MeasureTheory.Measure.Haar.Unique
MeasureTheory.Measure.measurePreserving_zsmul : ∀ {G : Type u_1} [inst : AddCommGroup G] [inst_1 : TopologicalSpace G] [IsTopologicalAddGroup G]
  [inst_3 : MeasurableSpace G] [BorelSpace G] (μ : MeasureTheory.Measure G) [μ.IsAddHaarMeasure] [CompactSpace G]
  [DivisibleBy G ℤ] {n : ℤ}, n ≠ 0 → MeasureTheory.MeasurePreserving (fun g => n • g) μ μ
-- Std.Data.DHashMap.Internal.Model
Std.DHashMap.Internal.Raw₀.getD_eq_getDₘ : ∀ {α : Type u} {β : α → Type v} [inst : BEq α] [inst_1 : LawfulBEq α] [inst_2 : Hashable α]
  (m : Std.DHashMap.Internal.Raw₀ α β) (a : α) (fallback : β a), m.getD a fallback = m.getDₘ a fallback
-- Mathlib.Tactic.ArithMult
/-- `arith_mult` solves goals of the form `IsMultiplicative f` for `f : ArithmeticFunction R`
by applying lemmas tagged with the user attribute `arith_mult`, and prints out the generated
proof term.  -/
ArithmeticFunction.arith_mult? : Lean.ParserDescr
-- Mathlib.Combinatorics.SimpleGraph.Subgraph
SimpleGraph.Subgraph.incidenceSet_subset : ∀ {V : Type u} {G : SimpleGraph V} (G' : G.Subgraph) (v : V), G'.incidenceSet v ⊆ G'.edgeSet
-- Mathlib.Condensed.AB
Condensed.instAB4StarCondensedMod : ∀ (R : Type (u + 1)) [inst : Ring R], CategoryTheory.AB4Star (CondensedMod R)
-- Mathlib.CategoryTheory.Monoidal.Mod
CategoryTheory.AddModObj.ext : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.MonoidalCategory C] {M : C}
  [inst_2 : CategoryTheory.AddMonObj M] {X : C} (h₁ h₂ : CategoryTheory.AddModObj M X),
  CategoryTheory.AddModObj.vadd = CategoryTheory.AddModObj.vadd → h₁ = h₂
-- Mathlib.Analysis.Polynomial.MahlerMeasure
Polynomial.prod_max_one_norm_roots_le_mahlerMeasure_of_one_le_leadingCoeff : ∀ {p : Polynomial ℂ}, 1 ≤ ‖p.leadingCoeff‖ → (Multiset.map (fun a => max 1 ‖a‖) p.roots).prod ≤ p.mahlerMeasure
-- Mathlib.Algebra.Homology.ShortComplex.RightHomology
CategoryTheory.ShortComplex.fromOpcycles_op_cyclesOpIso_inv : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  (S : CategoryTheory.ShortComplex C) [inst_2 : S.HasRightHomology],
  CategoryTheory.CategoryStruct.comp S.fromOpcycles.op S.cyclesOpIso.inv = S.op.toCycles
-- Init.Data.String.Lemmas.Pattern.Basic
String.Slice.Pattern.Model.IsLongestMatchAtChain.sliceTo : ∀ {ρ : Type} {pat : ρ} [inst : String.Slice.Pattern.Model.PatternModel pat] {s : String.Slice} {startPos endPos : s.Pos}
  (h : String.Slice.Pattern.Model.IsLongestMatchAtChain pat startPos endPos) (p : s.Pos) (hp : endPos ≤ p),
  String.Slice.Pattern.Model.IsLongestMatchAtChain pat (p.sliceTo startPos ⋯) (p.sliceTo endPos hp)
-- Mathlib.MeasureTheory.MeasurableSpace.MeasurablyGenerated
MeasurableSet.Subtype.instCompl : {α : Type u_1} → [inst : MeasurableSpace α] → Compl (Subtype MeasurableSet)
-- Mathlib.Analysis.Convex.Topology
/-- **Alias** of `Convex.nhdsWithin_sdiff_eq_nhdsLT`. -/
Convex.nhdsWithin_diff_eq_nhdsLT : ∀ {𝕜 : Type u_4} [inst : Field 𝕜] [inst_1 : LinearOrder 𝕜] [IsStrictOrderedRing 𝕜] [inst_3 : TopologicalSpace 𝕜]
  [OrderTopology 𝕜] {s : Set 𝕜},
  Convex 𝕜 s →
    ∀ {a : 𝕜},
      a ∈ closure s → (s ∩ Set.Iio a).Nonempty → s ∩ Set.Ioi a = ∅ → nhdsWithin a (s \ {a}) = nhdsWithin a (Set.Iio a)
-- Mathlib.MeasureTheory.Function.SimpleFunc
MeasureTheory.SimpleFunc.instAddMonoid : {α : Type u_1} → {β : Type u_2} → [inst : MeasurableSpace α] → [AddMonoid β] → AddMonoid (MeasureTheory.SimpleFunc α β)
-- Mathlib.RingTheory.Perfection
Perfection.lift.congr_simp : ∀ (p : ℕ) [hp : Fact (Nat.Prime p)] (R : Type u₁) [inst : CommSemiring R] [inst_1 : CharP R p]
  [inst_2 : PerfectRing R p] (S : Type u₂) [inst_3 : CommSemiring S] [inst_4 : CharP S p],
  Perfection.lift p R S = Perfection.lift p R S
-- Mathlib.Algebra.Homology.ShortComplex.FunctorEquivalence
CategoryTheory.ShortComplex.FunctorEquivalence.inverse_map_τ₁ : ∀ (J : Type u_1) (C : Type u_2) [inst : CategoryTheory.Category.{v_1, u_1} J]
  [inst_1 : CategoryTheory.Category.{v_2, u_2} C] [inst_2 : CategoryTheory.Limits.HasZeroMorphisms C]
  {X Y : CategoryTheory.Functor J (CategoryTheory.ShortComplex C)} (φ : X ⟶ Y),
  ((CategoryTheory.ShortComplex.FunctorEquivalence.inverse J C).map φ).τ₁ =
    CategoryTheory.Functor.whiskerRight φ CategoryTheory.ShortComplex.π₁
-- Mathlib.Algebra.MonoidAlgebra.Defs
MonoidAlgebra.ofCoeff_eq_zero : ∀ {R : Type u_1} {M : Type u_4} [inst : Semiring R] {x : M →₀ R}, MonoidAlgebra.ofCoeff x = 0 ↔ x = 0
-- Std.Data.ExtDHashMap.Lemmas
Std.ExtDHashMap.isEmpty_union : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} {β : α → Type v} {m₁ m₂ : Std.ExtDHashMap α β} [inst : EquivBEq α]
  [inst_1 : LawfulHashable α], (m₁ ∪ m₂).isEmpty = (m₁.isEmpty && m₂.isEmpty)
-- Mathlib.Order.GameAdd
Sym2.gameAdd_mk'_iff : ∀ {α : Type u_1} {rα : α → α → Prop} {a₁ a₂ b₁ b₂ : α},
  Sym2.GameAdd rα s(a₁, b₁) s(a₂, b₂) ↔ Prod.GameAdd rα rα (a₁, b₁) (a₂, b₂) ∨ Prod.GameAdd rα rα (b₁, a₁) (a₂, b₂)
-- Mathlib.Tactic.Simps.Basic
/-- Auxiliary function for `getRawProjections`.
Generates the default projection, and looks for a custom projection declared by the user,
and replaces the default projection with the custom one, if it can find it.  -/
Simps.findProjection : Lean.Name → Simps.ParsedProjectionData → List Lean.Level → Lean.CoreM Simps.ParsedProjectionData
-- Mathlib.Probability.Process.Adapted
/-- **Alias** of `MeasureTheory.IsStronglyProgressive.neg`. -/
MeasureTheory.ProgMeasurable.neg : ∀ {Ω : Type u_1} {ι : Type u_2} {m : MeasurableSpace Ω} [inst : Preorder ι] {f : MeasureTheory.Filtration ι m}
  {β : Type u_3} [inst_1 : TopologicalSpace β] {u : ι → Ω → β} [inst_2 : MeasurableSpace ι] [inst_3 : AddGroup β]
  [ContinuousNeg β], MeasureTheory.IsStronglyProgressive f u → MeasureTheory.IsStronglyProgressive f fun i ω => -u i ω
-- Std.Sat.CNF.Basic
Std.Sat.CNF.add : {α : Type u_1} → Std.Sat.CNF.Clause α → Std.Sat.CNF α → Std.Sat.CNF α
-- Mathlib.CategoryTheory.Equivalence
CategoryTheory.Equivalence.pow_neg_one : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] (e : C ≌ C), e ^ (-1) = e.symm