mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.CategoryTheory.Shift.ShiftedHom
CategoryTheory.ShiftedHom.map_naturality_1 : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] {D : Type u_2}
  [inst_1 : CategoryTheory.Category.{v_2, u_2} D] {M : Type u_4} [inst_2 : AddMonoid M]
  [inst_3 : CategoryTheory.HasShift C M] [inst_4 : CategoryTheory.HasShift D M] {X Y : C} {a : M}
  (f : CategoryTheory.ShiftedHom X Y a) {F G : CategoryTheory.Functor C D} (e : F ≅ G) [inst_5 : F.CommShift M]
  [inst_6 : G.CommShift M] [CategoryTheory.NatTrans.CommShift e.hom M],
  (CategoryTheory.ShiftedHom.mk₀ 0 ⋯ (e.inv.app X)).comp
      ((f.map F).comp (CategoryTheory.ShiftedHom.mk₀ 0 ⋯ (e.hom.app Y)) ⋯) ⋯ =
    f.map G
-- Mathlib.Algebra.Group.Opposite
MulOpposite.instSemigroup : {α : Type u_1} → [Semigroup α] → Semigroup αᵐᵒᵖ
-- Mathlib.RepresentationTheory.Rep.Basic
Rep.instSMulHom : {k : Type u} →
  {G : Type v} → [inst : CommSemiring k] → [inst_1 : Monoid G] → {M N : Rep.{u_1, u, v} k G} → SMul k (M ⟶ N)
-- Mathlib.Topology.Algebra.Group.Pointwise
/-- If `G` acts on `X` continuously, the set `s • t` is closed when `s : Set G` is *compact* and
`t : Set X` is *closed*.

See also `IsClosed.smul_right_of_isCompact` for a version with the assumptions on `s` and `t`
reversed, assuming that the action is *proper*.  -/
IsClosed.smul_left_of_isCompact : ∀ {α : Type u} {β : Type v} [inst : TopologicalSpace α] [inst_1 : TopologicalSpace β] [inst_2 : Group α]
  [inst_3 : MulAction α β] [ContinuousInv α] [ContinuousSMul α β] {s : Set α} {t : Set β},
  IsClosed t → IsCompact s → IsClosed (s • t)
-- Mathlib.Algebra.Homology.Embedding.Basic
ComplexShape.instIsRelIffNatIntEmbeddingDownNat : ComplexShape.embeddingDownNat.IsRelIff
-- Mathlib.Algebra.Group.Units.Defs
/-- Units of a monoid form a `DivInvMonoid`.  -/
Units.instDivInvMonoid : {α : Type u} → [inst : Monoid α] → DivInvMonoid αˣ
-- Mathlib.RingTheory.IsTensorProduct
_private.Mathlib.RingTheory.IsTensorProduct.0.IsTensorProduct.assocAux.congr_simp : ∀ {R : Type u_9} {S : Type u_10} [inst : CommSemiring R] [inst_1 : CommSemiring S] [inst_2 : Algebra R S]
  {M₁ : Type u_11} {M₂ : Type u_12} {M₃ : Type u_13} {M₁₂ : Type u_14} {M₂₃ : Type u_15} [inst_3 : AddCommMonoid M₁]
  [inst_4 : AddCommMonoid M₂] [inst_5 : AddCommMonoid M₃] [inst_6 : AddCommMonoid M₁₂] [inst_7 : AddCommMonoid M₂₃]
  [inst_8 : Module R M₁] [inst_9 : Module R M₂] [inst_10 : Module S M₂] [inst_11 : IsScalarTower R S M₂]
  [inst_12 : Module R M₃] [inst_13 : Module S M₃] [inst_14 : IsScalarTower R S M₃] [inst_15 : Module R M₁₂]
  [inst_16 : Module S M₁₂] [inst_17 : IsScalarTower R S M₁₂] [inst_18 : Module R M₂₃] [inst_19 : Module S M₂₃]
  [inst_20 : IsScalarTower R S M₂₃] (f f_1 : M₁ →ₗ[R] M₂ →ₗ[S] M₁₂) (e_f : f = f_1)
  (hf : IsTensorProduct (LinearMap.restrictScalars₁₂ R R f)) (g g_1 : M₂ →ₗ[S] M₃ →ₗ[S] M₂₃) (e_g : g = g_1)
  (hg : IsTensorProduct g), IsTensorProduct.assocAux✝ f hf g hg = IsTensorProduct.assocAux✝ f_1 ⋯ g_1 ⋯
