mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.CategoryTheory.Monoidal.Cartesian.Over
CategoryTheory.Over.associator_inv_left_fst_fst : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Limits.HasPullbacks C] {X : C}
  (R S T : CategoryTheory.Over X),
  CategoryTheory.CategoryStruct.comp
      (CategoryTheory.Over.Hom.left (CategoryTheory.MonoidalCategoryStruct.associator R S T).inv)
      (CategoryTheory.CategoryStruct.comp
        (CategoryTheory.Limits.pullback.fst
          (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pullback.fst R.hom S.hom) R.hom) T.hom)
        (CategoryTheory.Limits.pullback.fst R.hom S.hom)) =
    CategoryTheory.Limits.pullback.fst R.hom (CategoryTheory.MonoidalCategoryStruct.tensorObj S T).hom
-- Mathlib.Dynamics.Transitive
/-- An action of an additive monoid `M` on `α` is topologically transitive if and only
if for any nonempty open subset `U` of `α` the union over the elements of `M` of images of `U` is
dense in `α`.  -/
AddAction.isTopologicallyTransitive_iff_dense_iUnion : ∀ (M : Type u_1) {α : Type u_2} [inst : TopologicalSpace α] [inst_1 : AddMonoid M] [inst_2 : AddAction M α],
  AddAction.IsTopologicallyTransitive M α ↔ ∀ {U : Set α}, IsOpen U → U.Nonempty → Dense (⋃ m, m +ᵥ U)
-- Mathlib.Topology.Order.NhdsSet
Ioc_mem_nhdsSet_Ico : ∀ {α : Type u_1} [inst : LinearOrder α] [inst_1 : TopologicalSpace α] [OrderClosedTopology α] {a b c d : α},
  a < b → c ≤ d → Set.Ioc a d ∈ nhdsSet (Set.Ico b c)
-- Std.Data.DHashMap.Lemmas
Std.DHashMap.alter.congr_simp : ∀ {α : Type u} {β : α → Type v} {x : BEq α} {x_1 : Hashable α} [inst : LawfulBEq α] (m m_1 : Std.DHashMap α β),
  m = m_1 → ∀ (a : α) (f f_1 : Option (β a) → Option (β a)), f = f_1 → m.alter a f = m_1.alter a f_1
-- Mathlib.GroupTheory.Commutator.Basic
/-- **The Hall-Witt identity**  -/
commutatorElement_commutatorElement_conj_mul : ∀ {G : Type u_1} [inst : Group G] (a b c : G), ⁅⁅a, b⁆, b * c * b⁻¹⁆ * ⁅⁅b, c⁆, c * a * c⁻¹⁆ * ⁅⁅c, a⁆, a * b * a⁻¹⁆ = 1
-- Mathlib.Topology.NhdsWithin
/-- Obtain a "predictably-sided" neighborhood of `b` from two one-sided neighborhoods.  -/
nhds_of_Ici_Iic : ∀ {α : Type u_1} [inst : TopologicalSpace α] [inst_1 : LinearOrder α] {b : α} {L : Set α},
  L ∈ nhdsWithin b (Set.Iic b) → ∀ {R : Set α}, R ∈ nhdsWithin b (Set.Ici b) → L ∩ Set.Iic b ∪ R ∩ Set.Ici b ∈ nhds b
-- Std.Data.DTreeMap.Internal.Zipper
Std.DTreeMap.Internal.Const.RciSliceData.mk.inj : ∀ {α : Type u} {β : Type v} {inst : Ord α} {treeMap : Std.DTreeMap.Internal.Impl α fun x => β} {range : Std.Rci α}
  {treeMap_1 : Std.DTreeMap.Internal.Impl α fun x => β} {range_1 : Std.Rci α},
  { treeMap := treeMap, range := range } = { treeMap := treeMap_1, range := range_1 } →
    treeMap = treeMap_1 ∧ range = range_1
-- Init.Omega.Constraint
Option.merge.eq_3 : ∀ {α : Type u_1} (fn : α → α → α) (y : α), Option.merge fn none (some y) = some y
-- Mathlib.Tactic.ReduceModChar
/-- Given an expression `(-e) : t` such that `t` is a ring of characteristic `n`,
simplify this to `(n - 1) * e`.

This should be called only when `normIntNumeral` fails, because `normIntNumeral` would otherwise
be more useful by evaluating `-e` mod `n` to an actual numeral.
 -/
