mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Combinatorics.Matroid.Minor.Contract
/-- **Alias** of `Matroid.delete_contract_eq_sdiff`. -/
Matroid.delete_contract_eq_diff : ∀ {α : Type u_1} (M : Matroid α) (D C : Set α), (M.delete D).contract C = (M.delete D).contract (C \ D)
-- Mathlib.Computability.TuringMachine.ToPartrec
Turing.PartrecToTM2.supports_insert : ∀ {K S : Finset Turing.PartrecToTM2.Λ'} {q : Turing.PartrecToTM2.Λ'},
  Turing.PartrecToTM2.Supports (insert q K) S ↔
    Turing.TM2.SupportsStmt S (Turing.PartrecToTM2.tr q) ∧ Turing.PartrecToTM2.Supports K S
-- Init.Data.Range.Basic
Std.Legacy.Range.step_pos : ∀ (self : Std.Legacy.Range), 0 < self.step
-- Init.Data.UInt.Lemmas
instAssociativeUInt32HAdd : Std.Associative fun x1 x2 => x1 + x2
-- Mathlib.NumberTheory.NumberField.Units.DirichletTheorem
_private.Mathlib.NumberTheory.NumberField.Units.DirichletTheorem.0.NumberField.Units.dirichletUnitTheorem.seq.match_1.splitter : (motive : ℕ → Sort u_1) → (x : ℕ) → (Unit → motive 0) → ((n : ℕ) → motive n.succ) → motive x
-- Mathlib.Topology.Bases
TopologicalSpace.instSecondCountableTopologyOfCountableOfFirstCountableTopology : ∀ (α : Type u) [t : TopologicalSpace α] [Countable α] [FirstCountableTopology α], SecondCountableTopology α
-- Mathlib.Util.AtLocation
Mathlib.Tactic.instBEqBehaviorIfUnchanged : BEq Mathlib.Tactic.BehaviorIfUnchanged
-- Std.Sat.AIG.Basic
Std.Sat.AIG.mk.inj : ∀ {α : Type} {inst : DecidableEq α} {inst_1 : Hashable α} {decls : Array (Std.Sat.AIG.Decl α)}
  {cache : Std.Sat.AIG.Cache α decls} {hdag : Std.Sat.AIG.IsDAG α decls} {hzero : 0 < decls.size}
  {hconst : decls[0] = Std.Sat.AIG.Decl.false} {decls_1 : Array (Std.Sat.AIG.Decl α)}
  {cache_1 : Std.Sat.AIG.Cache α decls_1} {hdag_1 : Std.Sat.AIG.IsDAG α decls_1} {hzero_1 : 0 < decls_1.size}
  {hconst_1 : decls_1[0] = Std.Sat.AIG.Decl.false},
  { decls := decls, cache := cache, hdag := hdag, hzero := hzero, hconst := hconst } =
      { decls := decls_1, cache := cache_1, hdag := hdag_1, hzero := hzero_1, hconst := hconst_1 } →
    decls = decls_1 ∧ cache ≍ cache_1
-- Mathlib.Analysis.Convex.Intrinsic
closure_sdiff_intrinsicInterior : ∀ {𝕜 : Type u_1} {V : Type u_2} {P : Type u_5} [inst : NontriviallyNormedField 𝕜] [CompleteSpace 𝕜]
  [inst_2 : NormedAddCommGroup V] [inst_3 : NormedSpace 𝕜 V] [FiniteDimensional 𝕜 V] [inst_5 : MetricSpace P]
  [inst_6 : NormedAddTorsor V P] (s : Set P), closure s \ intrinsicInterior 𝕜 s = intrinsicFrontier 𝕜 s