-- Mathlib.Analysis.SpecialFunctions.Trigonometric.Complex
Complex.cos_eq_iff_quadratic : ∀ {z w : ℂ}, Complex.cos z = w ↔ Complex.exp (z * Complex.I) ^ 2 - 2 * w * Complex.exp (z * Complex.I) + 1 = 0
-- Mathlib.GroupTheory.CoprodI
Monoid.CoprodI.lift_word_prod_nontrivial_of_head_card : ∀ {ι : Type u_1} {G : Type u_4} [inst : Group G] {H : ι → Type u_5} [inst_1 : (i : ι) → Group (H i)]
  (f : (i : ι) → H i →* G) {α : Type u_6} [inst_2 : MulAction G α] (X : ι → Set α),
  (∀ (i : ι), (X i).Nonempty) →
    Pairwise (Function.onFun Disjoint X) →
      (Pairwise fun i j => ∀ (h : H i), h ≠ 1 → (f i) h • X j ⊆ X i) →
        ∀ [Nontrivial ι] {i j : ι} (w : Monoid.CoprodI.NeWord H i j),
          3 ≤ Cardinal.mk (H i) → i ≠ j → (Monoid.CoprodI.lift f) w.prod ≠ 1
-- Lean.ExtraModUses
Lean.instBEqIndirectModUse.beq : Lean.IndirectModUse → Lean.IndirectModUse → Bool
-- Mathlib.RingTheory.HahnSeries.Addition
HahnSeries.coeff_ofFinsuppLinearMap : ∀ {Γ : Type u_1} (R : Type u_3) {V : Type u_6} [inst : PartialOrder Γ] [inst_1 : Semiring R] [inst_2 : AddCommMonoid V]
  [inst_3 : Module R V] (f : Γ →₀ V) (a : Γ), ((HahnSeries.ofFinsuppLinearMap R) f).coeff a = f a
-- Mathlib.Tactic.Linter.FindDeprecations
/-- `parseLine line` assumes that the input string is of the form
```
info: File/Path.lean:12:0: [362, 398, 399]
```
and extracts `[362, 398, 399]`.
It makes the assumption that there is a unique `: [` substring and then retrieves the numbers.

Note that this is the output of `Mathlib.Linter.CommandRanges.commandRangesLinter`
that the script here is parsing.
 -/
Mathlib.Tactic.parseLine : String → Option (List String.Pos.Raw)
-- Mathlib.RingTheory.Localization.BaseChange
IsLocalization.Away.tensorProductEquivTMulRight_tmul : ∀ {R : Type u_7} {S : Type u_8} [inst : CommSemiring R] [inst_1 : CommSemiring S] [inst_2 : Algebra R S] (A : Type u_9)
  [inst_3 : CommSemiring A] [inst_4 : Algebra R A] (g : A) (B : Type u_10) [inst_5 : CommSemiring B]
  [inst_6 : Algebra R B] [inst_7 : Algebra A B] [inst_8 : IsScalarTower R A B] [inst_9 : IsLocalization.Away g B]
  (x : S) (a : A),
  (IsLocalization.Away.tensorProductEquivTMulRight R S g B) (x ⊗ₜ[R] (algebraMap A B) a) =
    (algebraMap (TensorProduct R S A) (Localization.Away (1 ⊗ₜ[R] g))) (x ⊗ₜ[R] a)
-- Lean.Meta.Tactic.Simp.Simproc
Lean.Meta.Simp.BuiltinSimprocs.mk : Std.HashMap Lean.Name (Array Lean.Meta.SimpTheoremKey) →
  Std.HashMap Lean.Name (Lean.Meta.Simp.Simproc ⊕ Lean.Meta.Simp.DSimproc) → Lean.Meta.Simp.BuiltinSimprocs