Tactic.ReduceModChar.normNeg : {u : Lean.Level} →
  {α : Q(Type u)} →
    (n : Q(ℕ)) → Q(«$α») → (_instRing : Q(Ring «$α»)) → Q(CharP «$α» «$n») → Lean.MetaM Lean.Meta.Simp.Result
-- Mathlib.RingTheory.RootsOfUnity.Basic
/-- `rootsOfUnity k M` is the subgroup of elements `m : Mˣ` that satisfy `m ^ k = 1`.  -/
rootsOfUnity : ℕ → (M : Type u_7) → [inst : CommMonoid M] → Subgroup Mˣ
-- Mathlib.Topology.MetricSpace.HolderNorm
eHolderNorm.eq_1 : ∀ {X : Type u_1} {Y : Type u_2} [inst : PseudoEMetricSpace X] [inst_1 : PseudoEMetricSpace Y] (r : NNReal) (f : X → Y),
  eHolderNorm r f = ⨅ C, ⨅ (_ : HolderWith C r f), ↑C
-- Mathlib.Algebra.MvPolynomial.Expand
MvPolynomial.expand_mul_eq_comp : ∀ {σ : Type u_1} {R : Type u_3} [inst : CommSemiring R] (p q : ℕ),
  MvPolynomial.expand (p * q) = (MvPolynomial.expand p).comp (MvPolynomial.expand q)
-- Mathlib.Algebra.Order.Group.Cyclic
LinearOrderedCommGroup.Subgroup.genLTOne_unique : ∀ {G : Type u_1} [inst : CommGroup G] [inst_1 : LinearOrder G] [inst_2 : IsOrderedMonoid G] (H : Subgroup G)
  [inst_3 : Nontrivial ↥H] [hH : IsCyclic ↥H] {g : G},
  g < 1 → Subgroup.zpowers g = H → g = LinearOrderedCommGroup.Subgroup.genLTOne H
-- Mathlib.Combinatorics.SimpleGraph.Copy
/-- The relation `IsContained A B`, `A ⊑ B` says that `B` contains a copy of `A`.

This is equivalent to the existence of an isomorphism from `A` to a subgraph of `B`.  -/
SimpleGraph.«term_⊑_» : Lean.TrailingParserDescr
-- Mathlib.SetTheory.Ordinal.Principal
/-- **Alias** of `Ordinal.isPrincipal_iff_of_monotone`. -/
Ordinal.principal_iff_of_monotone : ∀ {o : Ordinal.{u}} {op : Ordinal.{u} → Ordinal.{u} → Ordinal.{u}},
  (∀ (a : Ordinal.{u}), Monotone (op a)) →
    (∀ (a : Ordinal.{u}), Monotone (Function.swap op a)) → (Ordinal.IsPrincipal op o ↔ ∀ a < o, op a a < o)
-- Mathlib.LinearAlgebra.RootSystem.Chain
RootPairing.one_le_chainBotCoeff_of_root_add_mem : ∀ {ι : Type u_1} {R : Type u_2} {M : Type u_3} {N : Type u_4} [inst : Finite ι] [inst_1 : CommRing R]
  [inst_2 : CharZero R] [inst_3 : IsDomain R] [inst_4 : AddCommGroup M] [inst_5 : Module R M] [inst_6 : AddCommGroup N]
  [inst_7 : Module R N] {P : RootPairing ι R M N} [inst_8 : P.IsCrystallographic] {i j : ι} [P.IsReduced],
  P.root i - P.root j ∈ Set.range ⇑P.root → 1 ≤ RootPairing.chainBotCoeff i j
-- Mathlib.CategoryTheory.Limits.Shapes.Multiequalizer
CategoryTheory.Limits.WalkingMultispan.instSmallCategory : {J : CategoryTheory.Limits.MultispanShape} → CategoryTheory.SmallCategory (CategoryTheory.Limits.WalkingMultispan J)
-- Lean.Parser.Extension
Lean.Parser.registerParserCategory : Lean.Environment →
  Lean.Name →
    Lean.Name →
      optParam Lean.Parser.LeadingIdentBehavior Lean.Parser.LeadingIdentBehavior.default →
        autoParam Lean.Name Lean.Parser.registerParserCategory._auto_1 → IO Lean.Environment
