mathlib-initiative/mathlib-types huggingface dataset:
-- Std.Tactic.BVDecide.Bitblast.BVExpr.Circuit.Impl.Operations.RotateRight
Std.Tactic.BVDecide.BVExpr.bitblast.blastRotateRight.go : {α : Type} →
  [inst : Hashable α] →
    [inst_1 : DecidableEq α] →
      {w : ℕ} → {aig : Std.Sat.AIG α} → aig.RefVec w → ℕ → (curr : ℕ) → curr ≤ w → aig.RefVec curr → aig.RefVec w
-- Mathlib.Topology.MetricSpace.Defs
zero_eq_dist : ∀ {γ : Type w} [inst : MetricSpace γ] {x y : γ}, 0 = dist x y ↔ x = y
-- Mathlib.GroupTheory.ArchimedeanDensely
AddSubgroup.isLeast_of_closure_iff_eq_abs : ∀ {G : Type u_1} [inst : AddCommGroup G] [inst_1 : LinearOrder G] [IsOrderedAddMonoid G] [Archimedean G] {a b : G},
  IsLeast {y | y ∈ AddSubgroup.closure {a} ∧ 0 < y} b ↔ b = |a| ∧ 0 < b
-- Mathlib.Analysis.SpecialFunctions.MulExpNegMulSq
Real.mulExpNegMulSq.eq_1 : ∀ (ε x : ℝ), ε.mulExpNegMulSq x = x * Real.exp (-(ε * x * x))
-- Mathlib.Tactic.CategoryTheory.Coherence.Datatypes
Mathlib.Tactic.BicategoryLike.Context.mk : {ρ : Type} → (Lean.Expr → Lean.MetaM (Option ρ)) → Mathlib.Tactic.BicategoryLike.Context ρ
-- Mathlib.Combinatorics.Graph.Basic
Graph.IsLink.inc_left : ∀ {α : Type u_1} {β : Type u_2} {x y : α} {e : β} {G : Graph α β}, G.IsLink e x y → G.Inc e x
-- Mathlib.MeasureTheory.Integral.SetToL1
MeasureTheory.setToFun_zero : ∀ {α : Type u_1} {E : Type u_2} {F : Type u_3} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E]
  [inst_2 : NormedAddCommGroup F] [inst_3 : NormedSpace ℝ F] {m : MeasurableSpace α} {μ : MeasureTheory.Measure α}
  {T : Set α → E →L[ℝ] F} {C : ℝ} (hT : MeasureTheory.DominatedFinMeasAdditive μ T C),
  MeasureTheory.setToFun μ T hT 0 = 0
-- Mathlib.Topology.Connected.PathConnected
AddSubmonoid.coe_pathComponentZero : ∀ (M : Type u_4) [inst : AddMonoid M] [inst_1 : TopologicalSpace M] [inst_2 : ContinuousAdd M],
  ↑(AddSubmonoid.pathComponentZero M) = pathComponent 0
-- Mathlib.MeasureTheory.Measure.MeasureSpace
MeasureTheory.Measure.ae_smul_measure : ∀ {α : Type u_1} {R : Type u_6} {m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} {p : α → Prop}
  [inst : SMul R ENNReal] [inst_1 : IsScalarTower R ENNReal ENNReal],
  (∀ᵐ (x : α) ∂μ, p x) → ∀ (c : R), ∀ᵐ (x : α) ∂c • μ, p x
-- Mathlib.MeasureTheory.Integral.DivergenceTheorem
/-- **Divergence theorem** for functions on the plane. It is formulated in terms of two functions
`f g : ℝ × ℝ → E` and iterated integral `∫ x in a₁..b₁, ∫ y in a₂..b₂, _`, where
`a₁ a₂ b₁ b₂ : ℝ`. When thinking of `f` and `g` as the two coordinates of a single function
`F : ℝ × ℝ → E × E` and when `E = ℝ`, this is the usual statement that the integral of the
divergence of `F` inside the rectangle with vertices `(aᵢ, bⱼ)`, `i, j = 1, 2`,
equals the integral of the normal derivative of `F` along the boundary.

See also `MeasureTheory.integral_divergence_prod_Icc_of_hasFDerivAt_of_le`
for a version that uses an integral over `Icc a b`, where `a b : ℝ × ℝ`, `a ≤ b`.

