mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Tactic.GCongr.Core
/-- - Insert a `GCongrLemma` in the correct place in a list of lemmas.  -/
_private.Mathlib.Tactic.GCongr.Core.0.Mathlib.Tactic.GCongr.addGCongrLemmaEntry.insert : Mathlib.Tactic.GCongr.GCongrLemma → List Mathlib.Tactic.GCongr.GCongrLemma → List Mathlib.Tactic.GCongr.GCongrLemma
-- Mathlib.SetTheory.Cardinal.Continuum
Cardinal.continuum_le_lift : ∀ {c : Cardinal.{u}}, Cardinal.continuum ≤ Cardinal.lift.{v, u} c ↔ Cardinal.continuum ≤ c
-- Mathlib.RingTheory.Localization.Integer
IsLocalization.isInteger_smul : ∀ {R : Type u_1} [inst : CommSemiring R] {S : Type u_2} [inst_1 : CommSemiring S] [inst_2 : Algebra R S] {a : R}
  {b : S}, IsLocalization.IsInteger R b → IsLocalization.IsInteger R (a • b)
-- Mathlib.MeasureTheory.Integral.Bochner.Set
/-- If a function vanishes almost everywhere on `t \ s` with `s ⊆ t`, then its integrals on `s`
and `t` coincide if `t` is null-measurable.  -/
MeasureTheory.setIntegral_eq_of_subset_of_ae_sdiff_eq_zero : ∀ {X : Type u_1} {E : Type u_3} {mX : MeasurableSpace X} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E]
  {f : X → E} {s t : Set X} {μ : MeasureTheory.Measure X},
  MeasureTheory.NullMeasurableSet t μ →
    s ⊆ t → (∀ᵐ (x : X) ∂μ, x ∈ t \ s → f x = 0) → ∫ (x : X) in t, f x ∂μ = ∫ (x : X) in s, f x ∂μ
-- Mathlib.Analysis.Normed.Ring.WithAbs
WithAbs.equiv_apply : ∀ {R : Type u_1} {S : Type u_2} [inst : Semiring S] [inst_1 : PartialOrder S] [inst_2 : Semiring R]
  (v : AbsoluteValue R S) (self : WithAbs v), (WithAbs.equiv v) self = self.ofAbs
-- Mathlib.Order.Hom.WithTopBot
OrderHom.withBotMap_coe : ∀ {α : Type u_1} {β : Type u_2} [inst : Preorder α] [inst_1 : Preorder β] (f : α →o β), ⇑f.withBotMap = WithBot.map ⇑f
-- Lean.Elab.Do.Basic
Lean.Elab.Do.instInhabitedReturnCont.default : Lean.Elab.Do.ReturnCont
-- Mathlib.Algebra.Group.Subgroup.Map
AddSubgroup.comap_equiv_eq_map_symm : ∀ {G : Type u_1} [inst : AddGroup G] {N : Type u_5} [inst_1 : AddGroup N] (f : N ≃+ G) (K : AddSubgroup G),
  AddSubgroup.comap (↑f) K = AddSubgroup.map (↑f.symm) K
-- Mathlib.Order.Minimal
OrderIso.setOfPredMaximalIsoSetOfPredMinimal.eq_1 : ∀ {α : Type u_2} {β : Type u_3} [inst : Preorder α] [inst_1 : Preorder β] {s : Set α} {t : Set β} (f : ↑s ≃o (↑t)ᵒᵈ),
  f.setOfPredMaximalIsoSetOfPredMinimal =
    { toFun := fun x => ⟨↑(f ⟨↑x, ⋯⟩), ⋯⟩, invFun := fun x => ⟨↑(f.symm ⟨↑x, ⋯⟩), ⋯⟩, left_inv := ⋯, right_inv := ⋯,
      map_rel_iff' := ⋯ }
-- Mathlib.CategoryTheory.Sites.IsSheafFor
CategoryTheory.Presieve.Arrows.Compatible.familyOfElements_ofArrows_mk : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {P : CategoryTheory.Functor Cᵒᵖ (Type w)} {B : C}
  {I : Type u_1} {X : I → C} {π : (i : I) → X i ⟶ B} {x : (i : I) → P.obj (Opposite.op (X i))}
  (hx : CategoryTheory.Presieve.Arrows.Compatible P π x) (i : I), hx.familyOfElements (π i) ⋯ = x i
-- Std.Data.DTreeMap.Raw.Lemmas
Std.DTreeMap.Raw.Equiv.erase : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t₁ t₂ : Std.DTreeMap.Raw α β cmp} [Std.TransCmp cmp],
  t₁.WF → t₂.WF → t₁.Equiv t₂ → ∀ (k : α), (t₁.erase k).Equiv (t₂.erase k)