-- Init.Data.Vector.Lemmas
Vector.replicate_eq_append_iff : ∀ {α : Type u_1} {n m : ℕ} {xs : Vector α n} {ys : Vector α m} {a : α},
  Vector.replicate (n + m) a = xs ++ ys ↔ xs = Vector.replicate n a ∧ ys = Vector.replicate m a
-- Lean.Parser.Term
Lean.Parser.Term.assert.formatter : Lean.PrettyPrinter.Formatter
-- Std.Data.TreeSet.Basic
/-- Tries to retrieve the largest element of the tree set, returning `none` if the set is empty.
 -/
Std.TreeSet.max? : {α : Type u} → {cmp : α → α → Ordering} → Std.TreeSet α cmp → Option α
-- Mathlib.Geometry.Euclidean.SignedDist
signedDist_vsub_self : ∀ {V : Type u_1} {P : Type u_2} [inst : NormedAddCommGroup V] [inst_1 : InnerProductSpace ℝ V] [inst_2 : MetricSpace P]
  [inst_3 : NormedAddTorsor V P] (p q : P), ((signedDist (q -ᵥ p)) p) q = dist p q
-- Mathlib.CategoryTheory.Sites.NonabelianCohomology.H1
/-- The cohomology (equivalence) relation on 1-cocycles.  -/
CategoryTheory.PresheafOfGroups.OneCocycle.IsCohomologous : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    {G : CategoryTheory.Functor Cᵒᵖ GrpCat} →
      {I : Type w'} →
        {U : I → C} →
          CategoryTheory.PresheafOfGroups.OneCocycle G U → CategoryTheory.PresheafOfGroups.OneCocycle G U → Prop
-- Init.Data.SInt.Bitwise
ISize.zero_xor : ∀ {a : ISize}, 0 ^^^ a = a
-- Mathlib.Topology.Category.CompHausLike.Limits
CompHausLike.instHasExplicitPullbacksOfInclusionsOfHasExplicitPullbacks : ∀ {P : TopCat → Prop} [CompHausLike.HasExplicitPullbacks P] [inst : CompHausLike.HasExplicitFiniteCoproducts P],
  CompHausLike.HasExplicitPullbacksOfInclusions P
-- Mathlib.Combinatorics.Matroid.Loop
Matroid.uniqueBaseOn_isLoop_iff : ∀ {α : Type u_1} {e : α} {I E : Set α}, (Matroid.uniqueBaseOn I E).IsLoop e ↔ e ∈ E \ I
-- Mathlib.Tactic.Module
Mathlib.Tactic.Module.NF.add_eq_eval₂ : ∀ {R : Type u_2} {M : Type u_3} [inst : Semiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M] (r₁ r₂ : R) (x : M)
  {l₁ l₂ l : Mathlib.Tactic.Module.NF R M},
  l₁.eval + l₂.eval = l.eval → ((r₁, x) ::ᵣ l₁).eval + ((r₂, x) ::ᵣ l₂).eval = ((r₁ + r₂, x) ::ᵣ l).eval
-- Mathlib.Algebra.BigOperators.Group.Finset.Basic
Finset.prod_filter_ne_one : ∀ {ι : Type u_1} {M : Type u_4} [inst : CommMonoid M] {f : ι → M} (s : Finset ι)
  [inst_1 : (x : ι) → Decidable (f x ≠ 1)], ∏ x ∈ s with f x ≠ 1, f x = ∏ x ∈ s, f x
-- Lean.Compiler.LCNF.Basic
Lean.Compiler.LCNF.LetValue.uproj.sizeOf_spec : ∀ {pu : Lean.Compiler.LCNF.Purity} (i : ℕ) (var : Lean.FVarId)
  (h : autoParam (pu = Lean.Compiler.LCNF.Purity.impure) Lean.Compiler.LCNF.LetValue._auto_9),
  sizeOf (Lean.Compiler.LCNF.LetValue.uproj i var h) = 1 + sizeOf i + sizeOf var + sizeOf h
-- Init.Data.Int.Order
Int.eq_ofNat_of_zero_le : ∀ {a : ℤ}, 0 ≤ a → ∃ n, a = ↑n
-- Mathlib.Tactic.FunProp.Core
/-- Cache result if it does not have any subgoals.  -/
Mathlib.Meta.FunProp.cacheResult : Lean.Expr → Mathlib.Meta.FunProp.Result → Mathlib.Meta.FunProp.FunPropM Mathlib.Meta.FunProp.Result
-- Mathlib.Algebra.Lie.Weights.Basic
LieModule.disjoint_genWeightSpace : ∀ (R : Type u_2) (L : Type u_3) (M : Type u_4) [inst : CommRing R] [inst_1 : LieRing L] [inst_2 : LieAlgebra R L]
  [inst_3 : AddCommGroup M] [inst_4 : Module R M] [inst_5 : LieRingModule L M] [inst_6 : LieModule R L M]
  [inst_7 : LieRing.IsNilpotent L] [IsDomain R] [Module.IsTorsionFree R M] {χ₁ χ₂ : L → R},
  χ₁ ≠ χ₂ → Disjoint (LieModule.genWeightSpace M χ₁) (LieModule.genWeightSpace M χ₂)
-- Mathlib.Algebra.Homology.Double
HomologicalComplex.isZero_double_X : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  [inst_2 : CategoryTheory.Limits.HasZeroObject C] {X₀ X₁ : C} (f : X₀ ⟶ X₁) {ι : Type u_2} {c : ComplexShape ι}
  {i₀ i₁ : ι} (hi₀₁ : c.Rel i₀ i₁) (k : ι),
  k ≠ i₀ → k ≠ i₁ → CategoryTheory.Limits.IsZero ((HomologicalComplex.double f hi₀₁).X k)
-- Mathlib.Combinatorics.SimpleGraph.Paths
SimpleGraph.Walk.IsPath.getVert_injOn : ∀ {V : Type u} {G : SimpleGraph V} {u v : V} {p : G.Walk u v}, p.IsPath → Set.InjOn p.getVert {i | i ≤ p.length}
-- Mathlib.Geometry.Euclidean.Incenter
Affine.Simplex.touchpoint_mem_insphere : ∀ {V : Type u_1} {P : Type u_2} [inst : NormedAddCommGroup V] [inst_1 : InnerProductSpace ℝ V] [inst_2 : MetricSpace P]
  [inst_3 : NormedAddTorsor V P] {n : ℕ} [inst_4 : NeZero n] (s : Affine.Simplex ℝ P n) (i : Fin (n + 1)),
  s.touchpoint ∅ i ∈ s.insphere
-- Mathlib.GroupTheory.OreLocalization.Basic
OreLocalization.instCommMonoid.eq_1 : ∀ {R : Type u_1} [inst : CommMonoid R] {S : Submonoid R} [inst_1 : OreLocalization.OreSet S],
  OreLocalization.instCommMonoid = { toMonoid := OreLocalization.instMonoid, mul_comm := ⋯ }
-- Mathlib.Tactic.Positivity.Core
Mathlib.Meta.Positivity.Strictness.nonzero.injEq : ∀ {u : Lean.Level} {α : Q(Type u)} {zα : Q(Zero «$α»)} {e : Q(«$α»)} {pα? : Option Q(PartialOrder «$α»)}
  (pf pf_1 : Q(«$e» ≠ 0)),
  (Mathlib.Meta.Positivity.Strictness.nonzero pf = Mathlib.Meta.Positivity.Strictness.nonzero pf_1) = (pf = pf_1)
-- Init.Data.List.Lemmas
List.elem_eq_mem : ∀ {α : Type u_1} [inst : BEq α] [inst_1 : LawfulBEq α] (a : α) (as : List α), List.elem a as = decide (a ∈ as)
-- Mathlib.Data.Matrix.Block
Matrix.blockDiag'_apply : ∀ {o : Type u_4} {m' : o → Type u_7} {n' : o → Type u_8} {α : Type u_12}
  (M : Matrix ((i : o) × m' i) ((i : o) × n' i) α) (k : o) (i : m' k) (j : n' k), M.blockDiag' k i j = M ⟨k, i⟩ ⟨k, j⟩
-- Mathlib.Geometry.Manifold.IsManifold.ExtChartAt
map_extChartAt_symm_nhdsWithin_range' : ∀ {𝕜 : Type u_1} {E : Type u_2} {M : Type u_3} {H : Type u_4} [inst : NontriviallyNormedField 𝕜]
  [inst_1 : NormedAddCommGroup E] [inst_2 : NormedSpace 𝕜 E] [inst_3 : TopologicalSpace H] [inst_4 : TopologicalSpace M]
  {I : ModelWithCorners 𝕜 E H} [inst_5 : ChartedSpace H M] {x y : M},
  y ∈ (extChartAt I x).source →
    Filter.map (↑(extChartAt I x).symm) (nhdsWithin (↑(extChartAt I x) y) (Set.range ↑I)) = nhds y
-- Lean.Data.Lsp.LanguageFeatures
Lean.Lsp.RenameOptions : Type
-- Mathlib.Algebra.Polynomial.Module.Basic
/-- **Alias** of the forward direction of `PolynomialModule.coeff_inj`. -/
PolynomialModule.ext : ∀ {R : Type u_2} {M : Type u_3} [inst : CommRing R] [inst_1 : AddCommGroup M] [inst_2 : Module R M]
  {x y : PolynomialModule R M}, x.coeff = y.coeff → x = y
-- Mathlib.Data.Ordmap.Ordnode
/-- **Internal use only**

The ratio between an outer and inner sibling of the
heavier subtree in an unbalanced setting. It determines
whether a double or single rotation should be performed
to restore balance. It is corresponds with the inverse
of `α` in Adam's article.  -/
Ordnode.ratio : ℕ
-- Std.Http.Data.Body.Stream
/-- Builds a request with a streaming body generator.
 -/
Std.Http.Request.Builder.stream : Std.Http.Request.Builder →
  (Std.Http.Body.Stream → Std.Async.Async Unit) → Std.Async.Async (Std.Http.Request Std.Http.Body.Stream)
-- Std.Data.TreeSet.Raw.Lemmas
Std.TreeSet.Raw.Equiv.getLTD_eq : ∀ {α : Type u} {cmp : α → α → Ordering} {t₁ t₂ : Std.TreeSet.Raw α cmp} [Std.TransCmp cmp] {k fallback : α},
  t₁.WF → t₂.WF → t₁.Equiv t₂ → t₁.getLTD k fallback = t₂.getLTD k fallback
-- Mathlib.Data.Finsupp.Multiset
/-- The order on `ι →₀ ℕ` is well-founded.  -/
Finsupp.lt_wf : ∀ (ι : Type u_3), WellFounded LT.lt
-- Mathlib.Analysis.LocallyConvex.Separation
/-- If `A` is convex with nonempty interior and `x ∉ interior A`, then there is a nonzero
continuous linear functional whose maximum on `A` is attained at `x`.  -/
geometric_hahn_banach_of_nonempty_interior_point : ∀ {E : Type u_2} [inst : TopologicalSpace E] [inst_1 : AddCommGroup E] [inst_2 : Module ℝ E] {x : E}
  [IsTopologicalAddGroup E] [ContinuousSMul ℝ E] {A : Set E},
  Convex ℝ A → x ∉ interior A → (interior A).Nonempty → ∃ f, f ≠ 0 ∧ ∀ a ∈ A, f a ≤ f x
-- Mathlib.Tactic.CategoryTheory.BicategoricalComp
CategoryTheory.BicategoricalCoherence.left'_iso : ∀ {B : Type u} [inst : CategoryTheory.Bicategory B] {a b : B} (f g : a ⟶ b)
  [inst_1 : CategoryTheory.BicategoricalCoherence f g],
  CategoryTheory.BicategoricalCoherence.iso =
    CategoryTheory.BicategoricalCoherence.iso ≪≫ (CategoryTheory.Bicategory.leftUnitor g).symm
-- Lean.Environment
Lean.Environment.areRealizationsEnabledForConst : Lean.Environment → Lean.Name → Bool
-- Mathlib.Algebra.Order.Module.HahnEmbedding
HahnEmbedding.Seed.domain_baseEmbedding : ∀ {K : Type u_1} [inst : DivisionRing K] [inst_1 : LinearOrder K] [inst_2 : IsOrderedRing K] [inst_3 : Archimedean K]
  {M : Type u_2} [inst_4 : AddCommGroup M] [inst_5 : LinearOrder M] [inst_6 : IsOrderedAddMonoid M]
  [inst_7 : Module K M] [inst_8 : IsOrderedModule K M] {R : Type u_3} [inst_9 : AddCommGroup R]
  [inst_10 : LinearOrder R] [inst_11 : Module K R] (seed : HahnEmbedding.Seed K M R),
  seed.baseEmbedding.domain = seed.baseDomain
-- Mathlib.Data.Matrix.Block
/-- Two block matrices are equal if their blocks are equal.  -/
Matrix.ext_iff_blocks : ∀ {l : Type u_1} {m : Type u_2} {n : Type u_3} {o : Type u_4} {α : Type u_12} {A B : Matrix (n ⊕ o) (l ⊕ m) α},
  A = B ↔
    A.toBlocks₁₁ = B.toBlocks₁₁ ∧
      A.toBlocks₁₂ = B.toBlocks₁₂ ∧ A.toBlocks₂₁ = B.toBlocks₂₁ ∧ A.toBlocks₂₂ = B.toBlocks₂₂
-- Mathlib.Algebra.Order.Ring.Unbundled.Basic
mul_le_mul_of_nonpos_of_nonpos' : ∀ {R : Type u} [inst : Semiring R] [inst_1 : Preorder R] {a b c d : R} [ExistsAddOfLE R] [PosMulMono R] [MulPosMono R]
  [AddRightMono R] [AddRightReflectLE R], c ≤ a → d ≤ b → a ≤ 0 → d ≤ 0 → a * b ≤ c * d
-- Mathlib.CategoryTheory.Monoidal.Functor
CategoryTheory.Functor.LaxMonoidal.μ_natural_assoc : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.MonoidalCategory C] {D : Type u₂}
  [inst_2 : CategoryTheory.Category.{v₂, u₂} D] [inst_3 : CategoryTheory.MonoidalCategory D]
  (F : CategoryTheory.Functor C D) [inst_4 : F.LaxMonoidal] {X Y X' Y' : C} (f : X ⟶ Y) (g : X' ⟶ Y') {Z : D}
  (h : F.obj (CategoryTheory.MonoidalCategoryStruct.tensorObj Y Y') ⟶ Z),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.tensorHom (F.map f) (F.map g))
      (CategoryTheory.CategoryStruct.comp (CategoryTheory.Functor.LaxMonoidal.μ F Y Y') h) =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.Functor.LaxMonoidal.μ F X X')
      (CategoryTheory.CategoryStruct.comp (F.map (CategoryTheory.MonoidalCategoryStruct.tensorHom f g)) h)
-- Mathlib.Algebra.Homology.Single
HomologicalComplex.mkHomFromSingle_f : ∀ {V : Type u} [inst : CategoryTheory.Category.{v, u} V] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms V]
  [inst_2 : CategoryTheory.Limits.HasZeroObject V] {ι : Type u_1} [inst_3 : DecidableEq ι] {c : ComplexShape ι}
  {K : HomologicalComplex V c} {j : ι} {A : V} (φ : A ⟶ K.X j)
  (hφ : ∀ (k : ι), c.Rel j k → CategoryTheory.CategoryStruct.comp φ (K.d j k) = 0),
  (HomologicalComplex.mkHomFromSingle φ hφ).f j =
    CategoryTheory.CategoryStruct.comp (HomologicalComplex.singleObjXSelf c j A).hom φ
-- Aesop.Rule.Name
_private.Aesop.Rule.Name.0.Aesop.RuleName.instToJsonJson : Lean.ToJson Aesop.RuleName.Json✝
-- Mathlib.Analysis.InnerProductSpace.StandardSubspace
/-- The image of a standard subspace by the multiplication by `Complex.I`, bundled as a
`StandardSubspace`.  -/
StandardSubspace.mulI : {H : Type u_1} →
  [inst : NormedAddCommGroup H] → [inst_1 : InnerProductSpace ℂ H] → StandardSubspace H → StandardSubspace H
-- Mathlib.Topology.MetricSpace.Pseudo.Defs
dist_triangle8 : ∀ {α : Type u} [inst : PseudoMetricSpace α] (a b c d e f g h : α),
  dist a h ≤ dist a b + dist b c + dist c d + dist d e + dist e f + dist f g + dist g h
-- Mathlib.Data.Set.Insert
Set.disjoint_insert_right : ∀ {α : Type u_1} {s t : Set α} {a : α}, Disjoint s (insert a t) ↔ a ∉ s ∧ Disjoint s t
-- Std.Data.DTreeMap.Internal.Lemmas
Std.DTreeMap.Internal.Impl.getKey?_of_isEmpty : ∀ {α : Type u} {β : α → Type v} {instOrd : Ord α} {t : Std.DTreeMap.Internal.Impl α β} [Std.TransOrd α],
  t.WF → ∀ {a : α}, t.isEmpty = true → t.getKey? a = none
-- Mathlib.AlgebraicGeometry.Morphisms.QuasiFinite
AlgebraicGeometry.instLocallyQuasiFiniteOfIsFinite : ∀ {X Y : AlgebraicGeometry.Scheme} (f : X ⟶ Y) [AlgebraicGeometry.IsFinite f], AlgebraicGeometry.LocallyQuasiFinite f
-- Mathlib.CategoryTheory.Abelian.Basic
CategoryTheory.Abelian.has_finite_products : ∀ {C : Type u} {inst : CategoryTheory.Category.{v, u} C} [self : CategoryTheory.Abelian C],
  CategoryTheory.Limits.HasFiniteProducts C
-- Mathlib.CategoryTheory.Bicategory.NaturalTransformation.Lax
/-- `CategoryStruct` on `B ⥤ᴸ C` where the (1-)morphisms are given by strong
transformations.  -/
CategoryTheory.Lax.StrongTrans.categoryStruct : {B : Type u₁} →
  [inst : CategoryTheory.Bicategory B] →
    {C : Type u₂} →
      [inst_1 : CategoryTheory.Bicategory C] →
        CategoryTheory.CategoryStruct.{max (max (max u₁ v₁) v₂) w₂, max (max (max (max (max u₂ u₁) v₂) v₁) w₂) w₁}
          (CategoryTheory.LaxFunctor B C)
-- Mathlib.RingTheory.Finiteness.Basic
Submodule.fg_of_fg_map_injective : ∀ {R : Type u_1} {M : Type u_2} [inst : Semiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M] {S : Type u_3}
  {P : Type u_4} [inst_3 : Semiring S] [inst_4 : AddCommMonoid P] [inst_5 : Module S P] {σ : R →+* S}
  [inst_6 : RingHomSurjective σ] (f : M →ₛₗ[σ] P),
  Function.Injective ⇑f → ∀ {N : Submodule R M}, (Submodule.map f N).FG → N.FG
-- Mathlib.Analysis.Calculus.FDeriv.Mul
fderivWithin_multiset_prod : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {s : Set E} {ι : Type u_5} {𝔸' : Type u_7} [inst_3 : NormedCommRing 𝔸']
  [inst_4 : NormedAlgebra 𝕜 𝔸'] {g : ι → E → 𝔸'} [inst_5 : DecidableEq ι] {u : Multiset ι} {x : E},
  UniqueDiffWithinAt 𝕜 s x →
    (∀ i ∈ u, DifferentiableWithinAt 𝕜 (fun x => g i x) s x) →
      fderivWithin 𝕜 (fun x => (Multiset.map (fun x_1 => g x_1 x) u).prod) s x =
        (Multiset.map (fun i => (Multiset.map (fun x_1 => g x_1 x) (u.erase i)).prod • fderivWithin 𝕜 (g i) s x) u).sum
-- Mathlib.Algebra.Group.Subgroup.Map
Subgroup.gc_map_comap : ∀ {G : Type u_1} [inst : Group G] {N : Type u_5} [inst_1 : Group N] (f : G →* N),
  GaloisConnection (Subgroup.map f) (Subgroup.comap f)
-- Lean.Data.Lsp.LanguageFeatures
Lean.Lsp.ReferenceParams.mk.inj : ∀ {toTextDocumentPositionParams : Lean.Lsp.TextDocumentPositionParams} {context : Lean.Lsp.ReferenceContext}
  {toTextDocumentPositionParams_1 : Lean.Lsp.TextDocumentPositionParams} {context_1 : Lean.Lsp.ReferenceContext},
  { toTextDocumentPositionParams := toTextDocumentPositionParams, context := context } =
      { toTextDocumentPositionParams := toTextDocumentPositionParams_1, context := context_1 } →
    toTextDocumentPositionParams = toTextDocumentPositionParams_1 ∧ context = context_1
-- Mathlib.Algebra.Category.Grp.EpiMono
GrpCat.SurjectiveOfEpiAuxs.fromCoset_eq_of_mem_range : ∀ {A B : GrpCat} (f : A ⟶ B) {b : ↑B},
  b ∈ (GrpCat.Hom.hom f).range →
    GrpCat.SurjectiveOfEpiAuxs.XWithInfinity.fromCoset ⟨b • ↑(GrpCat.Hom.hom f).range, ⋯⟩ =
      GrpCat.SurjectiveOfEpiAuxs.XWithInfinity.fromCoset ⟨↑(GrpCat.Hom.hom f).range, ⋯⟩
-- Mathlib.RingTheory.Coalgebra.Basic
/-- Transfer `Coalgebra.IsCocomm` across an `Equiv`.  -/
Equiv.coalgebraIsCocomm : ∀ (R : Type u_1) {A : Type u_2} {B : Type u_3} [inst : CommSemiring R] [inst_1 : AddCommMonoid B] [inst_2 : Module R B]
  [inst_3 : Coalgebra R B] [Coalgebra.IsCocomm R B] (e : A ≃ B), Coalgebra.IsCocomm R A
-- Mathlib.FieldTheory.IntermediateField.Adjoin.Algebra
IntermediateField.adjoin_eq_algebra_adjoin : ∀ (F : Type u_1) [inst : Field F] {E : Type u_2} [inst_1 : Field E] [inst_2 : Algebra F E] (S : Set E),
  (∀ x ∈ Algebra.adjoin F S, x⁻¹ ∈ Algebra.adjoin F S) →
    (IntermediateField.adjoin F S).toSubalgebra = Algebra.adjoin F S
-- Std.Data.DHashMap.RawLemmas
Std.DHashMap.Raw.Const.getThenInsertIfNew?_snd : ∀ {α : Type u} [inst : BEq α] [inst_1 : Hashable α] {β : Type v} {m : Std.DHashMap.Raw α fun x => β},
  m.WF → ∀ {k : α} {v : β}, (Std.DHashMap.Raw.Const.getThenInsertIfNew? m k v).2 = m.insertIfNew k v
-- Mathlib.Analysis.CStarAlgebra.Classes
CStarAlgebra.toStarRing : {A : Type u_1} → [self : CStarAlgebra A] → StarRing A
-- Mathlib.CategoryTheory.Limits.Shapes.Products
CategoryTheory.Limits.Sigma.functorι_app : ∀ {α : Type w₂} {C : Type u} [inst : CategoryTheory.Category.{v, u} C]
  [inst_1 : CategoryTheory.Limits.HasCoproductsOfShape α C] (a : α) (f : α → C),
  (CategoryTheory.Limits.Sigma.functorι a).app f = CategoryTheory.Limits.Sigma.ι f a
-- Lean.Meta.Tactic.Grind.Extension
Lean.Meta.Grind.EMatchTheoremConstraint.genLt.injEq : ∀ (n n_1 : ℕ),
  (Lean.Meta.Grind.EMatchTheoremConstraint.genLt n = Lean.Meta.Grind.EMatchTheoremConstraint.genLt n_1) = (n = n_1)
-- Mathlib.CategoryTheory.PathCategory.MorphismProperty
CategoryTheory.MorphismProperty.composePath_mem : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] (W : CategoryTheory.MorphismProperty C)
  [W.IsMultiplicative] {X Y : C} {p : Quiver.Path X Y}, W.paths p → W (CategoryTheory.composePath p)
-- Mathlib.CategoryTheory.Monad.Adjunction
CategoryTheory.Comonad.comparisonForget_hom_app : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  {L : CategoryTheory.Functor C D} {R : CategoryTheory.Functor D C} (h : L ⊣ R) (x : C),
  (CategoryTheory.Comonad.comparisonForget h).hom.app x =
    CategoryTheory.CategoryStruct.id (((CategoryTheory.Comonad.comparison h).comp h.toComonad.forget).obj x)
-- Mathlib.AlgebraicTopology.ModelCategory.PathObject
HomotopicalAlgebra.PrepathObject.mk : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    {A : C} →
      (P : C) →
        (p₀ p₁ : P ⟶ A) →
          (ι : A ⟶ P) →
            autoParam (CategoryTheory.CategoryStruct.comp ι p₀ = CategoryTheory.CategoryStruct.id A)
                HomotopicalAlgebra.PrepathObject.ι_p₀._autoParam →
              autoParam (CategoryTheory.CategoryStruct.comp ι p₁ = CategoryTheory.CategoryStruct.id A)
                  HomotopicalAlgebra.PrepathObject.ι_p₁._autoParam →
                HomotopicalAlgebra.PrepathObject A
-- Mathlib.Algebra.Polynomial.Eval.Defs
Polynomial.map_mul : ∀ {R : Type u} {S : Type v} [inst : Semiring R] {p q : Polynomial R} [inst_1 : Semiring S] (f : R →+* S),
  Polynomial.map f (p * q) = Polynomial.map f p * Polynomial.map f q