mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.CategoryTheory.Limits.Shapes.Equalizers
CategoryTheory.Limits.WalkingParallelPairHom.right : CategoryTheory.Limits.WalkingParallelPairHom CategoryTheory.Limits.WalkingParallelPair.zero
  CategoryTheory.Limits.WalkingParallelPair.one
-- Init.Data.Array.Sort.Lemmas
Array.toList_mergeSort : ∀ {α : Type u_1} {xs : Array α} {le : α → α → Bool}, (xs.mergeSort le).toList = xs.toList.mergeSort le
-- Std.Http.Protocol.H1.Error
Std.Http.Protocol.H1.Error.other.sizeOf_spec : ∀ (message : String), sizeOf (Std.Http.Protocol.H1.Error.other message) = 1 + sizeOf message
-- Mathlib.Algebra.Group.Int.Units
Int.isUnit_eq_one_or : ∀ {u : ℤ}, IsUnit u → u = 1 ∨ u = -1
-- Mathlib.Logic.Function.Basic
Function.hfunext : ∀ {α α' : Sort u} {β : α → Sort v} {β' : α' → Sort v} {f : (a : α) → β a} {f' : (a : α') → β' a},
  α = α' → (∀ (a : α) (a' : α'), a ≍ a' → f a ≍ f' a') → f ≍ f'
-- Mathlib.Combinatorics.SimpleGraph.Dart
SimpleGraph.dart_edge_eq_iff : ∀ {V : Type u_1} {G : SimpleGraph V} (d₁ d₂ : G.Dart), d₁.edge = d₂.edge ↔ d₁ = d₂ ∨ d₁ = d₂.symm
-- Mathlib.Algebra.Group.Action.Sigma
Sigma.instSMul_mathlib.eq_1 : ∀ {ι : Type u_1} {M : Type u_2} {α : ι → Type u_4} [inst : (i : ι) → SMul M (α i)],
  Sigma.instSMul_mathlib = { smul := fun a => Sigma.map id fun x x_1 => a • x_1 }
-- Init.Data.UInt.Lemmas
UInt8.toUInt64_eq_mod_256_iff : ∀ (a : UInt8) (b : UInt64), a.toUInt64 = b % 256 ↔ a = b.toUInt8
-- Mathlib.Combinatorics.SimpleGraph.Clique
SimpleGraph.IsNClique.exists_not_adj_of_cliqueFree_succ : ∀ {α : Type u_1} {G : SimpleGraph α} {n : ℕ} {s : Finset α},
  G.IsNClique n s → G.CliqueFree (n + 1) → ∀ (x : α), ∃ y ∈ s, ¬G.Adj x y
-- Mathlib.CategoryTheory.Comma.Over.OverClass
CategoryTheory.OverClass.asOver_left : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] (X S : C) [inst_1 : CategoryTheory.OverClass X S],
  (CategoryTheory.OverClass.asOver X S).left = X
-- Init.Data.Range.Polymorphic.Lemmas
Std.Ric.mem_toList_iff_mem : ∀ {α : Type u} {r : Std.Ric α} [inst : LE α] [inst_1 : DecidableLE α] [inst_2 : Std.PRange.Least? α]
  [inst_3 : Std.PRange.UpwardEnumerable α] [inst_4 : Std.PRange.LawfulUpwardEnumerable α]
  [Std.PRange.LawfulUpwardEnumerableLE α] [Std.PRange.LawfulUpwardEnumerableLeast? α]
  [inst_7 : Std.Rxc.IsAlwaysFinite α] {a : α}, a ∈ r.toList ↔ a ∈ r
-- Init.System.CancelToken
_private.Init.System.CancelToken.0.IO.CancelToken.mk.injEq : ∀ (promise : IO.Promise Unit) (setRef : IO.Ref Bool) (promise_1 : IO.Promise Unit) (setRef_1 : IO.Ref Bool),
  ({ promise := promise, setRef := setRef } = { promise := promise_1, setRef := setRef_1 }) =
    (promise = promise_1 ∧ setRef = setRef_1)
-- Init.Data.Option.Attach
/-- Remove an attached proof that the value in an `Option` is indeed that value.

This function is usually inserted automatically by Lean, rather than explicitly in code. It is
introduced as an intermediate step during the elaboration of definitions by well-founded recursion.