-- Mathlib.Order.Heyting.Regular
Heyting.IsRegular.eq : ∀ {α : Type u_1} [inst : Compl α] {a : α}, Heyting.IsRegular a → aᶜᶜ = a
-- Mathlib.Topology.ContinuousMap.Defs
/-- Continuity  -/
ContinuousMapClass.map_continuous : ∀ {F : Type u_1} {X : outParam (Type u_2)} {Y : outParam (Type u_3)} {inst : TopologicalSpace X}
  {inst_1 : TopologicalSpace Y} {inst_2 : FunLike F X Y} [self : ContinuousMapClass F X Y] (f : F), Continuous ⇑f
-- Mathlib.Logic.Relation
/-- **Alias** of `Relation.isTrans_join`. -/
Relation.transitive_join : ∀ {α : Type u_1} {r : α → α → Prop} [IsTrans α r],
  (∀ (a b c : α), r a b → r a c → Relation.Join r b c) → IsTrans α (Relation.Join r)
-- Init.Prelude
/-- The list of trace messages that have been produced, each with a trace
class and a message.  -/
Lean.Macro.State.traceMsgs : Lean.Macro.State → List (Lean.Name × String)
-- Mathlib.Order.SemiconjSup
/-- Consider two actions `f₁ f₂ : G → α → α` of a group on a conditionally complete lattice by order
isomorphisms. Suppose that each set $s(x)=\{f_1(g)^{-1} (f_2(g)(x)) | g \in G\}$ is bounded above.
Then the map `x ↦ sSup s(x)` semiconjugates each `f₁ g'` to `f₂ g'`.