-- Mathlib.Algebra.Group.AddChar
AddChar.coe_eq_one : ∀ {A : Type u_1} {M : Type u_3} [inst : AddMonoid A] [inst_1 : Monoid M] {ψ : AddChar A M}, ⇑ψ = 1 ↔ ψ = 0
-- Mathlib.Data.Sym.Sym2
Set.sym2_image : ∀ {α : Type u_1} {β : Type u_2} {f : α → β} {s : Set α}, (f '' s).sym2 = Sym2.map f '' s.sym2
-- Lean.Elab.InfoTree.Main
Lean.Elab.FieldInfo.format : Lean.Elab.ContextInfo → Lean.Elab.FieldInfo → IO Std.Format
-- Mathlib.Data.List.Sublists
List.Sublist.sublists' : ∀ {α : Type u} {l₁ l₂ : List α}, l₁.Sublist l₂ → l₁.sublists'.Sublist l₂.sublists'
-- Mathlib.Analysis.Normed.Affine.AddTorsor
nndist_midpoint_midpoint_le' : ∀ {V : Type u_1} {P : Type u_2} [inst : SeminormedAddCommGroup V] [inst_1 : PseudoMetricSpace P]
  [inst_2 : NormedAddTorsor V P] {𝕜 : Type u_5} [inst_3 : NormedField 𝕜] [inst_4 : NormedSpace 𝕜 V]
  [inst_5 : Invertible 2] (p₁ p₂ p₃ p₄ : P),
  nndist (midpoint 𝕜 p₁ p₂) (midpoint 𝕜 p₃ p₄) ≤ (nndist p₁ p₃ + nndist p₂ p₄) / ‖2‖₊
-- Mathlib.Algebra.LieRinehartAlgebra.Defs
/-- A morphism of Lie-Rinehart algebras, from `(A₁, L₁)` to `(A₂, L₂)`, consists of a pair of maps
`(σ, F)` where `σ : A₁ → A₂` is a morphism of algebras and `F` is a morphism of Lie algebras, which
respect the module structures.

Here we define the type of such morphisms with fixed `σ` (which can be regarded as functions
`L₁ → L₂`). In the future it may be useful to define the type of such morphisms with fixed `F`
(which can be regarded as functions `A₁ → A₂`) and the type of all such morphisms (which can be
regarded as functions `A₁ × L₁ → A₂ × L₂`).  -/
LieRinehartAlgebra.Hom : {R : Type u_1} →
  {A₁ : Type u_2} →
    {A₂ : Type u_4} →
      [inst : CommRing R] →
        [inst_1 : CommRing A₁] →
          [inst_2 : CommRing A₂] →
            [inst_3 : Algebra R A₁] →
              [inst_4 : Algebra R A₂] →
                (A₁ →ₐ[R] A₂) →
                  (L₁ : Type u_8) →
                    (L₂ : Type u_9) →
                      [inst_5 : LieRing L₁] →
                        [Module A₁ L₁] →
                          [LieRingModule L₁ A₁] →
                            [LieAlgebra R L₁] →
                              [inst_9 : LieRing L₂] →
                                [Module A₂ L₂] → [LieRingModule L₂ A₂] → [LieAlgebra R L₂] → Type (max u_8 u_9)
-- Mathlib.CategoryTheory.Bicategory.Functor.Cat
CategoryTheory.Pseudofunctor.mapId'.congr_simp : ∀ {B : Type u₁} [inst : CategoryTheory.Bicategory B] {C : Type u₂} [inst_1 : CategoryTheory.Bicategory C]
  (F : CategoryTheory.Pseudofunctor B C) {b : B} (f : b ⟶ b) (hf : f = CategoryTheory.CategoryStruct.id b),
  F.mapId' f hf = F.mapId' f hf
-- Mathlib.RingTheory.Spectrum.Prime.ChevalleyComplexity
_private.Mathlib.RingTheory.Spectrum.Prime.ChevalleyComplexity.0.ChevalleyThm.PolynomialC.InductionObj.powBound_ne_zero : ∀ {R : Type u_2} [inst : CommRing R] {n : ℕ} {e : ChevalleyThm.PolynomialC.InductionObj✝ R n},
  ChevalleyThm.PolynomialC.InductionObj.powBound✝ e ≠ 0
