mathlib-initiative/mathlib-types huggingface dataset:
-- Batteries.Data.AssocList
Batteries.AssocList.cons.injEq : ∀ {α : Type u} {β : Type v} (key : α) (value : β) (tail : Batteries.AssocList α β) (key_1 : α) (value_1 : β)
  (tail_1 : Batteries.AssocList α β),
  (Batteries.AssocList.cons key value tail = Batteries.AssocList.cons key_1 value_1 tail_1) =
    (key = key_1 ∧ value = value_1 ∧ tail = tail_1)
-- Mathlib.CategoryTheory.Functor.KanExtension.Basic
CategoryTheory.Functor.isRightKanExtensionAlongEquivalence' : ∀ {C : Type u_1} {H : Type u_3} {D : Type u_4} [inst : CategoryTheory.Category.{v_1, u_1} C]
  [inst_1 : CategoryTheory.Category.{v_3, u_3} H] [inst_2 : CategoryTheory.Category.{v_4, u_4} D]
  {F₀ : CategoryTheory.Functor C H} {F₁ : CategoryTheory.Functor D H} (L : CategoryTheory.Functor C D)
  (α : L.comp F₁ ⟶ F₀) [L.IsEquivalence] [CategoryTheory.IsIso α], F₁.IsRightKanExtension α
-- Mathlib.Geometry.Manifold.Algebra.LieGroup
ContMDiffOn.inv₀ : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {n : WithTop ℕ∞} {H : Type u_2} [inst_1 : TopologicalSpace H]
  {E : Type u_3} [inst_2 : NormedAddCommGroup E] [inst_3 : NormedSpace 𝕜 E] {I : ModelWithCorners 𝕜 E H} {G : Type u_4}
  [inst_4 : TopologicalSpace G] [inst_5 : ChartedSpace H G] [inst_6 : Inv G] [inst_7 : Zero G] {E' : Type u_5}
  [inst_8 : NormedAddCommGroup E'] [inst_9 : NormedSpace 𝕜 E'] {H' : Type u_6} [inst_10 : TopologicalSpace H']
  {I' : ModelWithCorners 𝕜 E' H'} {M : Type u_7} [inst_11 : TopologicalSpace M] [inst_12 : ChartedSpace H' M]
  {f : M → G} [ContMDiffInv₀ I n G] {s : Set M},
  ContMDiffOn I' I n f s → (∀ x ∈ s, f x ≠ 0) → ContMDiffOn I' I n (fun x => (f x)⁻¹) s
-- Mathlib.Logic.Equiv.Defs
/-- A `PSigma` with `Prop` fibers is equivalent to the subtype.  -/
Equiv.psigmaEquivSubtype : {α : Type v} → (P : α → Prop) → (i : α) ×' P i ≃ Subtype P
-- Mathlib.CategoryTheory.Functor.Currying
/-- Natural isomorphism witnessing `comp_flip_uncurry_eq`.  -/
CategoryTheory.Functor.compFlipUncurryIso : {B : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} B] →
    {C : Type u₂} →
      [inst_1 : CategoryTheory.Category.{v₂, u₂} C] →
        {D : Type u₃} →
          [inst_2 : CategoryTheory.Category.{v₃, u₃} D] →
            {E : Type u₄} →
              [inst_3 : CategoryTheory.Category.{v₄, u₄} E] →
                (F : CategoryTheory.Functor B D) →
                  (G : CategoryTheory.Functor D (CategoryTheory.Functor C E)) →
                    CategoryTheory.Functor.uncurry.obj (F.comp G).flip ≅
                      ((CategoryTheory.Functor.id C).prod F).comp (CategoryTheory.Functor.uncurry.obj G.flip)
-- Init.Grind.Ordered.Linarith
Lean.Grind.Linarith.instBEqExpr : BEq Lean.Grind.Linarith.Expr
-- Init.Data.UInt.Lemmas
UInt64.toUSize_ofNat : ∀ {n : ℕ}, (OfNat.ofNat n).toUSize = OfNat.ofNat n
-- Mathlib.Algebra.Polynomial.Cardinal
Polynomial.cardinalMk_eq_max : ∀ {R : Type u} [inst : Semiring R] [Nontrivial R], Cardinal.mk (Polynomial R) = max (Cardinal.mk R) Cardinal.aleph0
-- Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic
Real.sin_pos_of_mem_Ioo : ∀ {x : ℝ}, x ∈ Set.Ioo 0 Real.pi → 0 < Real.sin x
-- Mathlib.CategoryTheory.Monad.Algebra
CategoryTheory.Comonad.forget_obj : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] (G : CategoryTheory.Comonad C) (A : G.Coalgebra),
  G.forget.obj A = A.A