-- Mathlib.MeasureTheory.Measure.Decomposition.Exhaustion
/-- `μ.sigmaFiniteSetWRT' ν` has maximal `ν`-measure among all measurable sets `s` with sigma-finite
`μ.restrict s`.  -/
MeasureTheory.measure_sigmaFiniteSetWRT' : ∀ {α : Type u_1} {mα : MeasurableSpace α} (μ ν : MeasureTheory.Measure α) [inst : MeasureTheory.IsFiniteMeasure ν],
  ν (μ.sigmaFiniteSetWRT' ν) = ⨆ s, ⨆ (_ : MeasurableSet s), ⨆ (_ : MeasureTheory.SigmaFinite (μ.restrict s)), ν s
-- Init.Data.BitVec.Lemmas
BitVec.clzAuxRec_eq_iff_of_getLsbD_false : ∀ {w n : ℕ} {x : BitVec w},
  (∀ (i : ℕ), n < i → x.getLsbD i = false) → (x.clzAuxRec n = BitVec.ofNat w w ↔ ∀ j ≤ n, x.getLsbD j = false)
-- Mathlib.Data.Finset.NoncommProd
Finset.noncommProd_cons : ∀ {α : Type u_3} {β : Type u_4} [inst : Monoid β] (s : Finset α) (a : α) (f : α → β) (ha : a ∉ s)
  (comm : (↑(Finset.cons a s ha)).Pairwise (Function.onFun Commute f)),
  (Finset.cons a s ha).noncommProd f comm = f a * s.noncommProd f ⋯
-- Mathlib.Data.Fintype.Card
Finset.card_lt_univ_of_notMem : ∀ {α : Type u_1} [inst : Fintype α] {s : Finset α} {x : α}, x ∉ s → s.card < Fintype.card α
-- Mathlib.AlgebraicTopology.SimplicialObject.Basic
CategoryTheory.CosimplicialObject.Truncated.whiskering_obj_map_app : ∀ (C : Type u) [inst : CategoryTheory.Category.{v, u} C] {n : ℕ} (D : Type u_1)
  [inst_1 : CategoryTheory.Category.{v_1, u_1} D] (H : CategoryTheory.Functor C D)
  {X Y : CategoryTheory.Functor (SimplexCategory.Truncated n) C} (α : X ⟶ Y) (X_1 : SimplexCategory.Truncated n),
  (((CategoryTheory.CosimplicialObject.Truncated.whiskering C D).obj H).map α).app X_1 = H.map (α.app X_1)
-- Mathlib.Topology.Sets.Closeds
TopologicalSpace.Closeds.coe_eq_univ : ∀ {α : Type u_2} [inst : TopologicalSpace α] {s : TopologicalSpace.Closeds α}, ↑s = Set.univ ↔ s = ⊤
-- Mathlib.Analysis.Asymptotics.AsymptoticEquivalent
Asymptotics.IsEquivalent.const_add_of_norm_tendsto_atTop : ∀ {α : Type u_1} {β : Type u_2} [inst : NormedAddCommGroup β] {u v : α → β} {l : Filter α} {c : β},
  Asymptotics.IsEquivalent l u v →
    Filter.Tendsto (norm ∘ v) l Filter.atTop → Asymptotics.IsEquivalent l (fun x => c + u x) v
-- Mathlib.NumberTheory.NumberField.Units.Regulator
/-- Let `u : Fin (rank K) → (𝓞 K)ˣ` be a family of units and let `w₁` and `w₂` be two infinite
places. Then, the two square matrices with entries `(mult w * log w (u i))_i` where `w ≠ w_j` for
`j = 1, 2` have the same determinant in absolute value.
 -/
NumberField.Units.abs_det_eq_abs_det : ∀ {K : Type u_1} [inst : Field K] [inst_1 : NumberField K]
  (u : Fin (NumberField.Units.rank K) → (NumberField.RingOfIntegers K)ˣ) {w₁ w₂ : NumberField.InfinitePlace K}
  (e₁ : { w // w ≠ w₁ } ≃ Fin (NumberField.Units.rank K)) (e₂ : { w // w ≠ w₂ } ≃ Fin (NumberField.Units.rank K)),
  |(Matrix.of fun i w => ↑(↑w).mult * Real.log (↑w ((algebraMap (NumberField.RingOfIntegers K) K) ↑(u (e₁ i))))).det| =
    |(Matrix.of fun i w => ↑(↑w).mult * Real.log (↑w ((algebraMap (NumberField.RingOfIntegers K) K) ↑(u (e₂ i))))).det|
-- Mathlib.Algebra.ContinuedFractions.Basic
/-- Returns the convergents `Aₙ / Bₙ` of `g`, where `Aₙ, Bₙ` are the nth continuants of `g`.  -/
GenContFract.convs : {K : Type u_2} → [DivisionRing K] → GenContFract K → Stream' K
-- Init.Data.Fin.Lemmas
Fin.lt_iff_val_lt_val : ∀ {n : ℕ} {a b : Fin n}, a < b ↔ ↑a < ↑b
-- Mathlib.MeasureTheory.MeasurableSpace.CountablyGenerated
MeasurableSpace.countablePartitionSet_of_mem : ∀ {α : Type u_1} [m : MeasurableSpace α] [h : MeasurableSpace.CountablyGenerated α] {n : ℕ} {a : α} {s : Set α},
  s ∈ MeasurableSpace.countablePartition α n → a ∈ s → MeasurableSpace.countablePartitionSet n a = s
-- Mathlib.CategoryTheory.Bicategory.Functor.LocallyDiscrete
CategoryTheory.Functor.toPseudofunctor'_map : ∀ {I : Type u_1} {B : Type u_2} [inst : CategoryTheory.Category.{v_1, u_1} I] [inst_1 : CategoryTheory.Bicategory B]
  [inst_2 : CategoryTheory.Bicategory.Strict B] (F : CategoryTheory.Functor I B)
  {X Y : CategoryTheory.LocallyDiscrete I} (x : X ⟶ Y),
  F.toPseudofunctor'.map x =
    match x with
    | { as := f } => F.map f
-- Std.Data.DHashMap.Internal.Defs
/-- Internal implementation detail of the hash map  -/
Std.DHashMap.Internal.toListModel : {α : Type u} → {β : α → Type v} → Array (Std.DHashMap.Internal.AssocList α β) → List ((a : α) × β a)
-- Mathlib.GroupTheory.OreLocalization.Basic
_private.Mathlib.GroupTheory.OreLocalization.Basic.0.AddOreLocalization.vadd'.eq_1 : ∀ {R : Type u_1} [inst : AddMonoid R] {S : AddSubmonoid R} [inst_1 : AddOreLocalization.AddOreSet S] {X : Type u_2}
  [inst_2 : AddAction R X] (r₁ : R) (s₁ : ↥S) (r₂ : X) (s₂ : ↥S),
  AddOreLocalization.vadd'✝ r₁ s₁ r₂ s₂ =
    (AddOreLocalization.oreMin r₁ s₂ +ᵥ r₂) -ₒ (AddOreLocalization.oreSubtra r₁ s₂ + s₁)
-- Init.Data.Array.Subarray
/-- The empty subarray.

This empty subarray is backed by an empty array.
 -/
Subarray.empty : {α : Type u_1} → Subarray α
-- Mathlib.CategoryTheory.Monad.Basic
/-- The data of a monad on C consists of an endofunctor T together with natural transformations
`η : 𝟭 C ⟶ T` and `μ : T ⋙ T ⟶ T` satisfying three equations:
- `T μ_X ≫ μ_X = μ_(TX) ≫ μ_X` (associativity)
- `η_(TX) ≫ μ_X = 1_X` (left unit)
- `Tη_X ≫ μ_X = 1_X` (right unit)
 -/
CategoryTheory.Monad : (C : Type u₁) → [CategoryTheory.Category.{v₁, u₁} C] → Type (max u₁ v₁)
-- Std.Time.Date.Unit.Weekday
Std.Time.Weekday.wednesday.sizeOf_spec : sizeOf Std.Time.Weekday.wednesday = 1
-- Mathlib.CategoryTheory.Iso
CategoryTheory.Iso.comp_inv_eq_id : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {X Y : C} (α : X ≅ Y) {f : X ⟶ Y},
  CategoryTheory.CategoryStruct.comp f α.inv = CategoryTheory.CategoryStruct.id X ↔ f = α.hom
-- Mathlib.Topology.Algebra.Algebra
ContinuousAlgHom.one_apply : ∀ (R : Type u_1) [inst : CommSemiring R] (A : Type u_2) [inst_1 : Semiring A] [inst_2 : TopologicalSpace A]
  [inst_3 : Algebra R A] (x : A), 1 x = x
-- Mathlib.Topology.Algebra.ContinuousAffineMap
ContinuousAffineMap.snd_decompEquiv : ∀ (R : Type u_1) (V : Type u_3) {W : Type u_4} (Q : Type u_5) [inst : Ring R] [inst_1 : AddCommGroup V]
  [inst_2 : Module R V] [inst_3 : TopologicalSpace V] [inst_4 : IsTopologicalAddGroup V] [inst_5 : AddCommGroup W]
  [inst_6 : Module R W] [inst_7 : TopologicalSpace W] [inst_8 : AddTorsor W Q] [inst_9 : TopologicalSpace Q]
  [inst_10 : IsTopologicalAddTorsor Q] (f : V →ᴬ[R] Q), ((ContinuousAffineMap.decompEquiv R V Q) f).2 = f.contLinear
-- Std.Http.Data.Body.Basic
Std.Http.Body.ToByteArray.mk : {α : Type} → (α → ByteArray) → Std.Http.Body.ToByteArray α
-- Mathlib.CategoryTheory.Products.Basic
/-- `CategoryStruct.prod C D` gives the Cartesian product of two `CategoryStruct`'s.  -/
CategoryTheory.prod : (C : Type u₁) →
  [CategoryTheory.CategoryStruct.{v₁, u₁} C] →
    (D : Type u₂) →
      [CategoryTheory.CategoryStruct.{v₂, u₂} D] → CategoryTheory.CategoryStruct.{max v₁ v₂, max u₂ u₁} (C × D)
-- Mathlib.Order.SuccPred.Basic
/-- A well-order is a `SuccOrder`.  -/
SuccOrder.ofLinearWellFoundedLT : (α : Type u_1) → [inst : LinearOrder α] → [WellFoundedLT α] → SuccOrder α
-- Lean.Data.Lsp.TextSync
Lean.Lsp.SaveOptions.mk.injEq : ∀ (includeText includeText_1 : Bool),
  ({ includeText := includeText } = { includeText := includeText_1 }) = (includeText = includeText_1)
-- Mathlib.Data.Set.Operations
/-- `f` is surjective from `s` to `t` if `t` is contained in the image of `s`.  -/
Set.SurjOn : {α : Type u} → {β : Type v} → (α → β) → Set α → Set β → Prop
-- Mathlib.Data.PFunctor.Univariate.M
_private.Mathlib.Data.PFunctor.Univariate.M.0.PFunctor.Approx.truncate.match_1.eq_2 : ∀ {F : PFunctor.{u_1, u_2}} (motive : (x : ℕ) → PFunctor.Approx.CofixA F (x + 1) → Sort u_3) (a : ℕ) (i : F.A)
  (f : F.B i → PFunctor.Approx.CofixA F (a + 1))
  (h_1 : (a : F.A) → (a_1 : F.B a → PFunctor.Approx.CofixA F 0) → motive 0 (PFunctor.Approx.CofixA.intro a a_1))
  (h_2 :
    (a : ℕ) →
      (i : F.A) → (f : F.B i → PFunctor.Approx.CofixA F (a + 1)) → motive a.succ (PFunctor.Approx.CofixA.intro i f)),
  (match a.succ, PFunctor.Approx.CofixA.intro i f with
    | 0, PFunctor.Approx.CofixA.intro a a_1 => h_1 a a_1
    | a.succ, PFunctor.Approx.CofixA.intro i f => h_2 a i f) =
    h_2 a i f
-- Mathlib.CategoryTheory.Abelian.SerreClass.MorphismProperty
CategoryTheory.ObjectProperty.monoModSerre.congr_simp : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Abelian C]
  (P P_1 : CategoryTheory.ObjectProperty C) (e_P : P = P_1) [inst_2 : P.IsSerreClass] ⦃X Y : C⦄ (x x_1 : X ⟶ Y),
  x = x_1 → P.monoModSerre x = P_1.monoModSerre x_1
-- Mathlib.Algebra.Star.StarAlgHom
StarAlgHom.coe_toNonUnitalStarAlgHom : ∀ {R : Type u_2} {A : Type u_3} {B : Type u_4} [inst : CommSemiring R] [inst_1 : Semiring A] [inst_2 : Algebra R A]
  [inst_3 : Star A] [inst_4 : Semiring B] [inst_5 : Algebra R B] [inst_6 : Star B] (f : A →⋆ₐ[R] B),
  ⇑f.toNonUnitalStarAlgHom = ⇑f
-- Init.Data.Float.Float32
/-- Computes the exponential `e^x` of a floating-point number.

This function does not reduce in the kernel. It is implemented in compiled code by the C function
`expf`.
 -/
Float32.exp : Float32 → Float32
-- Std.Data.ExtTreeSet.Lemmas
Std.ExtTreeSet.get?_union : ∀ {α : Type u} {cmp : α → α → Ordering} {t₁ t₂ : Std.ExtTreeSet α cmp} [inst : Std.TransCmp cmp] {k : α},
  (t₁ ∪ t₂).get? k = (t₂.get? k).or (t₁.get? k)
-- Mathlib.Analysis.Normed.Affine.Isometry
AffineIsometryEquiv.symm_trans_self : ∀ {𝕜 : Type u_1} {V : Type u_2} {V₂ : Type u_5} {P : Type u_10} {P₂ : Type u_11} [inst : NormedField 𝕜]
  [inst_1 : SeminormedAddCommGroup V] [inst_2 : NormedSpace 𝕜 V] [inst_3 : PseudoMetricSpace P]
  [inst_4 : NormedAddTorsor V P] [inst_5 : SeminormedAddCommGroup V₂] [inst_6 : NormedSpace 𝕜 V₂]
  [inst_7 : PseudoMetricSpace P₂] [inst_8 : NormedAddTorsor V₂ P₂] (e : P ≃ᵃⁱ[𝕜] P₂),
  e.symm.trans e = AffineIsometryEquiv.refl 𝕜 P₂
-- Mathlib.NumberTheory.Real.Irrational
Irrational.of_natCast_sub : ∀ {x : ℝ} (m : ℕ), Irrational (↑m - x) → Irrational x
-- Mathlib.LinearAlgebra.AffineSpace.FiniteDimensional
/-- If the `affineSpan` of a finite subset of an affinely independent
family lies in an affine subspace whose direction has dimension one
less than its cardinality, it equals that subspace.  -/
AffineIndependent.affineSpan_image_finset_eq_of_le_of_card_eq_finrank_add_one : ∀ {k : Type u_1} {V : Type u_2} {P : Type u_3} {ι : Type u_4} [inst : DivisionRing k] [inst_1 : AddCommGroup V]
  [inst_2 : Module k V] [inst_3 : AddTorsor V P] [inst_4 : DecidableEq P] {p : ι → P},
  AffineIndependent k p →
    ∀ {s : Finset ι} {sp : AffineSubspace k P} [FiniteDimensional k ↥sp.direction],
      affineSpan k ↑(Finset.image p s) ≤ sp →
        s.card = Module.finrank k ↥sp.direction + 1 → affineSpan k ↑(Finset.image p s) = sp
-- Std.Http.Data.Chunk
/-- Retrieves all values for the given trailer header name.
Returns `none` if absent.
 -/
Std.Http.Trailer.getAll? : Std.Http.Trailer → Std.Http.Header.Name → Option (Array Std.Http.Header.Value)
-- Mathlib.Order.Hom.CompleteLattice
/-- `id` as a `sSupHom`.  -/
sSupHom.id : (α : Type u_2) → [inst : SupSet α] → sSupHom α α
-- Mathlib.Geometry.Manifold.VectorBundle.Basic
ContMDiffVectorBundle.contMDiffOn_coordChangeL : ∀ {n : WithTop ℕ∞} {𝕜 : Type u_1} {B : Type u_2} {F : Type u_4} {E : B → Type u_6} {inst : NontriviallyNormedField 𝕜}
  {EB : Type u_7} {inst_1 : NormedAddCommGroup EB} {inst_2 : NormedSpace 𝕜 EB} {HB : Type u_8}
  {inst_3 : TopologicalSpace HB} {IB : ModelWithCorners 𝕜 EB HB} {inst_4 : TopologicalSpace B}
  {inst_5 : ChartedSpace HB B} {inst_6 : (x : B) → AddCommMonoid (E x)} {inst_7 : (x : B) → Module 𝕜 (E x)}
  {inst_8 : NormedAddCommGroup F} {inst_9 : NormedSpace 𝕜 F} {inst_10 : TopologicalSpace (Bundle.TotalSpace F E)}
  {inst_11 : (x : B) → TopologicalSpace (E x)} {inst_12 : FiberBundle F E} {inst_13 : VectorBundle 𝕜 F E}
  [self : ContMDiffVectorBundle n F E IB] (e e' : Bundle.Trivialization F Bundle.TotalSpace.proj)
  [inst_14 : MemTrivializationAtlas e] [inst_15 : MemTrivializationAtlas e'],
  ContMDiffOn IB (modelWithCornersSelf 𝕜 (F →L[𝕜] F)) n (fun b => ↑(Bundle.Trivialization.coordChangeL 𝕜 e e' b))
    (e.baseSet ∩ e'.baseSet)
-- Std.Do.Internal.Ensures.Def
/-- `Ensures p x` says every value returned by `x` satisfies `p`. The witness is a
`Subtype`-refined monadic action that is bind-faithful w.r.t. `x`.  -/
Std.Do.Internal.Ensures : {m : Type u → Type v} → [Bind m] → {α : Type u} → (α → Prop) → m α → Prop
-- Mathlib.CategoryTheory.Limits.Shapes.Multiequalizer
_private.Mathlib.CategoryTheory.Limits.Shapes.Multiequalizer.0.CategoryTheory.Limits.MultispanIndex.multispan.match_1.eq_1 : ∀ {J : CategoryTheory.Limits.MultispanShape}
  (motive : (x y : CategoryTheory.Limits.WalkingMultispan J) → (x ⟶ y) → Sort u_3)
  (x : CategoryTheory.Limits.WalkingMultispan J)
  (h_1 : (x : CategoryTheory.Limits.WalkingMultispan J) → motive x x (CategoryTheory.Limits.WalkingMultispan.Hom.id x))
  (h_2 :
    (b : J.L) →
      motive (CategoryTheory.Limits.WalkingMultispan.left b) (CategoryTheory.Limits.WalkingMultispan.right (J.fst b))
        (CategoryTheory.Limits.WalkingMultispan.Hom.fst b))
  (h_3 :
    (b : J.L) →
      motive (CategoryTheory.Limits.WalkingMultispan.left b) (CategoryTheory.Limits.WalkingMultispan.right (J.snd b))
        (CategoryTheory.Limits.WalkingMultispan.Hom.snd b)),
  (match x, x, CategoryTheory.Limits.WalkingMultispan.Hom.id x with
    | x, .(x), CategoryTheory.Limits.WalkingMultispan.Hom.id .(x) => h_1 x
    | .(CategoryTheory.Limits.WalkingMultispan.left b), .(CategoryTheory.Limits.WalkingMultispan.right (J.fst b)),
      CategoryTheory.Limits.WalkingMultispan.Hom.fst b => h_2 b
    | .(CategoryTheory.Limits.WalkingMultispan.left b), .(CategoryTheory.Limits.WalkingMultispan.right (J.snd b)),
      CategoryTheory.Limits.WalkingMultispan.Hom.snd b => h_3 b) =
    h_1 x
-- Mathlib.Tactic.Ring.RingNF
/-- `ring1` solves the goal when it is an equality in *commutative* (semi)rings,
allowing variables in the exponent.

This version of `ring` fails if the target is not an equality.

* `ring1!` uses a more aggressive reducibility setting to determine equality of atoms.


Extensions:

 * * `ring1_nf` additionally uses `ring_nf` to simplify in atoms.
   * `ring1_nf!` will use a more aggressive reducibility setting
     to determine equality of atoms. -/
Mathlib.Tactic.RingNF.tacticRing1_nf!_ : Lean.ParserDescr
-- Mathlib.Data.DFinsupp.NeLocus
DFinsupp.mapRange_neLocus_eq : ∀ {α : Type u_1} {N : α → Type u_2} [inst : DecidableEq α] {M : α → Type u_3} [inst_1 : (a : α) → Zero (N a)]
  [inst_2 : (a : α) → Zero (M a)] [inst_3 : (a : α) → DecidableEq (N a)] [inst_4 : (a : α) → DecidableEq (M a)]
  (f g : Π₀ (a : α), N a) {F : (a : α) → N a → M a} (F0 : ∀ (a : α), F a 0 = 0),
  (∀ (a : α), Function.Injective (F a)) → (DFinsupp.mapRange F F0 f).neLocus (DFinsupp.mapRange F F0 g) = f.neLocus g
-- Mathlib.Algebra.Order.Monoid.Unbundled.TypeTags
Multiplicative.toAdd_eq_bot : ∀ {α : Type u_1} [inst : LE α] [inst_1 : OrderBot α] {a : Multiplicative α}, Multiplicative.toAdd a = ⊥ ↔ a = ⊥
-- Mathlib.Data.Set.Pairwise.Basic
/-- **Alias** of the forward direction of `Set.injOn_iff_pairwise_ne`.

---

See also `Function.injective_iff_pairwise_ne`  -/
Set.InjOn.pairwise_ne : ∀ {α : Type u_1} {ι : Type u_4} {f : ι → α} {s : Set ι}, Set.InjOn f s → s.Pairwise fun x1 x2 => f x1 ≠ f x2
-- Mathlib.GroupTheory.QuotientGroup.Defs
QuotientAddGroup.con_mono : ∀ {G : Type u_1} [inst : AddGroup G] {N M : AddSubgroup G} [hN : N.Normal] [hM : M.Normal],
  N ≤ M → QuotientAddGroup.con N ≤ QuotientAddGroup.con M
-- Mathlib.CategoryTheory.Elements
CategoryTheory.Functor.Elements.initialOfRepresentableBy_snd : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {F : CategoryTheory.Functor Cᵒᵖ (Type u_1)} {X : C}
  (h : F.RepresentableBy X),
  (CategoryTheory.Functor.Elements.initialOfRepresentableBy h).snd = h.homEquiv (CategoryTheory.CategoryStruct.id X)
-- Mathlib.GroupTheory.Commutator.Basic
map_addCommutatorElement : ∀ {G : Type u_1} {G' : Type u_2} {F : Type u_3} [inst : AddGroup G] [inst_1 : AddGroup G'] [inst_2 : FunLike F G G']
  [AddMonoidHomClass F G G'] (f : F) (g₁ g₂ : G), f ⁅g₁, g₂⁆ = ⁅f g₁, f g₂⁆
-- Mathlib.Tactic.NormNum.Irrational
/-- Natural `k` such that `k ^ n < m < (k + 1) ^ n`.  -/
Mathlib.Meta.NormNum.NotPowerCertificate.k : {m n : Q(ℕ)} → Mathlib.Meta.NormNum.NotPowerCertificate m n → Q(ℕ)
-- Mathlib.Algebra.Order.GroupWithZero.Canonical
WithZero.instMulLeftMono : ∀ {α : Type u_1} [inst : Preorder α] [inst_1 : Mul α] [MulLeftMono α], MulLeftMono (WithZero α)
-- Batteries.Data.Array.Basic
/-- **Alias** of `Array.set`. -/
Array.setN : {α : Type u_1} → (xs : Array α) → (i : ℕ) → α → autoParam (i < xs.size) Array.set._auto_1 → Array α
-- Mathlib.Combinatorics.SimpleGraph.Connectivity.Subgraph
_private.Mathlib.Combinatorics.SimpleGraph.Connectivity.Subgraph.0.SimpleGraph.Walk.map.match_1.eq_1 : ∀ {V : Type u_1} {G : SimpleGraph V} {u : V} (motive : (v : V) → G.Walk u v → Sort u_2)
  (h_1 : Unit → motive u SimpleGraph.Walk.nil)
  (h_2 : (v v_1 : V) → (h : G.Adj u v_1) → (p : G.Walk v_1 v) → motive v (SimpleGraph.Walk.cons h p)),
  (match u, SimpleGraph.Walk.nil with
    | .(u), SimpleGraph.Walk.nil => h_1 ()
    | v, SimpleGraph.Walk.cons h p => h_2 v v_1 h p) =
    h_1 ()
-- Mathlib.Topology.Algebra.SeparationQuotient.Basic
SeparationQuotient.instInvolutiveNeg.eq_1 : ∀ {G : Type u_1} [inst : TopologicalSpace G] [inst_1 : InvolutiveNeg G] [inst_2 : ContinuousNeg G],
  SeparationQuotient.instInvolutiveNeg = Function.Surjective.involutiveNeg SeparationQuotient.mk ⋯ ⋯
-- Mathlib.LinearAlgebra.Matrix.SesquilinearForm
mem_skewAdjointMatricesSubmodule : ∀ {R : Type u_1} {n : Type u_11} [inst : CommRing R] [inst_1 : Fintype n] (J A₁ : Matrix n n R)
  [inst_2 : DecidableEq n], A₁ ∈ skewAdjointMatricesSubmodule J ↔ J.IsSkewAdjoint A₁
-- Mathlib.Order.Concept
Concept.extent_bot : ∀ {α : Type u_2} {β : Type u_3} {r : α → β → Prop}, ⊥.extent = lowerPolar r Set.univ
-- Mathlib.Algebra.Group.Pointwise.Finset.Basic
/-- **Alias** of the forward direction of `Finset.neg_nonempty_iff`. -/
Finset.Nonempty.of_neg : ∀ {α : Type u_2} [inst : DecidableEq α] [inst_1 : Neg α] {s : Finset α}, (-s).Nonempty → s.Nonempty
-- Mathlib.CategoryTheory.Limits.Types.Products
/-- A type is terminal if and only if it contains exactly one element.  -/
CategoryTheory.Limits.Types.isTerminalEquivUnique : (X : Type u) → CategoryTheory.Limits.IsTerminal X ≃ Unique X
-- Mathlib.Topology.Compactness.CompactlyGeneratedSpace
/-- In a compactly generated space `X`, a set `s` is closed when `f ⁻¹' s` is
closed for every continuous map `f : K → X`, where `K` is compact Hausdorff.  -/
UCompactlyGeneratedSpace.isClosed : ∀ {X : Type w} [tX : TopologicalSpace X] [UCompactlyGeneratedSpace X] {s : Set X},
  (∀ (S : CompHaus) (f : C(↑S.toTop, X)), IsClosed (⇑f ⁻¹' s)) → IsClosed s
-- Lean.Meta.DiscrTree.Types
Lean.Meta.DiscrTree.Trie.brecOn_2.go : {α : Type} →
  {motive_1 : Lean.Meta.DiscrTree.Trie α → Sort u} →
    {motive_2 : Array (Lean.Meta.DiscrTree.Key × Lean.Meta.DiscrTree.Trie α) → Sort u} →
      {motive_3 : List (Lean.Meta.DiscrTree.Key × Lean.Meta.DiscrTree.Trie α) → Sort u} →
        {motive_4 : Lean.Meta.DiscrTree.Key × Lean.Meta.DiscrTree.Trie α → Sort u} →
          (t : List (Lean.Meta.DiscrTree.Key × Lean.Meta.DiscrTree.Trie α)) →
            ((t : Lean.Meta.DiscrTree.Trie α) → t.below → motive_1 t) →
              ((t : Array (Lean.Meta.DiscrTree.Key × Lean.Meta.DiscrTree.Trie α)) →
                  Lean.Meta.DiscrTree.Trie.below_1 t → motive_2 t) →
                ((t : List (Lean.Meta.DiscrTree.Key × Lean.Meta.DiscrTree.Trie α)) →
                    Lean.Meta.DiscrTree.Trie.below_2 t → motive_3 t) →
                  ((t : Lean.Meta.DiscrTree.Key × Lean.Meta.DiscrTree.Trie α) →
                      Lean.Meta.DiscrTree.Trie.below_3 t → motive_4 t) →
                    motive_3 t ×' Lean.Meta.DiscrTree.Trie.below_2 t
-- Mathlib.AlgebraicTopology.ModelCategory.Cylinder
HomotopicalAlgebra.Cylinder.IsGood.mk : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {A : C}
  [inst_1 : HomotopicalAlgebra.CategoryWithWeakEquivalences C] {P : HomotopicalAlgebra.Cylinder A}
  [inst_2 : CategoryTheory.Limits.HasBinaryCoproduct A A] [inst_3 : HomotopicalAlgebra.CategoryWithCofibrations C],
  autoParam (HomotopicalAlgebra.Cofibration P.i) HomotopicalAlgebra.Cylinder.IsGood.cofibration_i._autoParam → P.IsGood
-- Mathlib.CategoryTheory.IsConnected
CategoryTheory.isPreconnected_of_isPreconnected_op : ∀ {J : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} J] [CategoryTheory.IsPreconnected Jᵒᵖ],
  CategoryTheory.IsPreconnected J
-- Std.Do.SPred.SPred
Std.Do.SPred.ext_nil : ∀ {P Q : Std.Do.SPred []}, (P.down ↔ Q.down) → P = Q
-- Mathlib.CategoryTheory.Sites.Sieves
/-- The infimum of a collection of sieves: the intersection of them all.  -/
CategoryTheory.Sieve.inf : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] → {X : C} → Set (CategoryTheory.Sieve X) → CategoryTheory.Sieve X
-- Mathlib.Probability.Independence.Conditional
ProbabilityTheory.condIndepFun_of_measurable_right : ∀ {Ω : Type u_1} {β : Type u_3} {β' : Type u_4} {m' mΩ : MeasurableSpace Ω} [inst : StandardBorelSpace Ω]
  {hm' : m' ≤ mΩ} {μ : MeasureTheory.Measure Ω} [inst_1 : MeasureTheory.IsFiniteMeasure μ] {mβ : MeasurableSpace β}
  {mβ' : MeasurableSpace β'} {X : Ω → β} {Y : Ω → β'},
  Measurable X → Measurable Y → ProbabilityTheory.CondIndepFun m' hm' X Y μ
-- Lean.Meta.Tactic.Grind.Arith.CommRing.MonadRing
Lean.Meta.Grind.Arith.CommRing.instMonadRingOfMonadOfMonadCommRing : (m : Type → Type) →
  [Monad m] → [Lean.Meta.Grind.Arith.CommRing.MonadCommRing m] → Lean.Meta.Grind.Arith.CommRing.MonadRing m
-- Init.Data.String.Lemmas.Pattern.TakeDrop.Basic
String.revAll_eq_revAll_toSlice : ∀ {ρ : Type} {pat : ρ} [inst : String.Slice.Pattern.BackwardPattern pat] {s : String},
  s.revAll pat = s.toSlice.revAll pat
-- Lean.Util.Path
Lean.getSrcSearchPath : IO Lean.SearchPath