If this function is encountered in a proof state, the right approach is usually the tactic
`simp [Option.unattach, -Option.map_subtype]`.

It is a synonym for `Option.map Subtype.val`.
 -/
Option.unattach : {α : Type u_1} → {p : α → Prop} → Option { x // p x } → Option α
-- Init.Data.Vector.MapIdx
Vector.getElem_mapFinIdx : ∀ {α : Type u_1} {n : ℕ} {β : Type u_2} {xs : Vector α n} {f : (i : ℕ) → α → i < n → β} {i : ℕ} (h : i < n),
  (xs.mapFinIdx f)[i] = f i xs[i] h
-- Mathlib.Analysis.SpecialFunctions.Log.Base
Real.tendsto_pow_logb_div_mul_add_atTop : ∀ {b : ℝ} (a c : ℝ) (n : ℕ), a ≠ 0 → Filter.Tendsto (fun x => Real.logb b x ^ n / (a * x + c)) Filter.atTop (nhds 0)
-- Mathlib.LinearAlgebra.Matrix.Vec
Matrix.vec_eq_uncurry : ∀ {m : Type u_1} {n : Type u_2} {R : Type u_3} (A : Matrix m n R), A.vec = Function.uncurry fun i j => A j i
-- Mathlib.Computability.TuringMachine.Computable
/-- the output alphabet is equivalent to `Γ₁`  -/
Turing.TM2ComputableAux.outputAlphabet : {Γ₀ Γ₁ : Type} → (self : Turing.TM2ComputableAux Γ₀ Γ₁) → self.tm.Γ self.tm.k₁ ≃ Γ₁
-- Std.Data.TreeMap.Raw.Lemmas
Std.TreeMap.Raw.getKey_minKey? : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Std.TreeMap.Raw α β cmp} [inst : Std.TransCmp cmp] (h : t.WF)
  {km : α} {hc : t.contains km = true}, t.minKey?.get ⋯ = km → t.getKey km hc = km
-- Mathlib.Data.List.MinMax
List.argAux.eq_1 : ∀ {α : Type u_1} (r : α → α → Prop) [inst : DecidableRel r] (a : Option α) (b : α),
  List.argAux r a b = Option.casesOn a (some b) fun c => if r b c then some b else some c
-- Mathlib.RingTheory.PowerSeries.Derivative
PowerSeries.derivativeFun_one : ∀ {R : Type u_1} [inst : CommSemiring R], PowerSeries.derivativeFun 1 = 0
-- Mathlib.CategoryTheory.Monoidal.Braided.Multifunctor
CategoryTheory.BraidedCategory.Hexagon.functor₃₁₂_obj_obj_map : ∀ (C : Type u_1) [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.MonoidalCategory C] (G k : C)
  {X Y : C} (f : X ⟶ Y),
  (((CategoryTheory.BraidedCategory.Hexagon.functor₃₁₂ C).obj G).obj k).map f =
    CategoryTheory.MonoidalCategoryStruct.whiskerRight (CategoryTheory.MonoidalCategoryStruct.whiskerRight f G) k
-- Mathlib.MeasureTheory.Group.Arithmetic
DiscreteMeasurableSpace.toMeasurableNeg : ∀ {α : Type u_1} [inst : MeasurableSpace α] [inst_1 : Neg α] [DiscreteMeasurableSpace α], MeasurableNeg α
-- Mathlib.Topology.ContinuousMap.Bounded.Normed
BoundedContinuousFunction.nnnorm_const_eq : ∀ {α : Type u} {β : Type v} [inst : TopologicalSpace α] [inst_1 : SeminormedAddCommGroup β] [Nonempty α] (b : β),
  ‖BoundedContinuousFunction.const α b‖₊ = ‖b‖₊
-- Mathlib.FieldTheory.LinearDisjoint
IntermediateField.LinearDisjoint.lift_adjoin_rank_eq_lift_rank_right_of_isAlgebraic_right : ∀ {F : Type u} {E : Type v} [inst : Field F] [inst_1 : Field E] [inst_2 : Algebra F E] {A : IntermediateField F E}
  {L : Type w} [inst_3 : Field L] [inst_4 : Algebra F L] [inst_5 : Algebra L E] [inst_6 : IsScalarTower F L E],
  A.LinearDisjoint L →
    ∀ [Algebra.IsAlgebraic F L],
      Cardinal.lift.{w, v} (Module.rank ↥A ↥(IntermediateField.extendScalars ⋯)) =
        Cardinal.lift.{v, w} (Module.rank F L)