-- Mathlib.Algebra.Polynomial.Basic
Polynomial.toFinsupp_add : ∀ {R : Type u} [inst : Semiring R] (a b : Polynomial R), (a + b).toFinsupp = a.toFinsupp + b.toFinsupp
-- Init.SimpLemmas
Lean.arrow_congr_right : ∀ {p : Sort u} {q₁ q₂ : Sort v}, q₁ = q₂ → Lean.Arrow p q₁ = Lean.Arrow p q₂
-- Init.Data.Rat.Lemmas
Rat.ofNat_eq_ofNat : ∀ {a b : ℕ}, OfNat.ofNat a = OfNat.ofNat b ↔ a = b
-- Lean.Meta.LazyDiscrTree
Lean.Meta.LazyDiscrTree.setTrie : {α : Type} → Lean.Meta.LazyDiscrTree.TrieIndex → Lean.Meta.LazyDiscrTree.Trie α → Lean.Meta.LazyDiscrTree.MatchM α Unit
-- Std.Data.TreeSet.Lemmas
Std.TreeSet.getD_minD : ∀ {α : Type u} {cmp : α → α → Ordering} {t : Std.TreeSet α cmp} [Std.TransCmp cmp],
  t.isEmpty = false → ∀ {fallback fallback' : α}, t.getD (t.minD fallback) fallback' = t.minD fallback
-- Mathlib.Analysis.Distribution.SchwartzSpace.Deriv
SchwartzMap.laplacian_apply : ∀ {E : Type u_5} {F : Type u_8} [inst : NormedAddCommGroup E] [inst_1 : NormedAddCommGroup F] [inst_2 : NormedSpace ℝ F]
  [inst_3 : InnerProductSpace ℝ E] [inst_4 : FiniteDimensional ℝ E] (f : SchwartzMap E F) (x : E),
  (Laplacian.laplacian f) x = Laplacian.laplacian (⇑f) x
-- Mathlib.RingTheory.Kaehler.JacobiZariski
Algebra.Generators.H1Cotangent.δAux_monomial : ∀ {R : Type u₁} {S : Type u₂} [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : Algebra R S] {T : Type u₃}
  [inst_3 : CommRing T] [inst_4 : Algebra R T] [inst_5 : Algebra S T] [inst_6 : IsScalarTower R S T] {ι : Type w₁}
  (Q : Algebra.Generators S T ι) (n : ι →₀ ℕ) (r : S),
  (Algebra.Generators.H1Cotangent.δAux R Q) ((MvPolynomial.monomial n) r) =
    (n.prod fun x1 x2 => Q.val x1 ^ x2) ⊗ₜ[S] (KaehlerDifferential.D R S) r
-- Mathlib.ModelTheory.FinitelyGenerated
FirstOrder.Language.Structure.FG.countable_embedding : ∀ {L : FirstOrder.Language} {M : Type u_1} [inst : L.Structure M] (N : Type u_2) [inst_1 : L.Structure N] [Countable N],
  FirstOrder.Language.Structure.FG L M → Countable (L.Embedding M N)
-- Std.Data.DTreeMap.Lemmas
Std.DTreeMap.Const.get?_filterMap : ∀ {α : Type u} {cmp : α → α → Ordering} {β : Type v} {γ : Type w} {t : Std.DTreeMap α (fun x => β) cmp}
  [inst : Std.TransCmp cmp] {f : α → β → Option γ} {k : α},
  Std.DTreeMap.Const.get? (Std.DTreeMap.filterMap f t) k =
    (Std.DTreeMap.Const.get? t k).pbind fun x h' => f (t.getKey k ⋯) x
-- Mathlib.Algebra.Order.Archimedean.Class
ArchimedeanClass.mk_right_le_mk_sub_iff : ∀ {M : Type u_1} [inst : AddCommGroup M] [inst_1 : LinearOrder M] [inst_2 : IsOrderedAddMonoid M] {a b : M},
  ArchimedeanClass.mk b ≤ ArchimedeanClass.mk (a - b) ↔ ArchimedeanClass.mk b ≤ ArchimedeanClass.mk a
-- Mathlib.Tactic.Ring.Common
Mathlib.Tactic.Ring.Common.ExSum.zero.sizeOf_spec : ∀ {u : Lean.Level} {α : Q(Type u)} {BaseType : Q(«$α») → Type} {sα : Q(CommSemiring «$α»)}
  [inst : (a : Q(«$α»)) → SizeOf (BaseType a)], sizeOf Mathlib.Tactic.Ring.Common.ExSum.zero = 1
-- Mathlib.Topology.List
Filter.Tendsto.cons : ∀ {β : Type u_2} [inst : TopologicalSpace β] {α : Type u_3} {f : α → β} {g : α → List β} {a : Filter α} {b : β}
  {l : List β},
  Filter.Tendsto f a (nhds b) → Filter.Tendsto g a (nhds l) → Filter.Tendsto (fun a => f a :: g a) a (nhds (b :: l))
-- Mathlib.CategoryTheory.Functor.Derived.RightDerived
/-- A functor `RF : D ⥤ H` is a right derived functor of `F : C ⥤ H`
if it is equipped with a natural transformation `α : F ⟶ L ⋙ RF`
which makes it a left Kan extension of `F` along `L`,
where `L : C ⥤ D` is a localization functor for `W : MorphismProperty C`.  -/
CategoryTheory.Functor.IsRightDerivedFunctor : {C : Type u_1} →
  {D : Type u_2} →
    {H : Type u_3} →
      [inst : CategoryTheory.Category.{v_1, u_1} C] →
        [inst_1 : CategoryTheory.Category.{v_3, u_2} D] →
          [inst_2 : CategoryTheory.Category.{v_5, u_3} H] →
            (RF : CategoryTheory.Functor D H) →
              {F : CategoryTheory.Functor C H} →
                {L : CategoryTheory.Functor C D} →
                  (F ⟶ L.comp RF) → (W : CategoryTheory.MorphismProperty C) → [L.IsLocalization W] → Prop
-- Mathlib.Analysis.Normed.Lp.ProdLp
/-- The `L^p` product of two linear isometries.  -/
LinearIsometry.withLpProdMap : (p : ENNReal) →
  {𝕜 : Type u_1} →
    {α : Type u_2} →
      {β : Type u_3} →
        {α' : Type u_5} →
          {β' : Type u_6} →
            [hp : Fact (1 ≤ p)] →
              [inst : Semiring 𝕜] →
                [inst_1 : SeminormedAddCommGroup α] →
                  [inst_2 : Module 𝕜 α] →
                    [inst_3 : SeminormedAddCommGroup β] →
                      [inst_4 : Module 𝕜 β] →
                        [inst_5 : SeminormedAddCommGroup α'] →
                          [inst_6 : Module 𝕜 α'] →
                            [inst_7 : SeminormedAddCommGroup β'] →
                              [inst_8 : Module 𝕜 β'] →
                                (α →ₗᵢ[𝕜] α') → (β →ₗᵢ[𝕜] β') → WithLp p (α × β) →ₗᵢ[𝕜] WithLp p (α' × β')
-- Mathlib.Data.EReal.Basic
EReal.coe_ennreal_ne_coe_ennreal_iff : ∀ {x y : ENNReal}, ↑x ≠ ↑y ↔ x ≠ y
-- Mathlib.Topology.ContinuousMap.Bounded.Basic
/-- The uniform distance between two bounded continuous functions.  -/
BoundedContinuousFunction.instDist : {α : Type u} →
  {β : Type v} → [inst : TopologicalSpace α] → [inst_1 : PseudoMetricSpace β] → Dist (BoundedContinuousFunction α β)
-- Std.Data.DTreeMap.Internal.Lemmas
Std.DTreeMap.Internal.Impl.size_insertMany_list_le : ∀ {α : Type u} {β : α → Type v} {instOrd : Ord α} {t : Std.DTreeMap.Internal.Impl α β} [Std.TransOrd α] (h : t.WF)
  {l : List ((a : α) × β a)}, (↑(t.insertMany l ⋯)).size ≤ t.size + l.length
-- Mathlib.Probability.Kernel.Invariance
ProbabilityTheory.Kernel.Invariant.def : ∀ {α : Type u_1} {mα : MeasurableSpace α} {κ : ProbabilityTheory.Kernel α α} {μ : MeasureTheory.Measure α},
  κ.Invariant μ → μ.bind ⇑κ = μ
-- Mathlib.Algebra.FreeMonoid.Count
FreeMonoid.countP'_one : ∀ {α : Type u_1} (p : α → Prop) [inst : DecidablePred p], FreeMonoid.countP' p 1 = 0
-- Mathlib.CategoryTheory.NatIso
/-- The dual of `ofComponents`  -/
CategoryTheory.NatIso.ofComponents' : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    {D : Type u₂} →
      [inst_1 : CategoryTheory.Category.{v₂, u₂} D] →
        {F G : CategoryTheory.Functor C D} →
          (app : (X : C) → F.obj X ≅ G.obj X) →
            autoParam
                (∀ {X Y : C} (f : Y ⟶ X),
                  CategoryTheory.CategoryStruct.comp (app Y).inv (F.map f) =
                    CategoryTheory.CategoryStruct.comp (G.map f) (app X).inv)
                CategoryTheory.NatIso.ofComponents'._auto_1 →
              (F ≅ G)
-- Mathlib.Topology.Algebra.InfiniteSum.SummationFilter
SummationFilter.unconditional.eq_1 : ∀ (β : Type u_2), SummationFilter.unconditional β = { filter := Filter.atTop }
-- Mathlib.Order.CompleteLattice.Basic
iSup₂_comm : ∀ {α : Type u_1} [inst : CompleteLattice α] {ι₁ : Sort u_8} {ι₂ : Sort u_9} {κ₁ : ι₁ → Sort u_10} {κ₂ : ι₂ → Sort u_11}
  (f : (i₁ : ι₁) → κ₁ i₁ → (i₂ : ι₂) → κ₂ i₂ → α),
  ⨆ i₁, ⨆ j₁, ⨆ i₂, ⨆ j₂, f i₁ j₁ i₂ j₂ = ⨆ i₂, ⨆ j₂, ⨆ i₁, ⨆ j₁, f i₁ j₁ i₂ j₂
-- Mathlib.GroupTheory.OrderOfElement
/-- If the additive order of `x` is finite, then `x` is an additive
unit with inverse `(addOrderOf x - 1) • x`.  -/
IsOfFinAddOrder.addUnit : {M : Type u_6} → [inst : AddMonoid M] → {x : M} → IsOfFinAddOrder x → AddUnits M
-- Std.Data.DTreeMap.Internal.Operations
Std.DTreeMap.Internal.Impl.Tree.mk.sizeOf_spec : ∀ {α : Type u} {β : α → Type v} {size : ℕ} [inst : SizeOf α] [inst_1 : (a : α) → SizeOf (β a)]
  (impl : Std.DTreeMap.Internal.Impl α β) (balanced_impl : impl.Balanced) (size_impl : impl.size = size),
  sizeOf { impl := impl, balanced_impl := balanced_impl, size_impl := size_impl } =
    1 + sizeOf impl + sizeOf balanced_impl + sizeOf size_impl
-- Mathlib.Analysis.Normed.Lp.lpSpace
lp.ext_continuousAddMonoidHom_iff : ∀ {α : Type u_3} {E : α → Type u_4} {p : ENNReal} [inst : (i : α) → NormedAddCommGroup (E i)] [inst_1 : DecidableEq α]
  {F : Type u_5} [inst_2 : AddCommMonoid F] [inst_3 : TopologicalSpace F] [T2Space F] [inst_5 : Fact (1 ≤ p)]
  {hp : p ≠ ⊤} {f g : ↥(lp E p) →ₜ+ F},
  f = g ↔ ∀ (i : α), f.comp (lp.singleContinuousAddMonoidHom E p i) = g.comp (lp.singleContinuousAddMonoidHom E p i)
-- Mathlib.GroupTheory.GroupAction.Hom
map_smul : ∀ {F : Type u_8} {M : Type u_9} {X : Type u_10} {Y : Type u_11} [inst : SMul M X] [inst_1 : SMul M Y]
  [inst_2 : FunLike F X Y] [MulActionHomClass F M X Y] (f : F) (c : M) (x : X), f (c • x) = c • f x
-- Mathlib.Computability.RegularExpressions
/-- `P.rmatch x` is true if and only if `P` matches `x`. This is a computable definition equivalent
to `matches'`.  -/
RegularExpression.rmatch : {α : Type u_1} → [DecidableEq α] → RegularExpression α → List α → Bool
-- Mathlib.Geometry.Convex.Cone.Pointed
PointedCone.ext_iff : ∀ {R : Type u_1} {E : Type u_2} [inst : Semiring R] [inst_1 : PartialOrder R] [inst_2 : IsOrderedRing R]
  [inst_3 : AddCommMonoid E] [inst_4 : Module R E] {C₁ C₂ : PointedCone R E}, C₁ = C₂ ↔ ∀ (x : E), x ∈ C₁ ↔ x ∈ C₂
-- Mathlib.GroupTheory.SpecificGroups.Cyclic
intEquivOfZPowersEqTop.congr_simp : ∀ {G : Type u_2} [inst : Infinite G] [inst_1 : Group G] (g g_1 : G) (e_g : g = g_1) (hg : Subgroup.zpowers g = ⊤),
  intEquivOfZPowersEqTop g hg = intEquivOfZPowersEqTop g_1 ⋯
-- Mathlib.Algebra.BigOperators.Finprod
finsum_mem_eq_sum_of_inter_support_eq : ∀ {α : Type u_1} {M : Type u_5} [inst : AddCommMonoid M] (f : α → M) {s : Set α} {t : Finset α},
  s ∩ Function.support f = ↑t ∩ Function.support f → ∑ᶠ (i : α) (_ : i ∈ s), f i = ∑ i ∈ t, f i
-- Lean.Elab.Do.PatternVar
Lean.Elab.Do.getLetPatDeclVars : Lean.TSyntax `Lean.Parser.Term.letPatDecl → Lean.Elab.TermElabM (Array Lean.Ident)
-- Lean.Elab.Term.TermElabM
Lean.Elab.Term.instInhabitedState : Inhabited Lean.Elab.Term.State
-- Mathlib.Computability.Encoding
/-- Deprecated alias for `encodingNatΓ'`.  -/
Computability.finEncodingNatΓ' : Computability.Encoding ℕ Computability.Γ'
-- Mathlib.CategoryTheory.Abelian.GrothendieckCategory.EnoughInjectives
CategoryTheory.IsGrothendieckAbelian.generatingMonomorphisms.exists_ordinal : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {G : C} [inst_1 : CategoryTheory.Abelian C]
  (hG : CategoryTheory.IsSeparator G) {X : C} [inst_2 : CategoryTheory.IsGrothendieckAbelian.{w, v, u} C]
  (A₀ : CategoryTheory.Subobject X),
  ∃ o j, transfiniteIterate (CategoryTheory.IsGrothendieckAbelian.generatingMonomorphisms.largerSubobject hG) j A₀ = ⊤
-- Mathlib.LinearAlgebra.Matrix.Defs
/-- `Matrix m n R` is the type of matrices with entries in `R`, whose rows are indexed by `m`
and whose columns are indexed by `n`.  -/
Matrix : Type u → Type u' → Type v → Type (max u u' v)
-- Mathlib.Algebra.Field.Basic
Commute.div_add_div : ∀ {K : Type u_1} [inst : DivisionSemiring K] {a b c d : K},
  Commute b c → Commute b d → b ≠ 0 → d ≠ 0 → a / b + c / d = (a * d + b * c) / (b * d)
-- Mathlib.AlgebraicTopology.SimplicialNerve
CategoryTheory.SimplicialThickening.instSimplicialCategory : (J : Type u_1) → [inst : LinearOrder J] → CategoryTheory.SimplicialCategory (CategoryTheory.SimplicialThickening J)
-- Init.Data.Vector.Lemmas
Vector.flatten_replicate_empty : ∀ {n : ℕ} {α : Type u_1}, (Vector.replicate n #v[]).flatten = #v[]
-- Mathlib.Data.Finsupp.Multiset
Sym.coe_equivNatSum_symm_apply : ∀ (α : Type u_1) [inst : DecidableEq α] (n : ℕ) (P : { P // (P.sum fun x => id) = n }),
  ↑((Sym.equivNatSum α n).symm P) = Finsupp.toMultiset ↑P
-- Mathlib.Logic.Equiv.Set
/-- **Alias** of `Equiv.setOfPred_apply_symm_eq_image_setOfPred`. -/
Equiv.setOf_apply_symm_eq_image_setOf : ∀ {α : Type u_3} {β : Type u_4} (e : α ≃ β) (p : α → Prop), {b | p (e.symm b)} = ⇑e '' {a | p a}
-- Std.Data.DTreeMap.Internal.Operations
/-- Slower version of `insertMany` which can be used in absence of balance information but still
assumes the preconditions of `insertMany`, otherwise might panic.
 -/
Std.DTreeMap.Internal.Impl.Const.insertMany! : {α : Type u} →
  {β : Type v} →
    [inst : Ord α] →
      {ρ : Type w} →
        [ForIn Id ρ (α × β)] →
          (t : Std.DTreeMap.Internal.Impl α fun x => β) →
            ρ → Std.DTreeMap.Internal.Impl.Const.IteratedSlowInsertionInto t
-- Mathlib.MeasureTheory.MeasurableSpace.Prod
/-- The comap of a product is the supremum of the comaps.  -/
MeasurableSpace.comap_prodMk : ∀ {α : Type u_3} {β : Type u_4} {γ : Type u_5} {mβ : MeasurableSpace β} {mγ : MeasurableSpace γ} (X : α → β)
  (Y : α → γ),
  MeasurableSpace.comap (fun ω => (X ω, Y ω)) (mβ.prod mγ) = MeasurableSpace.comap X mβ ⊔ MeasurableSpace.comap Y mγ
-- Batteries.Tactic.GeneralizeProofs
Batteries.Tactic.GeneralizeProofs.Config.mk : ℕ → Bool → Bool → Batteries.Tactic.GeneralizeProofs.Config
-- Mathlib.MeasureTheory.OuterMeasure.Induced
MeasureTheory.OuterMeasure.exists_measurable_superset_eq_trim : ∀ {α : Type u_1} [inst : MeasurableSpace α] (m : MeasureTheory.OuterMeasure α) (s : Set α),
  ∃ t, s ⊆ t ∧ MeasurableSet t ∧ m t = m.trim s
-- Mathlib.Analysis.Normed.Field.UnitBall
Metric.unitClosedBall.coe_zero : ∀ {𝕜 : Type u_1} [inst : Zero 𝕜] [inst_1 : PseudoMetricSpace 𝕜], ↑0 = 0
-- Mathlib.Algebra.Order.Field.Basic
lt_div_iff_of_neg' : ∀ {α : Type u_2} [inst : Field α] [inst_1 : PartialOrder α] [PosMulReflectLT α] [IsStrictOrderedRing α] {a b c : α},
  c < 0 → (a < b / c ↔ b < c * a)
-- Init.Grind.Ring.CommSolver
Lean.Grind.CommRing.one_eq_zero_unsat : ∀ {α : Type u_1} [inst : Lean.Grind.Field α] (ctx : Lean.Grind.CommRing.Context α) (p : Lean.Grind.CommRing.Poly),
  Lean.Grind.CommRing.one_eq_zero_unsat_cert p = true → Lean.Grind.CommRing.Poly.denote ctx p = 0 → False
-- Mathlib.Order.Filter.Defs
/-- The coheyting negation of a filter is the complement of its kernel.  -/
Filter.instHNot : {α : Type u_1} → HNot (Filter α)
-- Std.Data.DTreeMap.Raw.Lemmas
Std.DTreeMap.Raw.Const.size_alter_eq_self_of_mem : ∀ {α : Type u} {cmp : α → α → Ordering} {β : Type v} {t : Std.DTreeMap.Raw α (fun x => β) cmp} [Std.TransCmp cmp],
  t.WF →
    ∀ {k : α} {f : Option β → Option β},
      k ∈ t → (f (Std.DTreeMap.Raw.Const.get? t k)).isSome = true → (Std.DTreeMap.Raw.Const.alter t k f).size = t.size
-- Mathlib.Topology.Metrizable.Basic
TopologicalSpace.t2Space_of_metrizableSpace : ∀ {X : Type u_2} [inst : TopologicalSpace X] [TopologicalSpace.MetrizableSpace X], T2Space X
-- Mathlib.Algebra.Group.Prod
Prod.instInvolutiveNeg : {M : Type u_3} → {N : Type u_4} → [InvolutiveNeg M] → [InvolutiveNeg N] → InvolutiveNeg (M × N)
-- Mathlib.RingTheory.LinearDisjoint
/-- If `A` and `B` are flat `R`-algebras, such that `A ⊗[R] B` is a field, then one of `A` and `B`
is algebraic over `R`.  -/
Algebra.TensorProduct.isAlgebraic_of_isField : ∀ (R : Type u) [inst : CommRing R] (A : Type v) [inst_1 : CommRing A] (B : Type w) [inst_2 : CommRing B]
  [inst_3 : Algebra R A] [inst_4 : Algebra R B] [Module.Flat R A] [Module.Flat R B],
  IsField (TensorProduct R A B) → Algebra.IsAlgebraic R A ∨ Algebra.IsAlgebraic R B
-- Mathlib.CategoryTheory.Bicategory.Functor.StrictlyUnitary
CategoryTheory.StrictlyUnitaryLaxFunctor.mk'_map₂ : ∀ {B : Type u₁} [inst : CategoryTheory.Bicategory B] {C : Type u₂} [inst_1 : CategoryTheory.Bicategory C]
  (S : CategoryTheory.StrictlyUnitaryLaxFunctorCore B C) {a b : B} {f g : a ⟶ b} (a_1 : f ⟶ g),
  (CategoryTheory.StrictlyUnitaryLaxFunctor.mk' S).map₂ a_1 = S.map₂ a_1
-- Mathlib.Analysis.RCLike.BoundedContinuous
BoundedContinuousFunction.comp.congr_simp : ∀ {α : Type u} {β : Type v} {γ : Type w} [inst : TopologicalSpace α] [inst_1 : PseudoMetricSpace β]
  [inst_2 : PseudoMetricSpace γ] (G G_1 : β → γ) (e_G : G = G_1) {C C_1 : NNReal} (e_C : C = C_1)
  (H : LipschitzWith C G) (f f_1 : BoundedContinuousFunction α β),
  f = f_1 → BoundedContinuousFunction.comp G H f = BoundedContinuousFunction.comp G_1 ⋯ f_1
-- Mathlib.Topology.Semicontinuity.Defs
lowerHemicontinuousWithinAt_univ_iff : ∀ {α : Type u_1} {β : Type u_2} [inst : TopologicalSpace α] [inst_1 : TopologicalSpace β] {f : α → Set β} {x : α},
  LowerHemicontinuousWithinAt f Set.univ x ↔ LowerHemicontinuousAt f x