-- Std.Data.ExtDTreeMap.Lemmas
Std.ExtDTreeMap.Const.toList_filter : ∀ {α : Type u} {cmp : α → α → Ordering} {β : Type v} {t : Std.ExtDTreeMap α (fun x => β) cmp} [inst : Std.TransCmp cmp]
  {f : α → β → Bool},
  Std.ExtDTreeMap.Const.toList (Std.ExtDTreeMap.filter f t) =
    List.filter (fun p => f p.1 p.2) (Std.ExtDTreeMap.Const.toList t)
-- Std.Data.HashSet.RawLemmas
Std.HashSet.Raw.equiv_emptyWithCapacity_iff_isEmpty : ∀ {α : Type u} {m : Std.HashSet.Raw α} [inst : BEq α] [inst_1 : Hashable α] [EquivBEq α] [LawfulHashable α] {c : ℕ},
  m.WF → (m.Equiv (Std.HashSet.Raw.emptyWithCapacity c) ↔ m.isEmpty = true)
-- Mathlib.SetTheory.Cardinal.Regular
Cardinal.lsub_lt_ord_of_isRegular : ∀ {ι : Type (max u_1 u_2)} {f : ι → Ordinal.{max u_1 u_2}} {c : Cardinal.{max u_1 u_2}},
  c.IsRegular → Cardinal.mk ι < c → (∀ (i : ι), f i < c.ord) → Ordinal.lsub f < c.ord
-- Mathlib.Combinatorics.Nullstellensatz
/-- The **Combinatorial Nullstellensatz**.

Given a multi-index `t : σ →₀ ℕ` such that `t s < (S s).card` for all `s`,
`f.totalDegree = t.degree` and `f.coeff t ≠ 0`,
there exists a point `x : σ → R` such that `x s ∈ S s` for all `s` and `f.eval s ≠ 0`.

[Alon_1999], theorem 2  -/
MvPolynomial.combinatorial_nullstellensatz_exists_eval_nonzero : ∀ {R : Type u_1} [inst : CommRing R] {σ : Type u_2} [Finite σ] [IsDomain R] (f : MvPolynomial σ R) (t : σ →₀ ℕ),
  MvPolynomial.coeff t f ≠ 0 →
    f.totalDegree = Finsupp.degree t →
      ∀ (S : σ → Finset R), (∀ (i : σ), t i < (S i).card) → ∃ s, (∀ (i : σ), s i ∈ S i) ∧ (MvPolynomial.eval s) f ≠ 0
-- Mathlib.LinearAlgebra.TensorProduct.Map
TensorProduct.homTensorHomMap_apply : ∀ {R : Type u_1} {R₂ : Type u_2} [inst : CommSemiring R] [inst_1 : CommSemiring R₂] {σ₁₂ : R →+* R₂} {M : Type u_7}
  {N : Type u_8} {M₂ : Type u_12} {N₂ : Type u_14} [inst_2 : AddCommMonoid M] [inst_3 : AddCommMonoid N]
  [inst_4 : AddCommMonoid M₂] [inst_5 : AddCommMonoid N₂] [inst_6 : Module R M] [inst_7 : Module R N]
  [inst_8 : Module R₂ M₂] [inst_9 : Module R₂ N₂] (f : M →ₛₗ[σ₁₂] M₂) (g : N →ₛₗ[σ₁₂] N₂),
  (TensorProduct.homTensorHomMap σ₁₂ M N M₂ N₂) (f ⊗ₜ[R₂] g) = TensorProduct.map f g
-- Mathlib.RingTheory.Valuation.Basic
/-- This theorem is a weaker version of `Valuation.val_le_one_or_val_inv_lt_one`, but more symmetric
in `x` and `x⁻¹`.
 -/