This is a version of Proposition 5.4 from [Étienne Ghys, Groupes d'homéomorphismes du cercle et
cohomologie bornée][ghys87:groupes].  -/
Function.csSup_div_semiconj : ∀ {α : Type u_1} {G : Type u_4} [inst : ConditionallyCompleteLattice α] [inst_1 : Group G] (f₁ f₂ : G →* α ≃o α),
  (∀ (x : α), BddAbove (Set.range fun g => (f₁ g)⁻¹ ((f₂ g) x))) →
    ∀ (g : G), Function.Semiconj (fun x => ⨆ g', (f₁ g')⁻¹ ((f₂ g') x)) ⇑(f₂ g) ⇑(f₁ g)
-- Init.Data.Dyadic.Basic
Dyadic.add_comm : ∀ (x y : Dyadic), x + y = y + x
-- Mathlib.MeasureTheory.VectorMeasure.Integral
MeasureTheory.VectorMeasure.transpose_sub_cbm : ∀ {X : Type u_2} {E : Type u_4} {F : Type u_5} {G : Type u_6} {mX : MeasurableSpace X} [inst : NormedAddCommGroup E]
  [inst_1 : NormedSpace ℝ E] [inst_2 : NormedAddCommGroup F] [inst_3 : NormedSpace ℝ F] [inst_4 : NormedAddCommGroup G]
  [inst_5 : NormedSpace ℝ G] (μ : MeasureTheory.VectorMeasure X F) (B C : E →L[ℝ] F →L[ℝ] G),
  μ.transpose (B - C) = μ.transpose B - μ.transpose C
-- Mathlib.Topology.Algebra.Monoid
Filter.TendstoNhdsWithinIoi.mul_const : ∀ {α : Type u_2} {𝕜 : Type u_6} [inst : Preorder 𝕜] [inst_1 : Zero 𝕜] [inst_2 : Mul 𝕜] [inst_3 : TopologicalSpace 𝕜]
  [SeparatelyContinuousMul 𝕜] {l : Filter α} {f : α → 𝕜} {b c : 𝕜},
  0 < b →
    ∀ [MulPosStrictMono 𝕜],
      Filter.Tendsto f l (nhdsWithin c (Set.Ioi c)) →
        Filter.Tendsto (fun a => f a * b) l (nhdsWithin (c * b) (Set.Ioi (c * b)))
-- Mathlib.MeasureTheory.Integral.IntegralEqImproper
/-- If the derivative of a function defined on the real line is integrable close to `-∞`, then
the function has a limit at `-∞`.  -/
MeasureTheory.tendsto_limUnder_of_hasDerivAt_of_integrableOn_Iic : ∀ {E : Type u_1} {f f' : ℝ → E} {a : ℝ} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] [CompleteSpace E],
  (∀ x ∈ Set.Iic a, HasDerivAt f (f' x) x) →
    MeasureTheory.IntegrableOn f' (Set.Iic a) MeasureTheory.volume →
      Filter.Tendsto f Filter.atBot (nhds (Filter.atBot.limUnder f))
-- Mathlib.Computability.Partrec
Nat.rfind_min' : ∀ {p : ℕ → Bool} {m : ℕ}, p m = true → ∃ n ∈ Nat.rfind ↑p, n ≤ m
-- Mathlib.LinearAlgebra.Matrix.SpecialLinearGroup
/-- The transvection `transvection i j hij b` acts on `e_i = Pi.single i 1` as the identity.  -/
Matrix.SpecialLinearGroup.transvection_smul_single_fst : ∀ {ι : Type u_1} {F : Type u_2} [inst : DecidableEq ι] [inst_1 : Fintype ι] [inst_2 : CommRing F] {i j : ι}
  (hij : i ≠ j) (b : F), Matrix.SpecialLinearGroup.transvection hij b • Pi.single i 1 = Pi.single i 1
-- Mathlib.Algebra.Module.Torsion.Basic
Submodule.torsion'_torsion'_eq_top : ∀ {R : Type u_1} {M : Type u_2} [inst : CommSemiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M] (S : Type u_3)
  [inst_3 : CommMonoid S] [inst_4 : DistribMulAction S M] [inst_5 : SMulCommClass S R M],
  Submodule.torsion' R (↥(Submodule.torsion' R M S)) S = ⊤
-- Mathlib.CategoryTheory.Limits.Shapes.Pullback.Pasting
CategoryTheory.Limits.inl_pushoutRightPushoutInlIso_inv_assoc : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {W X Y Z : C} (f : X ⟶ Y) (g : X ⟶ Z) (f' : Y ⟶ W)
  [inst_1 : CategoryTheory.Limits.HasPushout f g]
  [inst_2 : CategoryTheory.Limits.HasPushout f' (CategoryTheory.Limits.pushout.inl f g)] {Z_1 : C}
  (h : CategoryTheory.Limits.pushout f' (CategoryTheory.Limits.pushout.inl f g) ⟶ Z_1),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pushout.inl (CategoryTheory.CategoryStruct.comp f f') g)
      (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pushoutRightPushoutInlIso f g f').inv h) =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pushout.inl f' (CategoryTheory.Limits.pushout.inl f g)) h
-- Mathlib.MeasureTheory.Measure.AEMeasurable
AEMeasurable.mono' : ∀ {α : Type u_2} {β : Type u_3} {m0 : MeasurableSpace α} [inst : MeasurableSpace β] {f : α → β}
  {μ ν : MeasureTheory.Measure α}, AEMeasurable f μ → ν.AbsolutelyContinuous μ → AEMeasurable f ν
-- Mathlib.RingTheory.Derivation.Basic
/-- See Note [custom simps projection]  -/
Derivation.Simps.apply : {R : Type u_1} →
  {A : Type u_2} →
    {M : Type u_4} →
      [inst : CommSemiring R] →
        [inst_1 : CommSemiring A] →
          [inst_2 : AddCommMonoid M] →
            [inst_3 : Algebra R A] → [inst_4 : Module A M] → [inst_5 : Module R M] → Derivation R A M → A → M
-- Init.Data.Int.OfNat
Nat.ToInt.pow_congr : ∀ {a : ℕ} (k : ℕ) (a' : ℤ), ↑a = a' → ↑(a ^ k) = a' ^ k
-- Mathlib.CategoryTheory.Sites.Grothendieck
/-- The shape of the multiequalizer diagrams associated to `S : J.Cover X`.  -/
CategoryTheory.GrothendieckTopology.Cover.shape : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    {X : C} → {J : CategoryTheory.GrothendieckTopology C} → J.Cover X → CategoryTheory.Limits.MulticospanShape
-- Mathlib.NumberTheory.PrimeCounting
Nat.primesBelow_eq_primesLE_sub_one : ∀ (n : ℕ), n.primesBelow = (n - 1).primesLE
-- Std.Async.TCP
/-- Sends data through the client socket.
 -/
Std.Async.TCP.Socket.Client.send : Std.Async.TCP.Socket.Client → ByteArray → Std.Async.Async Unit
-- Mathlib.Analysis.InnerProductSpace.WeakOperatorTopology
ContinuousLinearMapWOT.continuous_iff : ∀ {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [inst : RCLike 𝕜] [inst_1 : AddCommGroup E] [inst_2 : TopologicalSpace E]
  [inst_3 : Module 𝕜 E] [inst_4 : NormedAddCommGroup F] [inst_5 : InnerProductSpace 𝕜 F] [CompleteSpace F]
  {α : Type u_4} [inst_7 : TopologicalSpace α] {f : α → E →WOT[𝕜] F},
  Continuous f ↔ ∀ (x : E) (y : F), Continuous fun x_1 => inner 𝕜 y ((f x_1) x)
-- Mathlib.Topology.Category.TopCat.Adjunctions
/-- Equipping a type with the discrete topology is left adjoint to the forgetful functor
`Top ⥤ Type`.  -/
TopCat.adj₁ : TopCat.discrete ⊣ CategoryTheory.forget TopCat
-- Mathlib.Order.LatticeIntervals
Set.Ioc.coe_top : ∀ {α : Type u_1} [inst : PartialOrder α] (a b : α) [inst_1 : Fact (a < b)], ↑⊤ = b
-- Mathlib.Algebra.Module.LinearMap.Index
/-- The index of a linear map with sign convention `index = dim ker - dim coker`.

In the case that either the kernel or cokernel has infinite rank, the value is junk.  -/
LinearMap.index : {M : Type u_1} →
  {N : Type u_2} →
    [inst : AddCommGroup M] →
      [inst_1 : AddCommGroup N] →
        {R : Type u_3} → [inst_2 : Ring R] → [inst_3 : Module R M] → [inst_4 : Module R N] → (M →ₗ[R] N) → ℤ
-- Mathlib.LinearAlgebra.TensorProduct.Tower
TensorProduct.AlgebraTensorModule.map_id : ∀ {R : Type uR} {A : Type uA} {M : Type uM} {N : Type uN} [inst : CommSemiring R] [inst_1 : Semiring A]
  [inst_2 : Algebra R A] [inst_3 : AddCommMonoid M] [inst_4 : Module R M] [inst_5 : Module A M]
  [inst_6 : IsScalarTower R A M] [inst_7 : AddCommMonoid N] [inst_8 : Module R N],
  TensorProduct.AlgebraTensorModule.map LinearMap.id LinearMap.id = LinearMap.id
-- Lean.Meta.Sym.SymM
Lean.Meta.Sym.SharedExprs.bfalseExpr : Lean.Meta.Sym.SharedExprs → Lean.Expr
-- Mathlib.Algebra.Module.ZLattice.Basic
ZSpan.fract_apply : ∀ {E : Type u_1} {ι : Type u_2} {K : Type u_3} [inst : NormedField K] [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace K E] (b : Module.Basis ι K E) [inst_3 : LinearOrder K] [inst_4 : IsStrictOrderedRing K]
  [inst_5 : FloorRing K] [inst_6 : Fintype ι] (m : E), ZSpan.fract b m = m - ↑(ZSpan.floor b m)
-- Lean.Expr
/-- Optimized version of `Expr.mkData` for applications.  -/
Lean.Expr.mkAppData : Lean.Expr.Data → Lean.Expr.Data → Lean.Expr.Data
-- Mathlib.Data.Num.ZNum
ZNum.bit0.eq_1 : ZNum.zero.bit0 = 0
-- Mathlib.Order.RelIso.Basic
/-- `fun b ↦ Prod.mk a b` as a relation embedding.  -/
RelEmbedding.prodLexMkLeft : {α : Type u_1} → {β : Type u_2} → {r : α → α → Prop} → (s : β → β → Prop) → {a : α} → ¬r a a → s ↪r Prod.Lex r s
-- Mathlib.Algebra.Category.AlgCat.Limits
AlgCat.instRingElemForallObjCompForgetAlgHomCarrierSections : {R : Type u} →
  [inst : CommRing R] →
    {J : Type v} →
      [inst_1 : CategoryTheory.Category.{t, v} J] →
        (F : CategoryTheory.Functor J (AlgCat R)) → Ring ↑(F.comp (CategoryTheory.forget (AlgCat R))).sections
-- Mathlib.NumberTheory.FLT.Four
Fermat42.comm : ∀ {a b c : ℤ}, Fermat42 a b c ↔ Fermat42 b a c
-- Init.Data.Rat.Lemmas
Rat.mk_eq_mkRat : ∀ (num : ℤ) (den : ℕ) (nz : den ≠ 0) (c : num.natAbs.Coprime den),
  { num := num, den := den, den_nz := nz, reduced := c } = mkRat num den
-- Std.Data.DTreeMap.Lemmas
Std.DTreeMap.maxKey_eq_get_maxKey? : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t : Std.DTreeMap α β cmp} [inst : Std.TransCmp cmp]
  {he : t.isEmpty = false}, t.maxKey he = t.maxKey?.get ⋯
-- Mathlib.LinearAlgebra.Contraction
dualTensorHomEquivOfBasis_symm_cancel_right : ∀ {ι : Type u_1} {R : Type u_2} {M : Type u_3} {N : Type u_4} [inst : CommSemiring R] [inst_1 : AddCommMonoid M]
  [inst_2 : AddCommMonoid N] [inst_3 : Module R M] [inst_4 : Module R N] (b : Module.Basis ι R M)
  [inst_5 : DecidableEq ι] [inst_6 : Fintype ι] (x : M →ₗ[R] N),
  (dualTensorHom R M N) ((dualTensorHomEquivOfBasis b).symm x) = x
-- Mathlib.Data.Nat.ModEq
Nat.odd_of_mod_four_eq_three : ∀ {n : ℕ}, n % 4 = 3 → n % 2 = 1
-- Init.Data.Iterators.Lemmas.Consumers.Monadic.Loop
Std.IterM.fold_eq_forIn : ∀ {α β γ : Type w} {m : Type w → Type w'} [inst : Std.Iterator α m β] [Std.Iterators.Finite α m] [inst_2 : Monad m]
  [inst_3 : Std.IteratorLoop α m m] {f : γ → β → γ} {init : γ} {it : Std.IterM m β},
  Std.IterM.fold f init it = forIn it init fun x acc => pure (ForInStep.yield (f acc x))
-- Lean.Meta.Tactic.Subst
Lean.Meta.substSomeVar? : Lean.MVarId → Lean.MetaM (Option Lean.MVarId)
-- Mathlib.Algebra.Star.Conjneg
conjneg_conjneg : ∀ {G : Type u_2} {R : Type u_3} [inst : AddGroup G] [inst_1 : CommSemiring R] [inst_2 : StarRing R] (f : G → R),
  conjneg (conjneg f) = f
-- Init.Data.Iterators.Lemmas.Consumers.Loop
_private.Init.Data.Iterators.Lemmas.Consumers.Loop.0.List.findSomeM?_cons.match_1.eq_1 : ∀ {β : Type u_1} (motive : Option β → Sort u_2) (b : β) (h_1 : (b : β) → motive (some b)) (h_2 : Unit → motive none),
  (match some b with
    | some b => h_1 b
    | none => h_2 ()) =
    h_1 b
-- Mathlib.RingTheory.Ideal.Quotient.Nilpotent
Ideal.Quotient.isUnit_mk_pow_iff_isUnit_mk : ∀ {S : Type u_1} [inst : CommRing S] (I : Ideal S) {x : S} {n : ℕ},
  n ≠ 0 → (IsUnit ((Ideal.Quotient.mk (I ^ n)) x) ↔ IsUnit ((Ideal.Quotient.mk I) x))
-- Std.Data.Iterators.Producers.Monadic.Array
/-- Returns a finite monadic iterator for the given array starting at the given index.
The iterator yields the elements of the array in order and then terminates.

The pure version of this iterator is `Array.iterFromIdx`.

**Termination properties:**

* `Finite` instance: always
* `Productive` instance: always
 -/
Array.iterFromIdxM : {α : Type w} → Array α → (m : Type w → Type w') → ℕ → [Pure m] → Std.IterM m α
-- Mathlib.CategoryTheory.Limits.Final
CategoryTheory.Functor.Final.comp_reflectsColimit : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  (F : CategoryTheory.Functor C D) [F.Final] {E : Type u₃} [inst_3 : CategoryTheory.Category.{v₃, u₃} E]
  {G : CategoryTheory.Functor D E} {B : Type u₄} [inst_4 : CategoryTheory.Category.{v₄, u₄} B]
  {H : CategoryTheory.Functor E B} [CategoryTheory.Limits.ReflectsColimit G H],
  CategoryTheory.Limits.ReflectsColimit (F.comp G) H
-- Std.Data.TreeMap.Raw.Lemmas
Std.TreeMap.Raw.getElem!_erase : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Std.TreeMap.Raw α β cmp} [Std.TransCmp cmp]
  [inst : Inhabited β], t.WF → ∀ {k a : α}, (t.erase k)[a]! = if cmp k a = Ordering.eq then default else t[a]!
-- Mathlib.RingTheory.PowerSeries.WeierstrassPreparation
/-- The quotient `q` and the remainder `r` in the Weierstrass division are unique.

This result is stated using two `PowerSeries.IsWeierstrassDivision` assertions, and only requires
the ring being Hausdorff with respect to the maximal ideal. If you want `q` and `r` equal to
`f /ʷ g` and `f %ʷ g`, use `PowerSeries.IsWeierstrassDivision.unique`
instead, which requires the ring being complete with respect to the maximal ideal.  -/
PowerSeries.IsWeierstrassDivision.elim : ∀ {A : Type u_1} [inst : CommRing A] [inst_1 : IsLocalRing A] {f g : PowerSeries A},
  (PowerSeries.map (IsLocalRing.residue A)) g ≠ 0 →
    ∀ [IsHausdorff (IsLocalRing.maximalIdeal A) A] {q q' : PowerSeries A} {r r' : Polynomial A},
      f.IsWeierstrassDivision g q r → f.IsWeierstrassDivision g q' r' → q = q' ∧ r = r'
-- Mathlib.Algebra.Group.Pointwise.Set.Basic
Set.isAddUnit_singleton : ∀ {α : Type u_2} [inst : AddGroup α] (a : α), IsAddUnit {a}
-- Mathlib.LinearAlgebra.Basis.MulOpposite
MulOpposite.rank : ∀ {R : Type u_1} {H : Type u_2} [inst : Semiring R] [StrongRankCondition R] [inst_2 : AddCommMonoid H]
  [inst_3 : Module R H] [Module.Free R H], Module.rank R Hᵐᵒᵖ = Module.rank R H
-- Mathlib.Algebra.Category.Semigrp.Basic
AddMagmaCat.of.eq_1 : ∀ (M : Type u) [inst : Add M], AddMagmaCat.of M = { carrier := M, str := inst }
-- Mathlib.FieldTheory.Finite.Extension
FiniteField.instFiniteDimensionalZModExtension : ∀ (k : Type u_1) [inst : Field k] (p : ℕ) [inst_1 : Fact (Nat.Prime p)] [inst_2 : CharP k p] (n : ℕ),
  FiniteDimensional (ZMod p) (FiniteField.Extension k p n)
-- Mathlib.Algebra.Tropical.Basic
Tropical.mulLeftMono : ∀ {R : Type u} [inst : LE R] [inst_1 : Add R] [AddLeftMono R], MulLeftMono (Tropical R)
-- Mathlib.CategoryTheory.Limits.Presentation
/-- The natural maps `sᵢ : X ⟶ Dᵢ`.  -/
CategoryTheory.Limits.LimitPresentation.π : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    {J : Type w} →
      [inst_1 : CategoryTheory.Category.{t, w} J] →
        {X : C} →
          (self : CategoryTheory.Limits.LimitPresentation J X) → (CategoryTheory.Functor.const J).obj X ⟶ self.diag
-- Mathlib.RingTheory.LinearDisjoint
Subalgebra.LinearDisjoint.algebraMap_basisOfBasisRight_repr_apply : ∀ {R : Type u} {S : Type v} [inst : CommSemiring R] [inst_1 : CommSemiring S] [inst_2 : Algebra R S]
  {A B : Subalgebra R S} (H : A.LinearDisjoint B) (H' : A ⊔ B = ⊤) {ι : Type u_1} (b : Module.Basis ι R ↥B) (x : ↥B)
  (i : ι), (algebraMap (↥A) S) (((H.basisOfBasisRight H' b).repr ↑x) i) = (algebraMap R S) ((b.repr x) i)
-- Mathlib.LinearAlgebra.DFinsupp
DFinsupp.sigmaCurryLEquiv_apply : ∀ {ι : Type u_1} {R : Type u_3} [inst : Semiring R] [inst_1 : DecidableEq ι] {α : ι → Type u_7}
  {M : (i : ι) → α i → Type u_8} [inst_2 : (i : ι) → (j : α i) → AddCommMonoid (M i j)]
  [inst_3 : (i : ι) → (j : α i) → Module R (M i j)] (a : Π₀ (i : (x : ι) × α x), M i.fst i.snd),
  DFinsupp.sigmaCurryLEquiv a = DFinsupp.sigmaCurryEquiv a
-- ProofWidgets.Component.RefreshComponent
ProofWidgets.RefreshComponent.instTypeNameRefreshRef : TypeName ProofWidgets.RefreshComponent.RefreshRef
-- Mathlib.Probability.Process.Filtration
MeasureTheory.Filtration.instIsRightContinuousRightCont : ∀ {Ω : Type u_1} {ι : Type u_2} {m : MeasurableSpace Ω} [inst : PartialOrder ι] {𝓕 : MeasureTheory.Filtration ι m},
  𝓕.rightCont.IsRightContinuous
-- Init.Prelude
ReaderT.instMonadLift : {ρ : Type u} → {m : Type u → Type v} → MonadLift m (ReaderT ρ m)
-- Mathlib.LinearAlgebra.TensorProduct.Map
LinearMap.lTensor_sub : ∀ {R : Type u_1} [inst : CommSemiring R] {M : Type u_2} {N : Type u_3} {P : Type u_4} [inst_1 : AddCommGroup M]
  [inst_2 : AddCommMonoid N] [inst_3 : AddCommGroup P] [inst_4 : Module R M] [inst_5 : Module R N] [inst_6 : Module R P]
  (f g : N →ₗ[R] P), LinearMap.lTensor M (f - g) = LinearMap.lTensor M f - LinearMap.lTensor M g
-- Mathlib.Order.CompleteLattice.Basic
le_iSup₂_of_le : ∀ {α : Type u_1} {ι : Sort u_4} {κ : ι → Sort u_6} [inst : CompleteLattice α] {a : α} {f : (i : ι) → κ i → α} (i : ι)
  (j : κ i), a ≤ f i j → a ≤ ⨆ i, ⨆ j, f i j
-- Mathlib.Algebra.Free
FreeSemigroup.hom_ext : ∀ {α : Type u} {β : Type v} [inst : Mul β] {f g : FreeSemigroup α →ₙ* β},
  ⇑f ∘ FreeSemigroup.of = ⇑g ∘ FreeSemigroup.of → f = g
-- Mathlib.Tactic.ComputeAsymptotics.Multiseries.Corecursion
/-- The operation `cons hd ·` is friendly.  -/
Tactic.ComputeAsymptotics.Seq.FriendlyOperation.cons : ∀ {α : Type u_1} (hd : α), Tactic.ComputeAsymptotics.Seq.FriendlyOperation (Stream'.Seq.cons hd)
-- Mathlib.Combinatorics.SimpleGraph.Subgraph
/-- `coe` can be embedded in `spanningCoe`.  -/
SimpleGraph.Subgraph.coeEmbeddingSpanningCoe : {V : Type u} → {G : SimpleGraph V} → (G' : G.Subgraph) → G'.coe ↪g G'.spanningCoe
-- Mathlib.Analysis.Complex.Basic
RCLike.complexRingEquiv.congr_simp : ∀ {𝕜 : Type u_2} [inst : RCLike 𝕜] (h : RCLike.im RCLike.I = 1), RCLike.complexRingEquiv h = RCLike.complexRingEquiv h
-- Mathlib.RingTheory.FiniteType
/-- An algebra is finitely generated if and only if it is a quotient
of a free algebra whose variables are indexed by a finset.  -/
Algebra.FiniteType.iff_quotient_freeAlgebra : ∀ {R : Type uR} {A : Type uA} [inst : CommSemiring R] [inst_1 : Semiring A] [inst_2 : Algebra R A],
  Algebra.FiniteType R A ↔ ∃ s f, Function.Surjective ⇑f
-- Mathlib.Algebra.AddConstMap.Equiv
AddConstEquiv.instMul : {G : Type u_1} → [inst : Add G] → {a : G} → Mul (AddConstEquiv G G a a)
-- Mathlib.CategoryTheory.Monoidal.Opposite
CategoryTheory.MonoidalOpposite.monoidalOppositeCategory : {C : Type u₁} → [CategoryTheory.Category.{v₁, u₁} C] → CategoryTheory.Category.{v₁, u₁} Cᴹᵒᵖ
-- Mathlib.Topology.Semicontinuity.Defs
upperHemicontinuousOn_iff : ∀ {α : Type u_1} {β : Type u_2} [inst : TopologicalSpace α] [inst_1 : TopologicalSpace β] {f : α → Set β} {s : Set α},
  UpperHemicontinuousOn f s ↔ ∀ x ∈ s, UpperHemicontinuousWithinAt f s x
-- Aesop.RuleSet
Aesop.instInhabitedGlobalRuleSet : Inhabited Aesop.GlobalRuleSet
-- Mathlib.Order.Concept
Concept.compl_intent : ∀ {α : Type u_2} {r' : α → α → Prop} [IsStrictTotalOrder α r'] (c' : Concept α α r'), c'.intentᶜ = c'.extent
-- Mathlib.GroupTheory.ResiduallyFinite
AddGroup.residuallyFinite_iff_forall_finiteIndexNormalAddSubgroup : ∀ {G : Type u_1} [inst : AddGroup G],
  AddGroup.ResiduallyFinite G ↔ ∀ (g : G), (∀ (H : FiniteIndexNormalAddSubgroup G), g ∈ H) → g = 0
-- Mathlib.Logic.Encodable.Basic
Encodable.decode₂_ne_none_iff : ∀ {α : Type u_1} [inst : Encodable α] {n : ℕ}, Encodable.decode₂ α n ≠ none ↔ n ∈ Set.range Encodable.encode
-- Lean.Meta.ArgsPacker.Basic
Lean.Meta.instInhabitedArgsPacker.default : Lean.Meta.ArgsPacker
-- Mathlib.GroupTheory.Congruence.Opposite
Con.orderIsoOp.eq_1 : ∀ {M : Type u_1} [inst : Mul M],
  Con.orderIsoOp = { toFun := Con.op, invFun := Con.unop, left_inv := ⋯, right_inv := ⋯, map_rel_iff' := ⋯ }
-- Std.Data.DHashMap.Internal.RawLemmas
Std.DHashMap.Internal.Raw₀.insertMany_list_equiv_congr : ∀ {α : Type u} {β : α → Type v} [inst : BEq α] [inst_1 : Hashable α] (m₁ m₂ : Std.DHashMap.Internal.Raw₀ α β)
  [EquivBEq α] [LawfulHashable α],
  (↑m₁).WF → (↑m₂).WF → (↑m₁).Equiv ↑m₂ → ∀ {l : List ((a : α) × β a)}, (↑↑(m₁.insertMany l)).Equiv ↑↑(m₂.insertMany l)
-- Mathlib.Tactic.Linter.DirectoryDependency
/-- The `directoryDependency` linter detects imports between directories that are supposed to be
independent. If this is the case, it emits a warning.
 -/
Mathlib.Linter.directoryDependencyCheck : Lean.Name → Lean.Elab.Command.CommandElabM (Array Lean.MessageData)
-- Std.Data.ExtTreeMap.Lemmas
Std.ExtTreeMap.contains_diff : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t₁ t₂ : Std.ExtTreeMap α β cmp} [inst : Std.TransCmp cmp] {k : α},
  (t₁ \ t₂).contains k = (t₁.contains k && !t₂.contains k)
-- Mathlib.Order.SupClosed
InfClosed.iInf_mem_of_nonempty : ∀ {ι : Sort u_1} {α : Type u_3} [inst : ConditionallyCompleteLattice α] {f : ι → α} {s : Set α} [Finite ι] [Nonempty ι],
  InfClosed s → (∀ (i : ι), f i ∈ s) → ⨅ i, f i ∈ s
-- Mathlib.Data.Prod.Lex
Prod.Lex.boundedOrder : {α : Type u_1} →
  {β : Type u_2} →
    [inst : PartialOrder α] → [inst_1 : Preorder β] → [BoundedOrder α] → [BoundedOrder β] → BoundedOrder (Lex (α × β))
-- Mathlib.Control.Fold
Monoid.foldrM.ofFreeMonoid.eq_1 : ∀ {m : Type u → Type u} [inst : Monad m] {α β : Type u} [inst_1 : LawfulMonad m] (f : α → β → m β),
  Monoid.foldrM.ofFreeMonoid f =
    { toFun := fun xs => flip (List.foldrM f) (FreeMonoid.toList xs), map_one' := ⋯, map_mul' := ⋯ }
-- Mathlib.Analysis.Normed.Group.Basic
ne_one_of_mem_sphere : ∀ {E : Type u_5} [inst : SeminormedGroup E] {r : ℝ}, r ≠ 0 → ∀ (x : ↑(Metric.sphere 1 r)), ↑x ≠ 1