-- Init.Data.String.Basic
String.Pos.slice_ofSlice : ∀ {s : String} {p₀ p₁ : s.Pos} {h : p₀ ≤ p₁} {pos : (s.slice p₀ p₁ h).Pos},
  (String.Pos.ofSlice pos).slice p₀ p₁ ⋯ ⋯ = pos
-- Std.Time.Zoned.Database.TZdb
/-- Reads timezone rules from disk based on the provided file path and timezone ID.
 -/
Std.Time.Database.TZdb.readRulesFromDisk : System.FilePath → String → IO Std.Time.TimeZone.ZoneRules
-- Mathlib.MeasureTheory.Measure.ProbabilityMeasure
/-- The push-forward of a probability measure by a measurable function.  -/
MeasureTheory.ProbabilityMeasure.map : {Ω : Type u_1} →
  {Ω' : Type u_2} →
    [inst : MeasurableSpace Ω] →
      [inst_1 : MeasurableSpace Ω'] →
        (ν : MeasureTheory.ProbabilityMeasure Ω) →
          {f : Ω → Ω'} → AEMeasurable f ↑ν → MeasureTheory.ProbabilityMeasure Ω'
-- Mathlib.Algebra.Lie.Cochain
LieModule.Cohomology.d₂₃_comp_d₁₂ : ∀ (R : Type u_1) [inst : CommRing R] (L : Type u_2) [inst_1 : LieRing L] [inst_2 : LieAlgebra R L] (M : Type u_3)
  [inst_3 : AddCommGroup M] [inst_4 : Module R M] [inst_5 : LieRingModule L M] [inst_6 : LieModule R L M],
  LieModule.Cohomology.d₂₃ R L M ∘ₗ LieModule.Cohomology.d₁₂ R L M = 0
-- Mathlib.Topology.DenseEmbedding
Dense.extend_unique_at : ∀ {α : Type u_1} {β : Type u_2} [inst : TopologicalSpace α] [inst_1 : TopologicalSpace β] {s : Set α} {f : ↑s → β}
  [T2Space β] {a : α} {g : α → β} (hs : Dense s),
  (∀ᶠ (x : ↑s) in Filter.comap Subtype.val (nhds a), g ↑x = f x) → ContinuousAt g a → hs.extend f a = g a
-- Mathlib.Topology.Order.LiminfLimsup
/-- Every cluster point `x` of a filter `f` is less than or equal to `f.limsSup`.  -/
ClusterPt.le_limsSup : ∀ {α : Type u_2} [inst : ConditionallyCompleteLinearOrder α] [inst_1 : TopologicalSpace α] [OrderTopology α]
  {f : Filter α} {x : α},
  ClusterPt x f → autoParam (Filter.IsBounded (fun x1 x2 => x1 ≤ x2) f) ClusterPt.le_limsSup._auto_1 → x ≤ f.limsSup
-- Mathlib.CategoryTheory.Monoidal.Functor
CategoryTheory.Functor.OplaxMonoidal.δ_comp_η_tensorHom_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.OplaxMonoidal] {X : C} {Y : D} (f : F.obj X ⟶ Y) {Z : D}
  (h : CategoryTheory.MonoidalCategoryStruct.tensorObj (CategoryTheory.MonoidalCategoryStruct.tensorUnit D) Y ⟶ Z),
  CategoryTheory.CategoryStruct.comp
      (CategoryTheory.Functor.OplaxMonoidal.δ F (CategoryTheory.MonoidalCategoryStruct.tensorUnit C) X)
      (CategoryTheory.CategoryStruct.comp
        (CategoryTheory.MonoidalCategoryStruct.tensorHom (CategoryTheory.Functor.OplaxMonoidal.η F) f) h) =
    CategoryTheory.CategoryStruct.comp (F.map (CategoryTheory.MonoidalCategoryStruct.leftUnitor X).hom)
      (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.leftUnitor (F.obj X)).inv
        (CategoryTheory.CategoryStruct.comp
          (CategoryTheory.MonoidalCategoryStruct.whiskerLeft (CategoryTheory.MonoidalCategoryStruct.tensorUnit D) f) h))
-- Mathlib.Topology.EMetricSpace.Defs
instWeakEMetricSpaceOrderDual : {X : Type u_1} → [inst : TopologicalSpace X] → [WeakEMetricSpace X] → WeakEMetricSpace Xᵒᵈ
-- Mathlib.CategoryTheory.ComposableArrows.Three
/-- Variant of `threeδ₁Toδ₀` for preorders.  -/
CategoryTheory.ComposableArrows.threeδ₁Toδ₀' : {ι : Type u_1} →
  [inst : Preorder ι] →
    (i₀ i₁ i₂ i₃ : ι) →
      (hi₀₁ : i₀ ≤ i₁) →
        (hi₁₂ : i₁ ≤ i₂) →
          (hi₂₃ : i₂ ≤ i₃) →
            CategoryTheory.ComposableArrows.mk₂ (CategoryTheory.homOfLE ⋯) (CategoryTheory.homOfLE hi₂₃) ⟶
              CategoryTheory.ComposableArrows.mk₂ (CategoryTheory.homOfLE hi₁₂) (CategoryTheory.homOfLE hi₂₃)
-- Mathlib.Algebra.Group.Submonoid.Operations
Submonoid.monotone_comap : ∀ {M : Type u_1} {N : Type u_2} [inst : MulOneClass M] [inst_1 : MulOneClass N] {F : Type u_4} [inst_2 : FunLike F M N]
  [mc : MonoidHomClass F M N] {f : F}, Monotone (Submonoid.comap f)
-- Mathlib.LinearAlgebra.Matrix.Basis
/-- `b.toMatrix b'` and `b'.toMatrix b` are inverses.  -/
Module.Basis.toMatrix_mul_toMatrix_flip : ∀ {ι : 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] (b : Module.Basis ι R M) (b' : Module.Basis ι' R M) [inst_3 : DecidableEq ι]
  [inst_4 : Fintype ι'], b.toMatrix ⇑b' * b'.toMatrix ⇑b = 1
-- Mathlib.Algebra.AddConstMap.Basic
AddConstMapClass.mk : ∀ {F : Type u_1} {G : outParam (Type u_2)} {H : outParam (Type u_3)} [inst : Add G] [inst_1 : Add H] {a : outParam G}
  {b : outParam H} [inst_2 : FunLike F G H], (∀ (f : F) (x : G), f (x + a) = f x + b) → AddConstMapClass F G H a b
-- Init.Data.String.Lemmas.Pattern.Find.Pred
String.Slice.Pos.find?_prop_eq_some_iff_splits : ∀ {p : Char → Prop} [inst : DecidablePred p] {s : String.Slice} {pos : s.Pos} {t u : String},
  pos.Splits t u →
    ∀ {pos' : s.Pos},
      pos.find? p = some pos' ↔ ∃ v c w, pos'.Splits (t ++ v) (String.singleton c ++ w) ∧ p c ∧ ∀ d ∈ v.toList, ¬p d
-- Mathlib.Tactic.Find
Mathlib.Tactic.Find.findDeclsPerHead : Batteries.Tactic.DeclCache (Std.HashMap Lean.HeadIndex (Array Lean.Name))
-- Mathlib.LinearAlgebra.AffineSpace.AffineSubspace.Basic
AffineSubspace.comap_inf : ∀ {k : Type u_1} {V₁ : Type u_2} {P₁ : Type u_3} {V₂ : Type u_4} {P₂ : Type u_5} [inst : Ring k]
  [inst_1 : AddCommGroup V₁] [inst_2 : Module k V₁] [inst_3 : AddTorsor V₁ P₁] [inst_4 : AddCommGroup V₂]
  [inst_5 : Module k V₂] [inst_6 : AddTorsor V₂ P₂] (s t : AffineSubspace k P₂) (f : P₁ →ᵃ[k] P₂),
  AffineSubspace.comap f (s ⊓ t) = AffineSubspace.comap f s ⊓ AffineSubspace.comap f t
-- Init.Data.Slice.Array.Lemmas
Array.toList_mkSlice_roo : ∀ {α : Type u_1} {xs : Array α} {lo hi : ℕ},
  Std.Slice.toList (Std.Roo.Sliceable.mkSlice xs lo<...hi) = List.drop (lo + 1) (List.take hi xs.toList)
-- Mathlib.RingTheory.NonUnitalSubsemiring.Basic
/-- The center of a semiring `R` is the set of elements that commute and associate with everything
in `R`  -/
NonUnitalSubsemiring.center : (R : Type u) → [inst : NonUnitalNonAssocSemiring R] → NonUnitalSubsemiring R
-- Mathlib.CategoryTheory.Triangulated.TriangleShift
/-- Rotating triangles three times backwards identifies with the shift by `-1`.  -/
CategoryTheory.Pretriangulated.invRotateInvRotateInvRotateIso : (C : Type u) →
  [inst : CategoryTheory.Category.{v, u} C] →
    [inst_1 : CategoryTheory.Preadditive C] →
      [inst_2 : CategoryTheory.HasShift C ℤ] →
        (CategoryTheory.Pretriangulated.invRotate C).comp
            ((CategoryTheory.Pretriangulated.invRotate C).comp (CategoryTheory.Pretriangulated.invRotate C)) ≅
          CategoryTheory.Pretriangulated.Triangle.shiftFunctor C (-1)
-- Std.Data.DHashMap.Lemmas
Std.DHashMap.Const.get!_of_isEmpty : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} {β : Type v} {m : Std.DHashMap α fun x => β} [EquivBEq α]
  [LawfulHashable α] [inst : Inhabited β] {a : α}, m.isEmpty = true → Std.DHashMap.Const.get! m a = default
-- Mathlib.Analysis.CStarAlgebra.CStarMatrix
CStarMatrix.instNonUnitalSemiring : {n : Type u_2} → {A : Type u_5} → [Fintype n] → [NonUnitalSemiring A] → NonUnitalSemiring (CStarMatrix n n A)
-- Mathlib.MeasureTheory.Measure.Stieltjes
StieltjesFunction.mk.sizeOf_spec : ∀ {R : Type u_1} [inst : LinearOrder R] [inst_1 : TopologicalSpace R] [inst_2 : SizeOf R] (toFun : R → ℝ)
  (mono' : Monotone toFun) (right_continuous' : ∀ (x : R), ContinuousWithinAt toFun (Set.Ici x) x),
  sizeOf { toFun := toFun, mono' := mono', right_continuous' := right_continuous' } = 1
-- Mathlib.Algebra.Star.NonUnitalSubsemiring
NonUnitalStarSubsemiring.mk : {R : Type v} →
  [inst : NonUnitalNonAssocSemiring R] →
    [inst_1 : Star R] →
      (toNonUnitalSubsemiring : NonUnitalSubsemiring R) →
        (∀ {a : R}, a ∈ toNonUnitalSubsemiring.carrier → star a ∈ toNonUnitalSubsemiring.carrier) →
          NonUnitalStarSubsemiring R
-- Aesop.Options.Public
/-- Use simp theorems from the default `simp` set, i.e. those tagged with
`@[simp]`. If this option is `false`, Aesop uses only Aesop-specific simp
theorems, i.e. those tagged with `@[aesop simp]`. Note that the congruence
lemmas from the default `simp` set are always used.
 -/
Aesop.Options.useDefaultSimpSet : Aesop.Options → Bool
-- Mathlib.Algebra.Homology.HomotopyCategory.SingleFunctors
CochainComplex.instAdditiveIntFunctorSingleFunctors : ∀ (C : Type u) [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Preadditive C]
  [inst_2 : CategoryTheory.Limits.HasZeroObject C] (n : ℤ), ((CochainComplex.singleFunctors C).functor n).Additive
-- Mathlib.Topology.Algebra.Group.Quotient
QuotientAddGroup.discreteTopology : ∀ {G : Type u_1} [inst : TopologicalSpace G] [inst_1 : AddGroup G] [SeparatelyContinuousAdd G] {N : AddSubgroup G},
  IsOpen ↑N → DiscreteTopology (G ⧸ N)
-- Lean.Data.Json.FromToJson.Basic
Lean.instFromJsonInt : Lean.FromJson ℤ
-- Mathlib.GroupTheory.Congruence.Hom
Con.correspondence.eq_1 : ∀ {M : Type u_1} [inst : Mul M] {c : Con M},
  Con.correspondence =
    { toFun := fun d => Con.mapOfSurjective c.mkMulHom ⋯ ⋯, invFun := fun d => ⟨Con.comap Con.toQuotient ⋯ d, ⋯⟩,
      left_inv := ⋯, right_inv := ⋯, map_rel_iff' := ⋯ }
-- Mathlib.Order.GaloisConnection.Defs
GaloisCoinsertion.monotoneIntro.eq_1 : ∀ {α : Type u_2} {β : Type u_3} [inst : Preorder α] [inst_1 : Preorder β] {l : α → β} {u : β → α} (hl : Monotone l)
  (hu : Monotone u) (h_u_l : ∀ (a : α), u (l a) ≤ a) (h_l_u : ∀ (b : β), l (u b) = b),
  GaloisCoinsertion.monotoneIntro hl hu h_u_l h_l_u =
    { choice := fun x x_1 => l x, gc := ⋯, u_l_le := ⋯, choice_eq := ⋯ }
-- Mathlib.SetTheory.Ordinal.Basic
Ordinal.mem_range_lift_of_le : ∀ {a : Ordinal.{u}} {b : Ordinal.{max u v}}, b ≤ Ordinal.lift.{v, u} a → b ∈ Set.range Ordinal.lift.{v, u}
-- Mathlib.RingTheory.Valuation.Integers
Valuation.Integers.valuation_irreducible_lt_one : ∀ {F : Type u} {Γ₀ : Type v} [inst : Field F] [inst_1 : LinearOrderedCommGroupWithZero Γ₀] {v : Valuation F Γ₀}
  {O : Type w} [inst_2 : CommRing O] [inst_3 : Algebra O F],
  v.Integers O → ∀ {ϖ : O}, Irreducible ϖ → v ((algebraMap O F) ϖ) < 1
-- Std.Http.Data.Headers
/-- Converts the headers to an array of key-value pairs (flattened). Each header with multiple values
produces multiple pairs.
 -/
Std.Http.Headers.toArray : Std.Http.Headers → Array (Std.Http.Header.Name × Std.Http.Header.Value)
-- Mathlib.Algebra.Polynomial.Eval.Defs
/-- Polynomial evaluation commutes with `Multiset.prod`
 -/
Polynomial.eval_multiset_prod : ∀ {R : Type u} [inst : CommSemiring R] (s : Multiset (Polynomial R)) (x : R),
  Polynomial.eval x s.prod = (Multiset.map (Polynomial.eval x) s).prod
-- Mathlib.CategoryTheory.Sites.Grothendieck
/-- To every `S : J.Cover X` and presheaf `P`, associate a `MulticospanIndex`.  -/
CategoryTheory.GrothendieckTopology.Cover.index : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    {X : C} →
      {J : CategoryTheory.GrothendieckTopology C} →
        {D : Type u₁} →
          [inst_1 : CategoryTheory.Category.{v₁, u₁} D] →
            (S : J.Cover X) → CategoryTheory.Functor Cᵒᵖ D → CategoryTheory.Limits.MulticospanIndex S.shape D
-- Mathlib.RingTheory.SimpleModule.WedderburnArtin
IsSemisimpleRing.instMatrix : ∀ (R : Type u) [inst : Ring R] [IsSemisimpleRing R] (n : Type u_2) [inst_2 : Fintype n] [inst_3 : DecidableEq n],
  IsSemisimpleRing (Matrix n n R)
-- Mathlib.GroupTheory.Congruence.Defs
/-- The quotient of a `CommMonoid` by a congruence relation is a `CommMonoid`.  -/
Con.commMonoid : {M : Type u_4} → [inst : CommMonoid M] → (c : Con M) → CommMonoid c.Quotient
-- Batteries.CodeAction.Deprecated
/-- An environment extension for identifying `@[deprecated]` definitions which can be auto-fixed  -/
Batteries.machineApplicableDeprecated : Lean.TagDeclarationExtension
-- Mathlib.Data.Set.Lattice
Set.subset_sUnion_of_subset : ∀ {α : Type u_1} {s : Set α} (t : Set (Set α)) (u : Set α), s ⊆ u → u ∈ t → s ⊆ ⋃₀ t
-- Mathlib.Analysis.Complex.UpperHalfPlane.MoebiusAction
UpperHalfPlane.glPos_smul_def : ∀ {g : GL (Fin 2) ℝ} (hg : 0 < ↑(Matrix.GeneralLinearGroup.det g)) (z : UpperHalfPlane),
  g • z = { coe := UpperHalfPlane.num g ↑z / UpperHalfPlane.denom g ↑z, coe_im_pos := ⋯ }
-- Mathlib.Data.EReal.Basic
_private.Mathlib.Data.EReal.Basic.0.EReal.coe_ennreal_top_mul : ∀ (x : NNReal), ↑(⊤ * ↑x) = ⊤ * ↑↑x
-- Mathlib.CategoryTheory.Limits.Indization.ParallelPair
/-- `f` is in fact presented by `φ`.  -/
CategoryTheory.IndParallelPairPresentation.hf : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {A B : CategoryTheory.Functor Cᵒᵖ (Type v₁)} {f g : A ⟶ B}
  (self : CategoryTheory.IndParallelPairPresentation f g),
  f = self.isColimit₁.map { pt := B, ι := self.ι₂ } (CategoryTheory.Functor.whiskerRight self.φ CategoryTheory.yoneda)
-- Mathlib.Geometry.Euclidean.Projection
/-- Reflecting an orthogonal vector plus a point in the subspace
produces the negation of that vector plus the point.  -/
EuclideanGeometry.reflection_orthogonal_vadd : ∀ {𝕜 : 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 : AffineSubspace 𝕜 P}
  [inst_5 : Nonempty ↥s] [inst_6 : s.direction.HasOrthogonalProjection] {p : P},
  p ∈ s → ∀ {v : V}, v ∈ s.directionᗮ → (EuclideanGeometry.reflection s) (v +ᵥ p) = -v +ᵥ p
-- Mathlib.Algebra.Ring.Opposite
AddOpposite.unop_intCast : ∀ {R : Type u_1} [inst : IntCast R] (n : ℤ), AddOpposite.unop ↑n = ↑n
-- Mathlib.Algebra.Algebra.Subalgebra.Basic
algebraMap_mem : ∀ {S : Type u_1} {R : Type u_2} {A : Type u_3} [inst : CommSemiring R] [inst_1 : Semiring A] [inst_2 : Algebra R A]
  [inst_3 : SetLike S A] [OneMemClass S A] [SMulMemClass S R A] (s : S) (r : R), (algebraMap R A) r ∈ s
-- Std.Data.Internal.List.Associative
Std.Internal.List.containsKey_insertEntryIfNew_self : ∀ {α : Type u} {β : α → Type v} [inst : BEq α] [EquivBEq α] {l : List ((a : α) × β a)} {k : α} {v : β k},
  Std.Internal.List.containsKey k (Std.Internal.List.insertEntryIfNew k v l) = true
-- Mathlib.Data.Bool.Basic
Bool.or_inl : ∀ {a b : Bool}, a = true → (a || b) = true
-- Init.Data.String.Lemmas.Pattern.Pred
String.Slice.endsWith_prop_eq_endsWith_decide : ∀ {p : Char → Prop} [inst : DecidablePred p] {s : String.Slice}, s.endsWith p = s.endsWith fun x => decide (p x)
-- Init.Data.String.Defs
String.startValidPos : (s : String) → s.Pos
-- Std.Data.ExtTreeSet.Lemmas
Std.ExtTreeSet.minD_insert : ∀ {α : Type u} {cmp : α → α → Ordering} {t : Std.ExtTreeSet α cmp} [inst : Std.TransCmp cmp] {k fallback : α},
  (t.insert k).minD fallback = t.min?.elim k fun k' => if cmp k k' = Ordering.lt then k else k'
-- Mathlib.NumberTheory.NumberField.Basic
NumberField.RingOfIntegers.instIsIntegrallyClosed : ∀ {K : Type u_1} [inst : Field K] [NumberField K], IsIntegrallyClosed (NumberField.RingOfIntegers K)
-- Mathlib.Analysis.Normed.Algebra.Unitization
Unitization.uniformContinuous_fst : ∀ {𝕜 : Type u_3} {A : Type u_4} [inst : NontriviallyNormedField 𝕜] [inst_1 : NonUnitalNormedRing A],
  UniformContinuous fun x => x.toProd.1
-- Std.Http.Data.Request
Std.Http.Request.Head.mk : Std.Http.Method → Std.Http.Version → Std.Http.RequestTarget → Std.Http.Headers → Std.Http.Request.Head
-- Mathlib.Analysis.Real.Hyperreal
Hyperreal.infinitePos_iff_infinitesimal_inv_pos : ∀ {x : ℝ*}, x.InfinitePos ↔ x⁻¹.Infinitesimal ∧ 0 < x⁻¹
-- Mathlib.Condensed.Limits
instHasFiniteColimitsCondensedOfHasWeakSheafifyCompHausCoherentTopology : ∀ {A : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} A] [CategoryTheory.Limits.HasFiniteColimits A]
  [CategoryTheory.HasWeakSheafify (CategoryTheory.coherentTopology CompHaus) A],
  CategoryTheory.Limits.HasFiniteColimits (Condensed A)
-- Mathlib.Algebra.Order.Ring.StandardPart
ArchimedeanClass.FiniteElement.ext : ∀ {K : Type u_1} [inst : LinearOrder K] [inst_1 : Field K] [inst_2 : IsOrderedRing K]
  {x y : ArchimedeanClass.FiniteElement K}, ↑x = ↑y → x = y
-- Aesop.Options.Public
Aesop.instBEqStrategy : BEq Aesop.Strategy
-- Init.Data.Range.Polymorphic.RangeIterator
_private.Init.Data.Range.Polymorphic.RangeIterator.0.Std.IterM.DefaultConsumers.forIn'_eq_match_step.match_3.eq_1 : ∀ {α β : Type u_1} {m : Type u_1 → Type u_2} [inst : Std.Iterator α m β] {it : Std.IterM m β}
  (motive : it.Step → Sort u_3) (it' : Std.IterM m β) (out : β) (h : it.IsPlausibleStep (Std.IterStep.yield it' out))
  (h_1 :
    (it' : Std.IterM m β) →
      (out : β) → (h : it.IsPlausibleStep (Std.IterStep.yield it' out)) → motive ⟨Std.IterStep.yield it' out, h⟩)
  (h_2 : (it' : Std.IterM m β) → (h : it.IsPlausibleStep (Std.IterStep.skip it')) → motive ⟨Std.IterStep.skip it', h⟩)
  (h_3 : (property : it.IsPlausibleStep Std.IterStep.done) → motive ⟨Std.IterStep.done, property⟩),
  (match ⟨Std.IterStep.yield it' out, h⟩ with
    | ⟨Std.IterStep.yield it' out, h⟩ => h_1 it' out h
    | ⟨Std.IterStep.skip it', h⟩ => h_2 it' h
    | ⟨Std.IterStep.done, property⟩ => h_3 property) =
    h_1 it' out h
-- Mathlib.RingTheory.MvPolynomial.MonomialOrder
MonomialOrder.leadingTerm_C : ∀ {σ : Type u_1} {m : MonomialOrder σ} {R : Type u_2} [inst : CommSemiring R] (c : R),
  m.leadingTerm (MvPolynomial.C c) = MvPolynomial.C c
-- Lean.Meta.DiscrTree.Types
Lean.Meta.DiscrTree.mk : {α : Type} → Lean.PersistentHashMap Lean.Meta.DiscrTree.Key (Lean.Meta.DiscrTree.Trie α) → Lean.Meta.DiscrTree α
-- Init.Data.Array.Count
Array.countP_le_size : ∀ {α : Type u_1} {p : α → Bool} {xs : Array α}, Array.countP p xs ≤ xs.size
-- Mathlib.GroupTheory.Coset.Basic
Subgroup.quotientMapOfLE.eq_1 : ∀ {α : Type u_1} [inst : Group α] {s t : Subgroup α} (h : s ≤ t), Subgroup.quotientMapOfLE h = Quotient.map' id ⋯
-- Mathlib.Combinatorics.Configuration
Configuration.HasPoints.existsUnique_point : ∀ (P : Type u_1) (L : Type u_2) [inst : Membership P L] [Configuration.HasPoints P L] (l₁ l₂ : L),
  l₁ ≠ l₂ → ∃! p, p ∈ l₁ ∧ p ∈ l₂