See also `integral2_divergence_prod_of_hasFDerivAt_off_countable`
for a version that assumes differentiability outside of a countable set.  -/
MeasureTheory.integral2_divergence_prod_of_hasFDerivAt : ∀ {E : Type u} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] (f g : ℝ × ℝ → E)
  (f' g' : ℝ × ℝ → ℝ × ℝ →L[ℝ] E) (a₁ a₂ b₁ b₂ : ℝ),
  ContinuousOn f (Set.uIcc a₁ b₁ ×ˢ Set.uIcc a₂ b₂) →
    ContinuousOn g (Set.uIcc a₁ b₁ ×ˢ Set.uIcc a₂ b₂) →
      (∀ x ∈ Set.Ioo (min a₁ b₁) (max a₁ b₁) ×ˢ Set.Ioo (min a₂ b₂) (max a₂ b₂), HasFDerivAt f (f' x) x) →
        (∀ x ∈ Set.Ioo (min a₁ b₁) (max a₁ b₁) ×ˢ Set.Ioo (min a₂ b₂) (max a₂ b₂), HasFDerivAt g (g' x) x) →
          MeasureTheory.IntegrableOn (fun x => (f' x) (1, 0) + (g' x) (0, 1)) (Set.uIcc a₁ b₁ ×ˢ Set.uIcc a₂ b₂)
              MeasureTheory.volume →
            ∫ (x : ℝ) in a₁..b₁, ∫ (y : ℝ) in a₂..b₂, (f' (x, y)) (1, 0) + (g' (x, y)) (0, 1) =
              (((∫ (x : ℝ) in a₁..b₁, g (x, b₂)) - ∫ (x : ℝ) in a₁..b₁, g (x, a₂)) + ∫ (y : ℝ) in a₂..b₂, f (b₁, y)) -
                ∫ (y : ℝ) in a₂..b₂, f (a₁, y)
-- Std.Data.ExtDTreeMap.Lemmas
Std.ExtDTreeMap.mem_of_mem_filterMap : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t : Std.ExtDTreeMap α β cmp} {γ : α → Type w}
  [inst : Std.TransCmp cmp] {f : (a : α) → β a → Option (γ a)} {k : α}, k ∈ Std.ExtDTreeMap.filterMap f t → k ∈ t
-- Mathlib.Data.Finset.Sups
/-- **Alias** of the reverse direction of `Finset.compls_nonempty`. -/
Finset.Nonempty.compls : ∀ {α : Type u_2} [inst : BooleanAlgebra α] {s : Finset α}, s.Nonempty → s.compls.Nonempty
-- Mathlib.CategoryTheory.FintypeCat
FintypeCat.hom_ext : ∀ {X Y : FintypeCat} (f g : X ⟶ Y),
  (∀ (x : (fun X => X.obj) X), (CategoryTheory.ConcreteCategory.hom f) x = (CategoryTheory.ConcreteCategory.hom g) x) →
    f = g
-- Mathlib.Topology.MetricSpace.Antilipschitz
AntilipschitzWith.id : ∀ {α : Type u_1} [inst : PseudoEMetricSpace α], AntilipschitzWith 1 id
-- Mathlib.CategoryTheory.Category.ReflQuiv
CategoryTheory.Cat.toFreeRefl_obj : ∀ (V : Type u_1) [inst : CategoryTheory.ReflQuiver V] (v : V),
  (CategoryTheory.Cat.toFreeRefl V).obj v = CategoryTheory.Cat.FreeRefl.mk v
-- Mathlib.Data.List.Forall2
/-- Given a relation `R`, `sublist_forall₂ r l₁ l₂` indicates that there is a sublist of `l₂` such
that `forall₂ r l₁ l₂`.  -/
List.SublistForall₂ : {α : Type u_1} → {β : Type u_2} → (α → β → Prop) → List α → List β → Prop
-- Mathlib.LinearAlgebra.Matrix.Basis
/-- From a basis `e : ι → M` and a family of vectors `v : ι' → M`, make the matrix whose columns
are the vectors `v i` written in the basis `e`.  -/
Module.Basis.toMatrix : {ι : Type u_1} →
  {ι' : Type u_2} →
    {R : Type u_5} →
      {M : Type u_6} →
        [inst : CommSemiring R] →
          [inst_1 : AddCommMonoid M] → [inst_2 : Module R M] → Module.Basis ι R M → (ι' → M) → Matrix ι ι' R
-- Init.Data.String.Defs
String.Slice.Pos.lt_trans : ∀ {s : String.Slice} {p q r : s.Pos}, p < q → q < r → p < r
-- Std.Data.HashMap.Lemmas
Std.HashMap.contains_iff_mem : ∀ {α : Type u} {β : Type v} {x : BEq α} {x_1 : Hashable α} {m : Std.HashMap α β} {a : α}, m.contains a = true ↔ a ∈ m
-- Mathlib.RingTheory.Congruence.Basic
RingCon.coe_top : ∀ {R : Type u_3} [inst : Add R] [inst_1 : Mul R], ⇑⊤ = ⊤
-- Mathlib.Analysis.Real.Pi.Wallis
Real.Wallis.W_pos : ∀ (k : ℕ), 0 < Real.Wallis.W k
-- Mathlib.CategoryTheory.Limits.Shapes.RegularMono
CategoryTheory.MorphismProperty.regularEpi.containsIdentities : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C],
  (CategoryTheory.MorphismProperty.regularEpi C).ContainsIdentities
-- Std.Time.Format
/-- Parses a `String` in the `ISO8601`, `RFC822` or `RFC850` format and returns a `DateTime`.
 -/
Std.Time.DateTime.parse : String → Except String Std.Time.DateTime
-- Mathlib.Topology.MetricSpace.Bounded
Metric.instBoundedSpaceOfCompactSpace : ∀ {α : Type u} [inst : PseudoMetricSpace α] [CompactSpace α], BoundedSpace α
-- Mathlib.Combinatorics.Enumerative.InclusionExclusion
/-- **Inclusion-exclusion principle** for the cardinality of a union.

The cardinality of the union of the `S i` over `i ∈ s` is the alternating sum of the cardinalities
of the intersections of the `S i`.  -/
Finset.inclusion_exclusion_card_biUnion : ∀ {ι : Type u_1} {α : Type u_2} [inst : DecidableEq α] (s : Finset ι) (S : ι → Finset α),
  ↑(s.biUnion S).card = ∑ t, (-1) ^ ((↑t).card + 1) * ↑((↑t).inf' ⋯ S).card
-- Std.Data.DTreeMap.Internal.Model
_private.Std.Data.DTreeMap.Internal.Model.0.Std.DTreeMap.Internal.Impl.getEntryGE?ₘ'.match_1.eq_3 : ∀ {α : Type u_2} {β : α → Type u_1} [inst : Ord α] (k : α)
  (motive : Option ((a : α) × β a) → Std.DTreeMap.Internal.Impl.ExplorationStep α β (compare k) → Sort u_3)
  (base : Option ((a : α) × β a)) (a : List ((a : α) × β a)) (a_1 : α) (a_2 : compare k a_1 = Ordering.gt) (a_3 : β a_1)
  (h_1 :
    (x : Option ((a : α) × β a)) →
      (k' : α) →
        (a : compare k k' = Ordering.lt) →
          (v : β k') →
            (a_4 : List ((a : α) × β a)) → motive x (Std.DTreeMap.Internal.Impl.ExplorationStep.lt k' a v a_4))
  (h_2 :
    (base : Option ((a : α) × β a)) →
      (a : List ((a : α) × β a)) →
        (c : Std.DTreeMap.Internal.Cell α β (compare k)) →
          (r : List ((a : α) × β a)) → motive base (Std.DTreeMap.Internal.Impl.ExplorationStep.eq a c r))
  (h_3 :
    (base : Option ((a : α) × β a)) →
      (a : List ((a : α) × β a)) →
        (a_4 : α) →
          (a_5 : compare k a_4 = Ordering.gt) →
            (a_6 : β a_4) → motive base (Std.DTreeMap.Internal.Impl.ExplorationStep.gt a a_4 a_5 a_6)),
  (match base, Std.DTreeMap.Internal.Impl.ExplorationStep.gt a a_1 a_2 a_3 with
    | x, Std.DTreeMap.Internal.Impl.ExplorationStep.lt k' a v a_4 => h_1 x k' a v a_4
    | base, Std.DTreeMap.Internal.Impl.ExplorationStep.eq a c r => h_2 base a c r
    | base, Std.DTreeMap.Internal.Impl.ExplorationStep.gt a a_4 a_5 a_6 => h_3 base a a_4 a_5 a_6) =
    h_3 base a a_1 a_2 a_3
-- Mathlib.Order.BooleanAlgebra.Set
Set.sdiff_sdiff_right_self : ∀ {α : Type u_1} (s t : Set α), s \ (s \ t) = s ∩ t
-- Mathlib.GroupTheory.SpecificGroups.Cyclic.Basic
/-- Any non-identity element of a finite group of prime order generates the group.  -/
zpowers_eq_top_of_prime_card : ∀ {G : Type u_2} [inst : Group G] {p : ℕ} [hp : Fact (Nat.Prime p)],
  Nat.card G = p → ∀ {g : G}, g ≠ 1 → Subgroup.zpowers g = ⊤
-- Init.Data.String.Lemmas.FindPos
String.Slice.posLE_lt_iff : ∀ {s : String.Slice} {p : s.Pos} {q : String.Pos.Raw}, s.posLE q < p ↔ q < p.offset
-- Mathlib.RingTheory.Ideal.Int
Nat.absNorm_under_prime : ∀ {R : Type u_1} [inst : CommRing R] [IsDomain R] [Algebra.IsIntegral ℤ R] (P : Ideal R) [P.IsPrime] [NeZero P],
  Nat.Prime (Ideal.absNorm (Ideal.under ℤ P))
-- Mathlib.CategoryTheory.Adjunction.Limits
CategoryTheory.Adjunction.functorialityLeftAdjoint.eq_1 : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  {F : CategoryTheory.Functor C D} {G : CategoryTheory.Functor D C} (adj : F ⊣ G) {J : Type u}
  [inst_2 : CategoryTheory.Category.{v, u} J] (K : CategoryTheory.Functor J D),
  adj.functorialityLeftAdjoint K =
    (CategoryTheory.Limits.Cone.functoriality (K.comp G) F).comp
      (CategoryTheory.Limits.Cone.postcompose
        (CategoryTheory.CategoryStruct.comp (K.associator G F).hom
          (CategoryTheory.CategoryStruct.comp (K.whiskerLeft adj.counit) K.rightUnitor.hom)))
-- Mathlib.RingTheory.EssentialFiniteness
/-- A choice of a subalgebra of finite type in an essentially of finite type algebra, such that
its localization is the whole ring.  -/
Algebra.EssFiniteType.subalgebra : (R : Type u_1) →
  (S : Type u_2) →
    [inst : CommRing R] → [inst_1 : CommRing S] → [inst_2 : Algebra R S] → [Algebra.EssFiniteType R S] → Subalgebra R S
-- Init.Data.Nat.Internal.Linear
Nat.Internal.Linear.Poly.denote_eq.eq_1 : ∀ (ctx : Nat.Internal.Linear.Context) (mp : Nat.Internal.Linear.Poly × Nat.Internal.Linear.Poly),
  Nat.Internal.Linear.Poly.denote_eq ctx mp =
    (Nat.Internal.Linear.Poly.denote ctx mp.1 = Nat.Internal.Linear.Poly.denote ctx mp.2)
-- Mathlib.Data.FunLike.Group
FunLike.rightCancelMonoid.eq_1 : ∀ {F : Type u_1} {α : Type u_2} {β : Type u_3} [inst : FunLike F α β] [inst_1 : Mul F] [inst_2 : One F]
  [inst_3 : Pow F ℕ] [inst_4 : RightCancelMonoid β] [inst_5 : IsOneApply F α β] [inst_6 : IsMulApply F α β]
  [inst_7 : IsPowApply ℕ F α β], FunLike.rightCancelMonoid = Function.Injective.rightCancelMonoid (fun f => ⇑f) ⋯ ⋯ ⋯ ⋯
-- Mathlib.LinearAlgebra.BilinearForm.Properties
/-- Polarization identity: a symmetric bilinear form can be expressed through the values
it takes on the diagonal.  -/
LinearMap.BilinForm.IsSymm.polarization : ∀ {M : Type u_2} [inst : AddCommMonoid M] {R : Type u_8} [inst_1 : Field R] [NeZero 2] [inst_3 : Module R M]
  {B : LinearMap.BilinForm R M} (x y : M), B.IsSymm → (B x) y = ((B (x + y)) (x + y) - (B x) x - (B y) y) / 2
-- Mathlib.Topology.Semicontinuity.Hemicontinuity
/-- **Alias** of the reverse direction of `upperHemicontinuousOn_singleton_iff`. -/
ContinuousOn.upperHemicontinuousOn : ∀ {α : Type u_1} {β : Type u_2} [inst : TopologicalSpace α] [inst_1 : TopologicalSpace β] {f : α → β} {s : Set α},
  ContinuousOn f s → UpperHemicontinuousOn (fun x => {f x}) s
-- Mathlib.Geometry.Euclidean.Projection
/-- Since both instance arguments are propositions, allow `simp` to rewrite them
alongside the `s` argument.

Note that without the coercion to `P`, the LHS and RHS would have different types.  -/
EuclideanGeometry.orthogonalProjection_congr : ∀ {𝕜 : Type u_1} {V : Type u_2} {P : Type u_3} [inst : RCLike 𝕜] [inst_1 : NormedAddCommGroup V]
  [inst_2 : InnerProductSpace 𝕜 V] [inst_3 : MetricSpace P] [inst_4 : NormedAddTorsor V P] {s₁ s₂ : AffineSubspace 𝕜 P}
  {p₁ p₂ : P} [inst_5 : Nonempty ↥s₁] [inst_6 : s₁.direction.HasOrthogonalProjection] (h : s₁ = s₂),
  p₁ = p₂ → ↑((EuclideanGeometry.orthogonalProjection s₁) p₁) = ↑((EuclideanGeometry.orthogonalProjection s₂) p₂)
-- Mathlib.AlgebraicTopology.FundamentalGroupoid.SimplyConnected
simply_connected_iff_unique_homotopic : ∀ (X : Type u_3) [inst : TopologicalSpace X],
  SimplyConnectedSpace X ↔ Nonempty X ∧ ∀ (x y : X), Nonempty (Unique (Path.Homotopic.Quotient x y))
-- Mathlib.CategoryTheory.Bicategory.LocallyGroupoid
CategoryTheory.Bicategory.Pith.mk.sizeOf_spec : ∀ {B : Type u₁} [inst : SizeOf B] (as : B), sizeOf { as := as } = 1 + sizeOf as
-- Mathlib.RingTheory.Ideal.Operations
Ideal.multiset_prod_span_singleton : ∀ {R : Type u} [inst : CommSemiring R] (m : Multiset R),
  (Multiset.map (fun x => Ideal.span {x}) m).prod = Ideal.span {m.prod}
-- Mathlib.Algebra.Order.Rearrangement
/-- **Rearrangement Inequality**: Pointwise scalar multiplication of `f` and `g` is maximized when
`f` and `g` monovary together. Stated by permuting the entries of `g`.  -/
Monovary.sum_smul_comp_perm_le_sum_smul : ∀ {ι : Type u_1} {α : Type u_2} {β : Type u_3} [inst : Semiring α] [inst_1 : LinearOrder α] [IsStrictOrderedRing α]
  [ExistsAddOfLE α] [inst_4 : AddCommMonoid β] [inst_5 : LinearOrder β] [IsOrderedCancelAddMonoid β]
  [inst_7 : Module α β] [PosSMulMono α β] {σ : Equiv.Perm ι} {f : ι → α} {g : ι → β} [inst_9 : Fintype ι],
  Monovary f g → ∑ i, f i • g (σ i) ≤ ∑ i, f i • g i
-- Mathlib.AlgebraicTopology.SimplicialSet.CompStruct
/-- Maps an inverse along an morphism of simplicial sets.  -/
SSet.Edge.InvStruct.map : {X Y : SSet} →
  {x₀ x₁ : X.obj (Opposite.op { len := 0 })} →
    {hom : SSet.Edge x₀ x₁} → hom.InvStruct → (f : X ⟶ Y) → (hom.map f).InvStruct
-- Mathlib.Combinatorics.Enumerative.Partition.Glaisher
/-- The generating function of `Nat.Partition.countRestricted n m` is
$$
\prod_{i = 1}^{\infty} \sum_{j = 0}^{m - 1} X^{ij}
$$  -/
Nat.Partition.hasProd_powerSeriesMk_card_countRestricted : ∀ (R : Type u_1) [inst : TopologicalSpace R] [T2Space R] [inst_2 : CommSemiring R] {m : ℕ},
  0 < m →
    HasProd (fun i => ∑ j ∈ Finset.range m, PowerSeries.X ^ ((i + 1) * j))
      (PowerSeries.mk fun n => ↑(Nat.Partition.countRestricted n m).card)
-- Mathlib.CategoryTheory.WithTerminal.Basic
/-- Composition of morphisms for `WithTerminal C`.  -/
CategoryTheory.WithTerminal.comp : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] → {X Y Z : CategoryTheory.WithTerminal C} → X.Hom Y → Y.Hom Z → X.Hom Z
-- Mathlib.Geometry.Euclidean.Angle.Oriented.Basic
Complex.oangle : ∀ (w z : ℂ), Complex.orientation.oangle w z = ↑((starRingEnd ℂ) w * z).arg
-- Mathlib.Data.Fintype.Order
Finite.le_ciSup : ∀ {α : Type u_1} {ι : Type u_2} [Finite ι] [inst : ConditionallyCompleteLattice α] (f : ι → α) (i : ι), f i ≤ ⨆ j, f j
-- Std.Data.DHashMap.RawLemmas
Std.DHashMap.Raw.get_insert : ∀ {α : Type u} {β : α → Type v} {m : Std.DHashMap.Raw α β} [inst : BEq α] [inst_1 : Hashable α] [inst_2 : LawfulBEq α]
  (h : m.WF) {k a : α} {v : β k} {h₁ : a ∈ m.insert k v},
  (m.insert k v).get a h₁ = if h₂ : (k == a) = true then cast ⋯ v else m.get a ⋯
-- Init.Omega.IntList
Lean.Omega.IntList.add_def : ∀ (xs ys : Lean.Omega.IntList), xs + ys = List.zipWithAll (fun x y => x.getD 0 + y.getD 0) xs ys
-- Mathlib.CategoryTheory.Sites.Localization
CategoryTheory.GrothendieckTopology.W_iff_isIso_map_of_adjunction : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] (J : CategoryTheory.GrothendieckTopology C)
  {A : Type u_2} [inst_1 : CategoryTheory.Category.{v_2, u_2} A]
  {G : CategoryTheory.Functor (CategoryTheory.Functor Cᵒᵖ A) (CategoryTheory.Sheaf J A)}
  (adj : G ⊣ CategoryTheory.sheafToPresheaf J A) {P₁ P₂ : CategoryTheory.Functor Cᵒᵖ A} (f : P₁ ⟶ P₂),
  J.W f ↔ CategoryTheory.IsIso (G.map f)
-- Mathlib.Algebra.Homology.Embedding.TruncLE
HomologicalComplex.instIsIsoιTruncLEOfIsStrictlySupported : ∀ {ι : Type u_1} {ι' : Type u_2} {c : ComplexShape ι} {c' : ComplexShape ι'} {C : Type u_3}
  [inst : CategoryTheory.Category.{v_1, u_3} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  (K : HomologicalComplex C c') (e : c.Embedding c') [inst_2 : e.IsTruncLE] [inst_3 : ∀ (i' : ι'), K.HasHomology i']
  [inst_4 : CategoryTheory.Limits.HasZeroObject C] [K.IsStrictlySupported e], CategoryTheory.IsIso (K.ιTruncLE e)
-- Mathlib.Algebra.CharP.MixedCharZero
/-- Not mixed characteristic implies equal characteristic.  -/
_private.Mathlib.Algebra.CharP.MixedCharZero.0.EqualCharZero.of_not_mixedCharZero : ∀ (R : Type u_1) [inst : CommRing R] [CharZero R],
  (∀ p > 0, ¬MixedCharZero R p) → ∀ (I : Ideal R), I ≠ ⊤ → CharZero (R ⧸ I)
-- Lean.Attributes
Lean.instInhabitedTagAttribute.default : Lean.TagAttribute
-- Mathlib.Algebra.GroupWithZero.Action.Defs
smul_ne_zero_iff_ne : ∀ {α : Type u_10} {β : Type u_11} [inst : Group α] [inst_1 : AddMonoid β] [inst_2 : DistribMulAction α β] (a : α)
  {x : β}, a • x ≠ 0 ↔ x ≠ 0
-- Aesop.Script.CtorNames
Aesop.ctorNamesToInductionAlts : Array (Aesop.CtorNames × Array Lean.Syntax.Tactic) → Lean.TSyntax `Lean.Parser.Tactic.inductionAlts
-- Lean.Compiler.IR.Basic
Lean.IR.AlphaEqv.aeqv : {α : Type} → [self : Lean.IR.AlphaEqv α] → Lean.IR.IndexRenaming → α → α → Bool
-- Mathlib.Algebra.Order.Monoid.LocallyFiniteOrder
LocallyFiniteOrder.orderAddMonoidHom.eq_1 : ∀ (G : Type u_2) [inst : AddCommGroup G] [inst_1 : LinearOrder G] [inst_2 : IsOrderedAddMonoid G]
  [inst_3 : LocallyFiniteOrder G],
  LocallyFiniteOrder.orderAddMonoidHom G = { toAddMonoidHom := LocallyFiniteOrder.addMonoidHom G, monotone' := ⋯ }
-- Std.Data.Iterators.Combinators.Monadic.TakeWhile
Std.Iterators.Types.TakeWhile.PlausibleStep.yield : ∀ {α : Type w} {m : Type w → Type w'} {β : Type w} [inst : Std.Iterator α m β]
  {P : β → Std.Iterators.PostconditionT m (ULift.{w, 0} Bool)} {it : Std.IterM m β} {it' : Std.IterM m β} {out : β},
  it.internalState.inner.IsPlausibleStep (Std.IterStep.yield it' out) →
    (P out).Property { down := true } →
      Std.Iterators.Types.TakeWhile.PlausibleStep it
        (Std.IterStep.yield (Std.IterM.takeWhileWithPostcondition P it') out)
-- Mathlib.MeasureTheory.Function.L1Space.Integrable
MeasureTheory.integrable_withDensity_iff_integrable_coe_smul : ∀ {α : Type u_1} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} {E : Type u_8} [inst : NormedAddCommGroup E]
  [inst_1 : NormedSpace ℝ E] {f : α → NNReal},
  Measurable f →
    ∀ {g : α → E},
      MeasureTheory.Integrable g (μ.withDensity fun x => ↑(f x)) ↔ MeasureTheory.Integrable (fun x => ↑(f x) • g x) μ
-- Mathlib.Algebra.Homology.HomologicalComplex
HomologicalComplex.dFrom_comp_xNextIso : ∀ {ι : Type u_1} {V : Type u} [inst : CategoryTheory.Category.{v, u} V]
  [inst_1 : CategoryTheory.Limits.HasZeroMorphisms V] {c : ComplexShape ι} (C : HomologicalComplex V c) {i j : ι}
  (r : c.Rel i j), CategoryTheory.CategoryStruct.comp (C.dFrom i) (C.xNextIso r).hom = C.d i j
-- Mathlib.RingTheory.Bialgebra.MonoidAlgebra
MonoidAlgebra.mapDomainBialgHom_mul : ∀ {R : Type u_1} {M : Type u_8} {N : Type u_9} [inst : CommSemiring R] [inst_1 : CommMonoid M] [inst_2 : CommMonoid N]
  (f g : M →* N),
  MonoidAlgebra.mapDomainBialgHom R (f * g) =
    (WithConv.toConv (MonoidAlgebra.mapDomainBialgHom R f) *
        WithConv.toConv (MonoidAlgebra.mapDomainBialgHom R g)).ofConv
-- Mathlib.CategoryTheory.Monoidal.Opposite.Mon
MonObj.mopEquiv_inverse_obj_mon_mul : ∀ (C : Type u_1) [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.MonoidalCategory C]
  (M : CategoryTheory.Mon Cᴹᵒᵖ), CategoryTheory.MonObj.mul = CategoryTheory.MonObj.mul.unmop
-- Mathlib.GroupTheory.Coxeter.Basic
/-- The universal mapping property of Coxeter systems. For any monoid `G`,
functions `f : B → G` whose values satisfy the Coxeter relations are equivalent to
monoid homomorphisms `f' : W → G`.  -/
CoxeterSystem.lift : {B : Type u_1} →
  {W : Type u_3} →
    [inst : Group W] →
      {M : CoxeterMatrix B} →
        CoxeterSystem M W → {G : Type u_5} → [inst_1 : Monoid G] → { f // M.IsLiftable f } ≃ (W →* G)
-- Mathlib.GroupTheory.GroupAction.Quotient
AddAction.ofQuotientStabilizer_vadd : ∀ (G : Type u) {X : Type v} [inst : AddGroup G] [inst_1 : AddAction G X] (x : X) (g : G)
  (g' : G ⧸ AddAction.stabilizer G x),
  AddAction.ofQuotientStabilizer G x (g +ᵥ g') = g +ᵥ AddAction.ofQuotientStabilizer G x g'
-- Mathlib.RingTheory.AdjoinRoot
AdjoinRoot.instDecidableEq : {R : Type u_1} → [inst : CommRing R] → (f : Polynomial R) → DecidableEq (AdjoinRoot f)
-- Mathlib.SetTheory.ZFC.PSet
PSet.lift_mem_embed : ∀ (x : PSet.{u}), x.Lift ∈ PSet.embed
-- Mathlib.Topology.Algebra.Group.Basic
continuous_sub_right : ∀ {G : Type w} [inst : TopologicalSpace G] [inst_1 : Sub G] [ContinuousSub G] (a : G), Continuous fun x => x - a
-- Mathlib.Topology.Algebra.InfiniteSum.Group
HasProd.hasProd_iff_compl : ∀ {α : Type u_1} {β : Type u_2} [inst : CommGroup α] [inst_1 : TopologicalSpace α] [IsTopologicalGroup α] {f : β → α}
  {a₁ a₂ : α} {s : Set β}, HasProd (f ∘ Subtype.val) a₁ → (HasProd f a₂ ↔ HasProd (f ∘ Subtype.val) (a₂ / a₁))
-- Mathlib.AlgebraicGeometry.Noetherian
AlgebraicGeometry.instIsLocallyNoetherianSpecOfIsNoetherianRingCarrier : ∀ {R : CommRingCat} [IsNoetherianRing ↑R], AlgebraicGeometry.IsLocallyNoetherian (AlgebraicGeometry.Spec R)
-- Mathlib.Algebra.Group.Fin.Tuple
Matrix.tail_sub : ∀ {α : Type u_1} {n : ℕ} [inst : Sub α] (a b : Fin n.succ → α),
  Matrix.vecTail (a - b) = Matrix.vecTail a - Matrix.vecTail b
-- Init.Data.Array.OfFn
/-- Construct (in a monadic context) an array by applying a monadic function to each index.  -/
Array.ofFnM : {m : Type u_1 → Type u_2} → {α : Type u_1} → {n : ℕ} → [Monad m] → (Fin n → m α) → m (Array α)
-- Mathlib.CategoryTheory.Monoidal.Mod
/-- **Alias** of `CategoryTheory.Mod.Hom`.

---

A morphism of module objects.  -/
CategoryTheory.Mod_.Hom : {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.MonoidalLeftAction C D] →
            {A : C} → [inst_4 : CategoryTheory.MonObj A] → CategoryTheory.Mod D A → CategoryTheory.Mod D A → Type v₂
-- Mathlib.CategoryTheory.Bicategory.Functor.Pseudofunctor
CategoryTheory.Pseudofunctor.mapComp_id_left_inv_assoc : ∀ {B : Type u₁} [inst : CategoryTheory.Bicategory B] {C : Type u₂} [inst_1 : CategoryTheory.Bicategory C]
  (F : CategoryTheory.Pseudofunctor B C) {a b : B} (f : a ⟶ b) {Z : F.obj a ⟶ F.obj b}
  (h : F.map (CategoryTheory.CategoryStruct.comp (CategoryTheory.CategoryStruct.id a) f) ⟶ Z),
  CategoryTheory.CategoryStruct.comp (F.mapComp (CategoryTheory.CategoryStruct.id a) f).inv h =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.whiskerRight (F.mapId a).hom (F.map f))
      (CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.leftUnitor (F.map f)).hom
        (CategoryTheory.CategoryStruct.comp (F.map₂ (CategoryTheory.Bicategory.leftUnitor f).inv) h))