Valuation.val_le_one_or_val_inv_le_one : ∀ {K : Type u_1} [inst : DivisionRing K] {Γ₀ : Type u_4} [inst_1 : LinearOrderedCommGroupWithZero Γ₀]
  (v : Valuation K Γ₀) (x : K), v x ≤ 1 ∨ v x⁻¹ ≤ 1
-- Mathlib.Algebra.Ring.Hom.Defs
NonUnitalRingHom.coe_toMulHom : ∀ {α : Type u_2} {β : Type u_3} [inst : NonUnitalNonAssocSemiring α] [inst_1 : NonUnitalNonAssocSemiring β]
  (f : α →ₙ+* β), ⇑f.toMulHom = ⇑f
-- Mathlib.Data.Seq.Basic
Stream'.Seq.Pairwise_cons_cons_head : ∀ {α : Type u} {R : α → α → Prop} {hd tl_hd : α} {tl_tl : Stream'.Seq α},
  Stream'.Seq.Pairwise R (Stream'.Seq.cons hd (Stream'.Seq.cons tl_hd tl_tl)) → R hd tl_hd
-- Mathlib.CategoryTheory.Limits.Shapes.Pullback.Categorical.CatCospanTransform
CategoryTheory.Limits.CatCospanTransformMorphism.right_coherence_app : ∀ {A : Type u₁} {B : Type u₂} {C : Type u₃} {A' : Type u₄} {B' : Type u₅} {C' : Type u₆}
  [inst : CategoryTheory.Category.{v₁, u₁} A] [inst_1 : CategoryTheory.Category.{v₂, u₂} B]
  [inst_2 : CategoryTheory.Category.{v₃, u₃} C] {F : CategoryTheory.Functor A B} {G : CategoryTheory.Functor C B}
  [inst_3 : CategoryTheory.Category.{v₄, u₄} A'] [inst_4 : CategoryTheory.Category.{v₅, u₅} B']
  [inst_5 : CategoryTheory.Category.{v₆, u₆} C'] {F' : CategoryTheory.Functor A' B'} {G' : CategoryTheory.Functor C' B'}
  {ψ ψ' : CategoryTheory.Limits.CatCospanTransform F G F' G'} (α : ψ ⟶ ψ') (x : C),
  CategoryTheory.CategoryStruct.comp ((CategoryTheory.CatCommSq.iso G ψ.right ψ.base G').hom.app x)
      (G'.map (α.right.app x)) =
    CategoryTheory.CategoryStruct.comp (α.base.app (G.obj x))
      ((CategoryTheory.CatCommSq.iso G ψ'.right ψ'.base G').hom.app x)
-- Mathlib.Data.Matrix.Basis
Matrix.sum_single_one : ∀ {m : Type u_2} {α : Type u_7} [inst : DecidableEq m] [inst_1 : AddCommMonoid α] [inst_2 : One α] [inst_3 : Fintype m],
  ∑ i, Matrix.single i i 1 = 1
-- Mathlib.LinearAlgebra.Transvection.Generation
_private.Mathlib.LinearAlgebra.Transvection.Generation.0.LinearEquiv.finrank_mod_auxTransvection_mul_fixed : ∀ {K : Type u_1} [inst : DivisionRing K] {V : Type u_2} [inst_1 : AddCommGroup V] [inst_2 : Module K V]
  [Module.Finite K V] {e : V ≃ₗ[K] V} {f : Module.Dual K V} {u : V}
  {hf : (↑e).fixedSubmodule ⊔ K ∙ (e u - u) ≤ LinearMap.ker f},
  f u = 1 →
    u ∉ (↑e).fixedSubmodule →
      Module.finrank K (V ⧸ (↑(LinearEquiv.auxTransvection✝ hf * e)).fixedSubmodule) + 1 =
        Module.finrank K (V ⧸ (↑e).fixedSubmodule)
-- Mathlib.MeasureTheory.Function.LpSpace.Basic
MeasureTheory.Lp.eLpNorm_lt_top : ∀ {α : Type u_1} {E : Type u_4} {m : MeasurableSpace α} {p : ENNReal} {μ : MeasureTheory.Measure α}
  [inst : NormedAddCommGroup E] (f : ↥(MeasureTheory.Lp E p μ)), MeasureTheory.eLpNorm (↑↑f) p μ < ⊤
-- Mathlib.CategoryTheory.Limits.Preserves.Creates.Pullbacks
CategoryTheory.Limits.HasPushout.of_createsColimit : ∀ {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] (F : CategoryTheory.Functor C D) {X Y S : C} (f : S ⟶ X) (g : S ⟶ Y)
  [CategoryTheory.CreatesColimit (CategoryTheory.Limits.span f g) F]
  [CategoryTheory.Limits.HasPushout (F.map f) (F.map g)], CategoryTheory.Limits.HasPushout f g
-- Mathlib.Algebra.Category.Grp.Basic
/-- The type of morphisms in `AddCommGrpCat R`.  -/
AddCommGrpCat.Hom : AddCommGrpCat → AddCommGrpCat → Type u
-- Mathlib.Topology.Compactness.CompactSystem
/-- The set of compact and closed sets is a compact system.  -/
isCompactSystem_isCompact_isClosed : ∀ (α : Type u_2) [inst : TopologicalSpace α], IsCompactSystem {s | IsCompact s ∧ IsClosed s}
-- Std.Data.DHashMap.RawLemmas
Std.DHashMap.Raw.getKey!_ofList_of_contains_eq_false : ∀ {α : Type u} {β : α → Type v} [inst : BEq α] [inst_1 : Hashable α] [EquivBEq α] [LawfulHashable α]
  [inst_4 : Inhabited α] {l : List ((a : α) × β a)} {k : α},
  (List.map Sigma.fst l).contains k = false → (Std.DHashMap.Raw.ofList l).getKey! k = default
-- Mathlib.Data.FP.Basic
FP.nextDn : [C : FP.FloatCfg] → FP.Float → FP.Float
-- Mathlib.Algebra.Algebra.Subalgebra.Basic
Subalgebra.instCommSemiringSubtypeMemCenter : {R : Type u} →
  {A : Type v} →
    [inst : CommSemiring R] → [inst_1 : Semiring A] → [inst_2 : Algebra R A] → CommSemiring ↥(Subalgebra.center R A)
-- Mathlib.GroupTheory.Complement
AddSubgroup.IsComplement.leftQuotientEquiv_apply : ∀ {G : Type u_1} [inst : AddGroup G] {H : AddSubgroup G} {f : G ⧸ H → G} (hf : ∀ (q : G ⧸ H), ↑(f q) = q) (q : G ⧸ H),
  ↑(⋯.leftQuotientEquiv q) = f q
-- Mathlib.Data.Multiset.Basic
Multiset.coe_toList : ∀ {α : Type u_1} (s : Multiset α), ↑s.toList = s
-- Mathlib.Algebra.DirectSum.Decomposition
DirectSum.decompose_symm_add : ∀ {ι : Type u_1} {M : Type u_3} {σ : Type u_4} [inst : DecidableEq ι] [inst_1 : AddCommMonoid M] [inst_2 : SetLike σ M]
  [inst_3 : AddSubmonoidClass σ M] (ℳ : ι → σ) [inst_4 : DirectSum.Decomposition ℳ] (x y : DirectSum ι fun i => ↥(ℳ i)),
  (DirectSum.decompose ℳ).symm (x + y) = (DirectSum.decompose ℳ).symm x + (DirectSum.decompose ℳ).symm y
-- Mathlib.Data.Int.Init
Int.inductionOn'.pos.match_1.congr_eq_1 : ∀ (motive : ℕ → Sort u_1) (x : ℕ) (h_1 : Unit → motive 0) (h_2 : (n : ℕ) → motive n.succ),
  x = 0 →
    (match x with
      | 0 => h_1 ()
      | n.succ => h_2 n) ≍
      h_1 ()
-- Mathlib.GroupTheory.PGroup
/-- If a p-group acts on `α` and the cardinality of `α` is not a multiple
of `p` then the action has a fixed point.  -/
IsPGroup.nonempty_fixed_point_of_prime_not_dvd_card : ∀ {p : ℕ} {G : Type u_1} [inst : Group G],
  IsPGroup p G →
    ∀ [hp : Fact (Nat.Prime p)] (α : Type u_3) [inst_1 : MulAction G α],
      ¬p ∣ Nat.card α → (MulAction.fixedPoints G α).Nonempty
-- Lean.Elab.Tactic.Doc
/-- Computes a table that heuristically maps parser syntax kinds to their first tokens by inspecting the
Pratt parsing tables for the `tactic syntax kind. If a custom name is provided for the tactic, then
it is returned instead.
 -/
Lean.Elab.Tactic.Doc.firstTacticTokens : {m : Type → Type} → [Monad m] → [Lean.MonadEnv m] → m (Lean.NameMap String)
-- Mathlib.Algebra.Group.Action.Pointwise.Set.Basic
Set.vadd_inter_nonempty_iff : ∀ {α : Type u_2} [inst : AddGroup α] {s t : Set α} {x : α},
  ((x +ᵥ s) ∩ t).Nonempty ↔ ∃ a b, (a ∈ t ∧ b ∈ s) ∧ a + -b = x
-- Mathlib.RingTheory.PicardGroup
/-- An invertible module is free iff it is isomorphic to the ring, i.e. its class is trivial in
the Picard group.  -/
Module.Invertible.free_iff_linearEquiv : ∀ {R : Type u} {M : Type v} [inst : CommSemiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M]
  [Module.Invertible R M], Module.Free R M ↔ Nonempty (M ≃ₗ[R] R)
-- Mathlib.RingTheory.Bialgebra.MonoidAlgebra
MonoidAlgebra.liftGroupLikeBialgHom_apply : ∀ {R : Type u_1} {A : Type u_3} [inst : CommSemiring R] [inst_1 : Semiring A] [inst_2 : Bialgebra R A]
  (a : MonoidAlgebra R (GroupLike R A)),
  MonoidAlgebra.liftGroupLikeBialgHom a =
    ((MonoidAlgebra.lift R A (GroupLike R A)) { toFun := fun g => ↑g, map_one' := ⋯, map_mul' := ⋯ }) a
-- Lean.Meta.Tactic.Simp.BuiltinSimprocs.Fin
_private.Lean.Meta.Tactic.Simp.BuiltinSimprocs.Fin.0.Fin.instReprValue.repr : Fin.Value✝ → ℕ → Std.Format
-- Mathlib.LinearAlgebra.Matrix.NonsingularInverse
Matrix.mul_inv_rev : ∀ {n : Type u'} {α : Type v} [inst : Fintype n] [inst_1 : DecidableEq n] [inst_2 : CommRing α] (A B : Matrix n n α),
  (A * B)⁻¹ = B⁻¹ * A⁻¹
-- Mathlib.Algebra.Category.Ring.Basic
SemiRingCat.Hom.ext : ∀ {R S : SemiRingCat} {x y : R.Hom S}, x.hom' = y.hom' → x = y
-- Mathlib.Analysis.Distribution.ContDiffMapSupportedIn
/-- `fderivCLM 𝕜 n k` is the continuous `𝕜`-linear-map sending `f : 𝓓^{n}_{K}(E, F)` to
its derivative as an element of `𝓓^{k}_{K}(E, E →L[ℝ] F)`.
This only makes mathematical sense if `k + 1 ≤ n`, otherwise we define it as the zero map.  -/
ContDiffMapSupportedIn.fderivCLM : (𝕜 : Type u_1) →
  {E : Type u_2} →
    {F : Type u_3} →
      [inst : NontriviallyNormedField 𝕜] →
        [inst_1 : NormedAddCommGroup E] →
          [inst_2 : NormedSpace ℝ E] →
            [inst_3 : NormedAddCommGroup F] →
              [inst_4 : NormedSpace ℝ F] →
                [inst_5 : NormedSpace 𝕜 F] →
                  [inst_6 : SMulCommClass ℝ 𝕜 F] →
                    (n k : ℕ∞) →
                      {K : TopologicalSpace.Compacts E} →
                        ContDiffMapSupportedIn E F n K →L[𝕜] ContDiffMapSupportedIn E (E →L[ℝ] F) k K
-- Mathlib.Analysis.Complex.Asymptotics
Complex.isLittleO_ofReal_left : ∀ {α : Type u_1} {E : Type u_2} [inst : Norm E] {l : Filter α} {f : α → ℝ} {g : α → E},
  (fun x => ↑(f x)) =o[l] g ↔ f =o[l] g
-- Mathlib.Algebra.Group.UniqueProds.Basic
/-- `UniqueSums` is preserved under additive equivalences.  -/
AddEquiv.uniqueSums_iff : ∀ {G : Type u} {H : Type v} [inst : Add G] [inst_1 : Add H] (f : G ≃+ H), UniqueSums G ↔ UniqueSums H
-- Mathlib.Algebra.Homology.SpectralObject.Cycles
CategoryTheory.Abelian.SpectralObject.p_descOpcycles_assoc : ∀ {C : Type u_1} {ι : Type u_2} [inst : CategoryTheory.Category.{v_1, u_1} C]
  [inst_1 : CategoryTheory.Category.{v_2, u_2} ι] [inst_2 : CategoryTheory.Abelian C]
  (X : CategoryTheory.Abelian.SpectralObject C ι) {i j k : ι} (f : i ⟶ j) (g : j ⟶ k) (n₀ n₁ : ℤ) (hn₁ : n₀ + 1 = n₁)
  {A : C} (x : (X.H n₁).obj (CategoryTheory.ComposableArrows.mk₁ f) ⟶ A)
  (hx : CategoryTheory.CategoryStruct.comp (X.δ f g n₀ n₁ hn₁) x = 0) {Z : C} (h : A ⟶ Z),
  CategoryTheory.CategoryStruct.comp (X.pOpcycles f g n₁)
      (CategoryTheory.CategoryStruct.comp (X.descOpcycles f g n₀ n₁ hn₁ x hx) h) =
    CategoryTheory.CategoryStruct.comp x h
-- Aesop.Stats.Basic
Aesop.ForwardRuleStateStats.ruleName : Aesop.ForwardRuleStateStats → Aesop.RuleName
-- Mathlib.Topology.CompactOpen
ContinuousMap.continuousOn_of_continuousOn_uncurry : ∀ {X : Type u_2} {Y : Type u_3} {Z : Type u_4} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y]
  [inst_2 : TopologicalSpace Z] {s : Set X} (f : X → C(Y, Z)),
  ContinuousOn (Function.uncurry fun x y => (f x) y) (s ×ˢ Set.univ) → ContinuousOn f s
-- Mathlib.Algebra.Group.Units.Defs
/-- Units of a `Monoid`, bundled version. Notation: `αˣ`.

An element of a `Monoid` is a unit if it has a two-sided inverse.
This version bundles the inverse element so that it can be computed.
For a predicate see `IsUnit`.  -/
Units : (α : Type u) → [Monoid α] → Type u
-- Mathlib.Algebra.Group.Translate
translate_zero : ∀ {α : Type u_2} {G : Type u_5} [inst : AddCommGroup G] (f : G → α), translate 0 f = f
-- Mathlib.CategoryTheory.Bicategory.FunctorBicategory.Oplax
CategoryTheory.Oplax.LaxTrans.associator_inv_as_app : ∀ {B : Type u₁} [inst : CategoryTheory.Bicategory B] {C : Type u₂} [inst_1 : CategoryTheory.Bicategory C]
  {F G H I : CategoryTheory.OplaxFunctor B C} (η : F ⟶ G) (θ : G ⟶ H) (ι : H ⟶ I) (a : B),
  (CategoryTheory.Oplax.LaxTrans.associator η θ ι).inv.as.app a =
    (CategoryTheory.Bicategory.associator (η.app a) (θ.app a) (ι.app a)).inv
-- Mathlib.Analysis.Distribution.TestFunction
/-- **Alias** of `FunLike.coe_add`. -/
TestFunction.coe_add : ∀ {F : Type u_3} {α : Type u_5} {β : Type u_6} [inst : FunLike F α β] [inst_1 : Add F] [inst_2 : Add β]
  [IsAddApply F α β] (f g : F), ⇑(f + g) = ⇑f + ⇑g
-- Mathlib.RingTheory.PowerSeries.Derivative
PowerSeries.derivative.eq_1 : ∀ (R : Type u_1) [inst : CommSemiring R], PowerSeries.derivative R = MvPowerSeries.pderiv R ()
-- Mathlib.Order.GameAdd
/-- Recursion on the well-founded `Prod.GameAdd` relation.
Note that it's strictly more general to recurse on the lexicographic order instead.  -/
Prod.GameAdd.recursion : {α : Type u_1} →
  {β : Type u_2} →
    {rα : α → α → Prop} →
      {rβ : β → β → Prop} →
        {C : α → β → Sort u_3} →
          WellFounded rα →
            WellFounded rβ →
              ((a₁ : α) → (b₁ : β) → ((a₂ : α) → (b₂ : β) → Prod.GameAdd rα rβ (a₂, b₂) (a₁, b₁) → C a₂ b₂) → C a₁ b₁) →
                (a : α) → (b : β) → C a b
-- Mathlib.Algebra.Group.Semiconj.Defs
/-- **Alias** of `SemiconjBy.refl`.

---

The relation “there exists an element that semiconjugates `a` to `b`” on a monoid (or, more
generally, on `MulOneClass` type) is reflexive.  -/
SemiconjBy.reflexive : ∀ {M : Type u_2} [inst : MulOneClass M], Std.Refl fun a b => ∃ c, SemiconjBy c a b
-- Mathlib.Order.CompleteLatticeIntervals
Set.Iic.coe_iSup : ∀ {ι : Sort u_1} {α : Type u_2} [inst : CompleteLattice α] {a : α} (f : ι → ↑(Set.Iic a)), ↑(⨆ i, f i) = ⨆ i, ↑(f i)
-- Mathlib.CategoryTheory.Monoidal.Closed.FunctorCategory.Basic
CategoryTheory.MonoidalClosed.FunctorCategory.homEquiv_naturality_three : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.MonoidalCategory C]
  [inst_2 : CategoryTheory.MonoidalClosed C] {J : Type u₂} [inst_3 : CategoryTheory.Category.{v₂, u₂} J]
  [inst_4 :
    ∀ (F₁ F₂ : CategoryTheory.Functor J C), CategoryTheory.Enriched.FunctorCategory.HasFunctorEnrichedHom C F₁ F₂]
  {F₁ F₂ F₃ F₃' : CategoryTheory.Functor J C}
  [inst_5 : ∀ (F₁ F₂ : CategoryTheory.Functor J C), CategoryTheory.Enriched.FunctorCategory.HasEnrichedHom C F₁ F₂]
  (f : CategoryTheory.MonoidalCategoryStruct.tensorObj F₁ F₂ ⟶ F₃) (f₃ : F₃ ⟶ F₃'),
  CategoryTheory.MonoidalClosed.FunctorCategory.homEquiv (CategoryTheory.CategoryStruct.comp f f₃) =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalClosed.FunctorCategory.homEquiv f)
      (CategoryTheory.CategoryStruct.comp
        (CategoryTheory.MonoidalCategoryStruct.rightUnitor
            (CategoryTheory.Enriched.FunctorCategory.functorEnrichedHom C F₁ F₃)).inv
        (CategoryTheory.CategoryStruct.comp
          (CategoryTheory.MonoidalCategoryStruct.whiskerLeft
            (CategoryTheory.Enriched.FunctorCategory.functorEnrichedHom C F₁ F₃)
            ((CategoryTheory.Enriched.FunctorCategory.functorHomEquiv C) f₃))
          (CategoryTheory.Enriched.FunctorCategory.functorEnrichedComp C F₁ F₃ F₃')))
-- Mathlib.Algebra.Category.ModuleCat.ChangeOfRings
ModuleCat.extendScalarsId_inv_app_apply : ∀ {R : Type u₁} [inst : CommRing R] (M : ModuleCat R) (m : ↑M),
  (CategoryTheory.ConcreteCategory.hom ((ModuleCat.extendScalarsId R).inv.app M)) m = 1 ⊗ₜ[R] m
-- Mathlib.Topology.Algebra.Module.Equiv
/-- The natural equivalence `N × M ≃L[R] M` for any `Unique` type `N`.
This is `Equiv.uniqueProd` as a continuous linear equivalence.  -/
ContinuousLinearEquiv.uniqueProd : (R : Type u_8) →
  (M : Type u_9) →
    (N : Type u_10) →
      [inst : Semiring R] →
        [inst_1 : TopologicalSpace M] →
          [inst_2 : AddCommMonoid M] →
            [inst_3 : TopologicalSpace N] →
              [inst_4 : AddCommMonoid N] → [Unique N] → [inst_6 : Module R M] → [inst_7 : Module R N] → (N × M) ≃L[R] M
-- Aesop.Forward.State
Aesop.ClusterState.mk : (slots : Array Aesop.Slot) →
  Array Aesop.PremiseIndex →
    Aesop.VariableMap →
      Lean.PHashSet Aesop.Match →
        Bool → (slotQueues : Array (Array Aesop.RawHyp)) → slotQueues.size = slots.size → Aesop.ClusterState
-- Mathlib.Algebra.Order.GroupWithZero.Defs
/-- **Alias** of `mul_lt_mul_of_le_of_lt_of_nonneg_of_pos`. -/
mul_lt_mul_of_nonneg_of_pos' : ∀ {α : Type u_1} [inst : Mul α] [inst_1 : Zero α] [inst_2 : Preorder α] {a b c d : α} [PosMulStrictMono α]
  [MulPosMono α], a ≤ b → c < d → 0 ≤ c → 0 < b → a * c < b * d
-- Plausible.Random
/-- Given a random generator for `ULift α`, we can convert it to a random generator for `α`.  -/
Plausible.RandT.down : {α : Type u} →
  {m : Type (max u v) → Type w} →
    {m' : Type u → Type w'} →
      {g : Type} →
        [RandomGen g] →
          [Monad m] →
            [Monad m'] →
              ({α : Type u} → m (ULift.{v, u} α) → m' α) →
                Plausible.RandGT g m (ULift.{v, u} α) → Plausible.RandGT g m' α
-- Mathlib.Data.Fin.VecNotation
/-- `vecAlt0 v` gives a vector with half the length of `v`, with
only alternate elements (even-numbered).  -/
Matrix.vecAlt0 : {α : Type u} → {m n : ℕ} → m = n + n → (Fin m → α) → Fin n → α
-- Mathlib.Data.PNat.Basic
instAddLeftMonoPNat : AddLeftMono ℕ+
-- Mathlib.RingTheory.Valuation.ValuativeRel.Basic
/-- **Alias** of the reverse direction of `ValuativeRel.not_vlt`. -/
ValuativeRel.vle.not_vlt : ∀ {R : Type u_1} [inst : Semiring R] [inst_1 : ValuativeRel R] {x y : R}, y ≤ᵥ x → ¬x <ᵥ y
-- Mathlib.AlgebraicGeometry.Properties
AlgebraicGeometry.isIntegral_iff_irreducibleSpace_and_isReduced : ∀ (X : AlgebraicGeometry.Scheme), AlgebraicGeometry.IsIntegral X ↔ IrreducibleSpace ↥X ∧ AlgebraicGeometry.IsReduced X
-- Std.Tactic.BVDecide.Syntax
/-- Canonicalize with respect to associativity and commutativity.
 -/
Lean.Elab.Tactic.BVDecide.BVDecideConfig.acNf : Lean.Elab.Tactic.BVDecide.BVDecideConfig → Bool
-- Std.Data.Internal.List.Associative
Std.Internal.List.getValueCast_eq_getValueCastD : ∀ {α : Type u} {β : α → Type v} [inst : BEq α] [inst_1 : LawfulBEq α] {l : List ((a : α) × β a)} {a : α}
  {fallback : β a} (h : Std.Internal.List.containsKey a l = true),
  Std.Internal.List.getValueCast a l h = Std.Internal.List.getValueCastD a l fallback
-- Mathlib.Geometry.Manifold.LocalDiffeomorph
/-- A local diffeomorphism at `x` is differentiable at `x`.  -/
IsLocalDiffeomorphAt.mdifferentiableAt : ∀ {𝕜 : 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] {H₁ : Type u_5}
  [inst_5 : TopologicalSpace H₁] {H₂ : Type u_6} [inst_6 : TopologicalSpace H₂] {I : ModelWithCorners 𝕜 E H₁}
  {J : ModelWithCorners 𝕜 F H₂} {M : Type u_8} [inst_7 : TopologicalSpace M] [inst_8 : ChartedSpace H₁ M] {N : Type u_9}
  [inst_9 : TopologicalSpace N] [inst_10 : ChartedSpace H₂ N] {n : WithTop ℕ∞} {f : M → N} {x : M},
  IsLocalDiffeomorphAt I J n f x → n ≠ 0 → MDiffAt f x
-- Mathlib.Algebra.Order.Monoid.Units
Units.instMaxOfLinearOrder.eq_1 : ∀ {α : Type u_1} [inst : Monoid α] [inst_1 : LinearOrder α],
  Units.instMaxOfLinearOrder = { max := fun a b => if a ≤ b then b else a }