mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Topology.Algebra.SeparationQuotient.FiniteDimensional
/-- The separation quotient of a finite module is a finite module.  -/
SeparationQuotient.instModuleFinite : ∀ {R : Type u_1} {M : Type u_2} [inst : Semiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M] [Module.Finite R M]
  [inst_4 : TopologicalSpace M] [inst_5 : ContinuousAdd M] [inst_6 : ContinuousConstSMul R M],
  Module.Finite R (SeparationQuotient M)
-- Mathlib.LinearAlgebra.FreeModule.Finite.Basic
/-- A free module with a basis indexed by a `Fintype` is finite.  -/
Module.Finite.of_basis : ∀ {R : Type u_1} {M : Type u_2} {ι : Type u_3} [inst : Semiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M]
  [Finite ι] (b : Module.Basis ι R M), Module.Finite R M
-- Lean.Data.Lsp.TextSync
Lean.Lsp.instFromJsonDidChangeTextDocumentParams.fromJson : Lean.Json → Except String Lean.Lsp.DidChangeTextDocumentParams
-- Mathlib.LinearAlgebra.Matrix.Basis
Module.Basis.toMatrix_apply : ∀ {ι : 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] (e : Module.Basis ι R M) (v : ι' → M) (i : ι) (j : ι'), e.toMatrix v i j = (e.repr (v j)) i
-- Mathlib.Algebra.QuaternionBasis
QuaternionAlgebra.Basis.mk.inj : ∀ {R : Type u_1} {A : Type u_2} {inst : CommRing R} {inst_1 : Ring A} {inst_2 : Algebra R A} {c₁ c₂ c₃ : R} {i j k : A}
  {i_mul_i : i * i = c₁ • 1 + c₂ • i} {j_mul_j : j * j = c₃ • 1} {i_mul_j : i * j = k} {j_mul_i : j * i = c₂ • j - k}
  {i_1 j_1 k_1 : A} {i_mul_i_1 : i_1 * i_1 = c₁ • 1 + c₂ • i_1} {j_mul_j_1 : j_1 * j_1 = c₃ • 1}
  {i_mul_j_1 : i_1 * j_1 = k_1} {j_mul_i_1 : j_1 * i_1 = c₂ • j_1 - k_1},
  { i := i, j := j, k := k, i_mul_i := i_mul_i, j_mul_j := j_mul_j, i_mul_j := i_mul_j, j_mul_i := j_mul_i } =
      { i := i_1, j := j_1, k := k_1, i_mul_i := i_mul_i_1, j_mul_j := j_mul_j_1, i_mul_j := i_mul_j_1,
        j_mul_i := j_mul_i_1 } →
    i = i_1 ∧ j = j_1 ∧ k = k_1
-- Mathlib.CategoryTheory.Groupoid.VertexGroup
CategoryTheory.Groupoid.vertexGroup_mul : ∀ {C : Type u} [inst : CategoryTheory.Groupoid C] (c : C) (x y : c ⟶ c), x * y = CategoryTheory.CategoryStruct.comp x y
-- Mathlib.Analysis.LocallyConvex.AbsConvex
nhds_hasBasis_absConvex_closed : ∀ (𝕜 : Type u_1) (E : Type u_2) [inst : NontriviallyNormedField 𝕜] [inst_1 : PartialOrder 𝕜] [inst_2 : AddCommGroup E]
  [inst_3 : Module 𝕜 E] [inst_4 : TopologicalSpace E] [LocallyConvexSpace 𝕜 E] [ContinuousSMul 𝕜 E]
  [IsTopologicalAddGroup E] [ZeroLEOneClass 𝕜], (nhds 0).HasBasis (fun s => s ∈ nhds 0 ∧ IsClosed s ∧ AbsConvex 𝕜 s) id
-- Mathlib.Data.EReal.Basic
EReal.preimage_coe_Iio : ∀ (y : ℝ), Real.toEReal ⁻¹' Set.Iio ↑y = Set.Iio y
-- Mathlib.Data.Analysis.Topology
Ctop.Realizer.mem_nhds : ∀ {α : Type u_1} [T : TopologicalSpace α] (F : Ctop.Realizer α) {s : Set α} {a : α},
  s ∈ nhds a ↔ ∃ b, a ∈ F.F.f b ∧ F.F.f b ⊆ s
-- Mathlib.Order.Interval.Set.Basic
Set.Iio_True : Set.Iio True = {False}
-- Mathlib.Order.RelClasses
isStrictOrderConnected_of_isStrictTotalOrder : ∀ {α : Type u} {r : α → α → Prop} [IsStrictTotalOrder α r], IsOrderConnected α r
-- Mathlib.RingTheory.Ideal.Operations
Ideal.isCoprime_iff_exists : ∀ {R : Type u} [inst : CommSemiring R] {I J : Ideal R}, IsCoprime I J ↔ ∃ i ∈ I, ∃ j ∈ J, i + j = 1
-- Mathlib.Order.Iterate
/-- If `f ≤ g` and `f` is monotone, then `f^[n] ≤ g^[n]`.  -/
Monotone.iterate_le_of_le : ∀ {α : Type u_1} [inst : Preorder α] {f g : α → α}, Monotone f → f ≤ g → ∀ (n : ℕ), f^[n] ≤ g^[n]
-- Std.Tactic.BVDecide.Bitblast.BVExpr.Circuit.Impl.Operations.Cpop
Std.Tactic.BVDecide.BVExpr.bitblast.blastCpopTreeTarget.mk.congr_simp : ∀ {α : Type} [inst : Hashable α] [inst_1 : DecidableEq α] {aig : Std.Sat.AIG α} {w len : ℕ}
  (x x_1 : aig.RefVec (len * w)),
  x = x_1 → ∀ (h : 0 < len), { len := len, x := x, h := h } = { len := len, x := x_1, h := h }
-- Mathlib.MeasureTheory.Integral.Bochner.Set
MeasureTheory.setIntegral_le_nonneg : ∀ {X : Type u_1} {mX : MeasurableSpace X} {μ : MeasureTheory.Measure X} {f : X → ℝ} {s : Set X},
  MeasurableSet s →
    MeasureTheory.StronglyMeasurable f →
      MeasureTheory.Integrable f μ → ∫ (x : X) in s, f x ∂μ ≤ ∫ (x : X) in {y | 0 ≤ f y}, f x ∂μ
-- Init.Data.Array.Find
Array.findIdx?_empty : ∀ {α : Type u_1} {p : α → Bool}, Array.findIdx? p #[] = none
-- Mathlib.CategoryTheory.Shift.InducedShiftSequence
/-- The `isoZero` field of the induced shift sequence.  -/
CategoryTheory.Functor.ShiftSequence.induced.isoZero : {C : Type u_1} →
  {D : Type u_2} →
    {A : Type u_3} →
      [inst : CategoryTheory.Category.{v_1, u_1} C] →
        [inst_1 : CategoryTheory.Category.{v_2, u_2} D] →
          [inst_2 : CategoryTheory.Category.{v_3, u_3} A] →
            {L : CategoryTheory.Functor C D} →
              {F : CategoryTheory.Functor D A} →
                {G : CategoryTheory.Functor C A} →
                  (L.comp F ≅ G) →
                    (M : Type u_4) →
                      [inst_3 : AddMonoid M] →
                        [inst_4 : CategoryTheory.HasShift C M] →
                          [inst_5 : G.ShiftSequence M] →
                            (F' : M → CategoryTheory.Functor D A) →
                              ((m : M) → L.comp (F' m) ≅ G.shift m) →
                                [((CategoryTheory.Functor.whiskeringLeft C D A).obj L).Full] →
                                  [((CategoryTheory.Functor.whiskeringLeft C D A).obj L).Faithful] → F' 0 ≅ F
-- Mathlib.Topology.Order.Hom.Esakia
EsakiaHomClass.toContinuousOrderHomClass : ∀ {F : Type u_6} {α : outParam (Type u_7)} {β : outParam (Type u_8)} {inst : TopologicalSpace α} {inst_1 : Preorder α}
  {inst_2 : TopologicalSpace β} {inst_3 : Preorder β} {inst_4 : FunLike F α β} [self : EsakiaHomClass F α β],
  ContinuousOrderHomClass F α β
-- Mathlib.CategoryTheory.Generator.Basic
CategoryTheory.hasCoseparator_op_iff : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C],
  CategoryTheory.HasCoseparator Cᵒᵖ ↔ CategoryTheory.HasSeparator C
-- Init.Data.List.Nat.Range
List.find?_range'_eq_none : ∀ {s n : ℕ} {p : ℕ → Bool}, List.find? p (List.range' s n) = none ↔ ∀ (i : ℕ), s ≤ i → i < s + n → (!p i) = true
-- Lean.Data.Lsp.CodeActions
Lean.Lsp.CodeActionDisabled.mk.sizeOf_spec : ∀ (reason : String), sizeOf { reason := reason } = 1 + sizeOf reason
-- Mathlib.Analysis.Complex.Hadamard
/-- The norm of the function `scale f l u` is bounded above on the closed strip `re⁻¹' [0, 1]`.  -/
Complex.HadamardThreeLines.scale_bddAbove : ∀ {E : Type u_1} [inst : NormedAddCommGroup E] {f : ℂ → E} {l u : ℝ},
  l < u →
    BddAbove (norm ∘ f '' Complex.HadamardThreeLines.verticalClosedStrip l u) →
      BddAbove (norm ∘ Complex.HadamardThreeLines.scale f l u '' Complex.HadamardThreeLines.verticalClosedStrip 0 1)
-- Mathlib.Combinatorics.Quiver.Covering
Quiver.symmetrifyStar.eq_1 : ∀ {U : Type u_1} [inst : Quiver U] (u : U),
  Quiver.symmetrifyStar u =
    Equiv.sigmaSumDistrib (Quiver.Hom (Quiver.Symmetrify.of.obj u)) fun v => v ⟶ Quiver.Symmetrify.of.obj u
-- Mathlib.GroupTheory.Perm.Fin
Fin.cycleRange_apply : ∀ {n : ℕ} [inst : NeZero n] (i j : Fin n), i.cycleRange j = if j < i then j + 1 else if j = i then 0 else j
-- Mathlib.Algebra.Order.Hom.Ring
/-- Copy of an `OrderRingHom` with a new `toFun` equal to the old one. Useful to fix definitional
equalities.  -/
OrderRingHom.copy : {α : Type u_2} →
  {β : Type u_3} →
    [inst : NonAssocSemiring α] →
      [inst_1 : Preorder α] →
        [inst_2 : NonAssocSemiring β] → [inst_3 : Preorder β] → (f : α →+*o β) → (f' : α → β) → f' = ⇑f → α →+*o β
-- Mathlib.Combinatorics.Matroid.Loop
Matroid.isLoop_iff_closure_eq_loops_and_mem_ground : ∀ {α : Type u_1} {M : Matroid α} {e : α}, M.IsLoop e ↔ M.closure {e} = M.loops ∧ e ∈ M.E
-- Std.Sync.Broadcast
_private.Std.Sync.Broadcast.0.Std.instReprSlot : {α : Type} → [Repr α] → Repr (Std.Slot✝ α)
-- Mathlib.Algebra.Order.Group.Unbundled.Int
Int.sign_mul_abs : ∀ (a : ℤ), a.sign * |a| = a
-- Init.Data.String.Lemmas.Pattern.TakeDrop.Basic
String.startsWith_dropWhile : ∀ {ρ : Type} {pat : ρ} [inst : String.Slice.Pattern.Model.PatternModel pat]
  [String.Slice.Pattern.Model.StrictPatternModel pat] [inst_2 : String.Slice.Pattern.ForwardPattern pat]
  [String.Slice.Pattern.Model.LawfulForwardPatternModel pat] {s : String}, (s.dropWhile pat).startsWith pat = false
-- Mathlib.Algebra.Order.Group.Synonym
Colex.instLeftCancelMonoid : {α : Type u_1} → [LeftCancelMonoid α] → LeftCancelMonoid (Colex α)
-- Mathlib.Tactic.ComputeAsymptotics.Multiseries.Monomial.Predicates
Tactic.ComputeAsymptotics.UnitMonomial.Sign.pos.sizeOf_spec : sizeOf Tactic.ComputeAsymptotics.UnitMonomial.Sign.pos = 1
-- Mathlib.Data.Nat.Multiplicity
Nat.Prime.emultiplicity_pow_self : ∀ {p n : ℕ}, Nat.Prime p → emultiplicity p (p ^ n) = ↑n
-- Mathlib.CategoryTheory.Limits.Shapes.BinaryBiproducts
CategoryTheory.Limits.biprod.mapIso_hom : ∀ {C : Type uC} [inst : CategoryTheory.Category.{uC', uC} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  {W X Y Z : C} [inst_2 : CategoryTheory.Limits.HasBinaryBiproduct W X]
  [inst_3 : CategoryTheory.Limits.HasBinaryBiproduct Y Z] (f : W ≅ Y) (g : X ≅ Z),
  (CategoryTheory.Limits.biprod.mapIso f g).hom = CategoryTheory.Limits.biprod.map f.hom g.hom
-- Mathlib.CategoryTheory.Sites.Hypercover.One
CategoryTheory.PreZeroHypercover.refineOneHypercover_p₂ : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {X : C} (E : CategoryTheory.PreZeroHypercover X)
  [inst_1 : E.HasPullbacks]
  (F : (i j : E.I₀) → CategoryTheory.PreZeroHypercover (CategoryTheory.Limits.pullback (E.f i) (E.f j))) (i j : E.I₀)
  (k : (F i j).I₀),
  (E.refineOneHypercover F).p₂ k =
    CategoryTheory.CategoryStruct.comp ((F i j).f k) (CategoryTheory.Limits.pullback.snd (E.f i) (E.f j))
-- Std.Data.ExtTreeSet.Lemmas
Std.ExtTreeSet.insertMany_append : ∀ {α : Type u} {cmp : α → α → Ordering} {t : Std.ExtTreeSet α cmp} [inst : Std.TransCmp cmp] {l₁ l₂ : List α},
  t.insertMany (l₁ ++ l₂) = (t.insertMany l₁).insertMany l₂
-- Std.Async.Basic
/-- Lifts a `BaseAsync` computation into a `Task` that can be awaited and joined.
 -/
Std.Async.BaseAsync.asTask : {α : Type} → Std.Async.BaseAsync α → optParam Task.Priority Task.Priority.default → BaseIO (Task α)
-- Mathlib.Analysis.Asymptotics.Lemmas
Asymptotics.IsBigOWith.smul : ∀ {α : Type u_1} {E' : Type u_6} {F' : Type u_7} {R : Type u_13} {𝕜' : Type u_16} [inst : SeminormedAddCommGroup E']
  [inst_1 : SeminormedAddCommGroup F'] [inst_2 : SeminormedRing R] [inst_3 : NormedDivisionRing 𝕜'] {c c' : ℝ}
  {f' : α → E'} {g' : α → F'} {l : Filter α} [inst_4 : Module R E'] [IsBoundedSMul R E'] [inst_6 : Module 𝕜' F']
  [NormSMulClass 𝕜' F'] {k₁ : α → R} {k₂ : α → 𝕜'},
  Asymptotics.IsBigOWith c l k₁ k₂ →
    Asymptotics.IsBigOWith c' l f' g' → Asymptotics.IsBigOWith (c * c') l (fun x => k₁ x • f' x) fun x => k₂ x • g' x
-- Mathlib.GroupTheory.Coset.Basic
orbit_subgroup_eq_rightCoset : ∀ {α : Type u_1} [inst : Group α] (s : Subgroup α) (a : α), MulAction.orbit (↥s) a = MulOpposite.op a • ↑s
-- Mathlib.Topology.MetricSpace.DilationEquiv
DilationEquiv.symm_trans_self : ∀ {X : Type u_1} {Y : Type u_2} [inst : PseudoEMetricSpace X] [inst_1 : PseudoEMetricSpace Y] (e : X ≃ᵈ Y),
  e.symm.trans e = DilationEquiv.refl Y
-- Mathlib.CategoryTheory.Monad.Adjunction
CategoryTheory.instFullAlgebraToMonadAdjComparison : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] (T : CategoryTheory.Monad C),
  (CategoryTheory.Monad.comparison T.adj).Full
-- Mathlib.RingTheory.AdicCompletion.LocalRing
AdicCompletion.instIsLocalHomMaximalIdealRingHomAlgebraMapOfIsNoetherianRing : ∀ {R : Type u_1} [inst : CommRing R] [IsNoetherianRing R] [inst_2 : IsLocalRing R],
  IsLocalHom (algebraMap R (AdicCompletion (IsLocalRing.maximalIdeal R) R))
-- Mathlib.AlgebraicGeometry.StructureSheaf
_private.Mathlib.AlgebraicGeometry.StructureSheaf.0.AlgebraicGeometry.StructureSheaf.instIsLocalizedModuleCarrierOfStalkModuleCatStructurePresheafInModuleCatPrimeComplAsIdealHomToStalkₗ' : ∀ {R M : Type u} [inst : CommRing R] [inst_1 : AddCommGroup M] [inst_2 : Module R M]
  (x : ↑(AlgebraicGeometry.PrimeSpectrum.Top R)),
  IsLocalizedModule x.asIdeal.primeCompl (ModuleCat.Hom.hom (AlgebraicGeometry.StructureSheaf.toStalkₗ'✝ R M x))
-- Mathlib.MeasureTheory.Function.StronglyMeasurable.AEStronglyMeasurable
/-- **Alias** of `MeasureTheory.AEStronglyMeasurable.fun_const_smul`.

---

Eta-expanded form of `MeasureTheory.AEStronglyMeasurable.const_smul` -/
MeasureTheory.AEStronglyMeasurable.const_smul' : ∀ {α : Type u_1} {β : Type u_2} [inst : TopologicalSpace β] {m m₀ : MeasurableSpace α} {μ : MeasureTheory.Measure α}
  {f : α → β} {𝕜 : Type u_5} [inst_1 : SMul 𝕜 β] [ContinuousConstSMul 𝕜 β],
  MeasureTheory.AEStronglyMeasurable f μ → ∀ (c : 𝕜), MeasureTheory.AEStronglyMeasurable (fun i => c • f i) μ
-- Mathlib.MeasureTheory.Measure.MeasureSpace
MeasureTheory.Measure.le_iff : ∀ {α : Type u_1} {m0 : MeasurableSpace α} {μ₁ μ₂ : MeasureTheory.Measure α},
  μ₁ ≤ μ₂ ↔ ∀ (s : Set α), MeasurableSet s → μ₁ s ≤ μ₂ s
-- Mathlib.RingTheory.WittVector.StructurePolynomial
constantCoeff_wittStructureRat : ∀ (p : ℕ) {idx : Type u_2} [hp : Fact (Nat.Prime p)] (Φ : MvPolynomial idx ℚ),
  MvPolynomial.constantCoeff Φ = 0 → ∀ (n : ℕ), MvPolynomial.constantCoeff (wittStructureRat p Φ n) = 0
-- Mathlib.Algebra.Order.AbsoluteValue.Basic
/-- The absolute value is nonnegative  -/
AbsoluteValue.nonneg' : ∀ {R : Type u_5} {S : Type u_6} [inst : Semiring R] [inst_1 : Semiring S] [inst_2 : PartialOrder S]
  (self : AbsoluteValue R S) (x : R), 0 ≤ self.toFun x
-- Std.Data.DHashMap.Internal.RawLemmas
Std.DHashMap.Internal.Raw₀.Const.distinct_keys_toList : ∀ {α : Type u} [inst : BEq α] [inst_1 : Hashable α] {β : Type v} (m : Std.DHashMap.Internal.Raw₀ α fun x => β)
  [EquivBEq α] [LawfulHashable α],
  (↑m).WF → List.Pairwise (fun a b => (a.1 == b.1) = false) (Std.DHashMap.Raw.Const.toList ↑m)
-- Std.Data.DTreeMap.Internal.Model
Std.DTreeMap.Internal.Impl.entryAtIdx?.eq_2 : ∀ {α : Type u} {β : α → Type v} (x size : ℕ) (k : α) (v : β k) (l r : Std.DTreeMap.Internal.Impl α β),
  (Std.DTreeMap.Internal.Impl.inner size k v l r).entryAtIdx? x =
    match compare x l.size with
    | Ordering.lt => l.entryAtIdx? x
    | Ordering.eq => some ⟨k, v⟩
    | Ordering.gt => r.entryAtIdx? (x - l.size - 1)
-- Mathlib.Algebra.Homology.ImageToKernel
factorThruImageSubobject_comp_imageToKernel : ∀ {V : Type u} [inst : CategoryTheory.Category.{v, u} V] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms V] {A B C : V}
  (f : A ⟶ B) [inst_2 : CategoryTheory.Limits.HasImage f] (g : B ⟶ C) [inst_3 : CategoryTheory.Limits.HasKernel g]
  (w : CategoryTheory.CategoryStruct.comp f g = 0),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.factorThruImageSubobject f) (imageToKernel f g w) =
    CategoryTheory.Limits.factorThruKernelSubobject g f w
-- Std.Tactic.BVDecide.Bitblast.BVExpr.Basic
Std.Tactic.BVDecide.BVLogicalExpr.eval_literal : ∀ {assign : Std.Tactic.BVDecide.BVExpr.Assignment} {pred : Std.Tactic.BVDecide.BVPred},
  Std.Tactic.BVDecide.BVLogicalExpr.eval assign (Std.Tactic.BVDecide.BoolExpr.literal pred) =
    Std.Tactic.BVDecide.BVPred.eval assign pred
-- Mathlib.MeasureTheory.Measure.Content
MeasureTheory.Content.mono' : ∀ {G : Type w} [inst : TopologicalSpace G] (self : MeasureTheory.Content G) (K₁ K₂ : TopologicalSpace.Compacts G),
  ↑K₁ ⊆ ↑K₂ → self.toFun K₁ ≤ self.toFun K₂
-- Mathlib.Algebra.Order.Group.Pointwise.Interval
Set.preimage_mul_const_Ici : ∀ {α : Type u_1} [inst : CommGroup α] [inst_1 : PartialOrder α] [IsOrderedMonoid α] (a b : α),
  (fun x => x * a) ⁻¹' Set.Ici b = Set.Ici (b / a)
-- Init.Data.Array.Lemmas
Array.back?_replicate : ∀ {α : Type u_1} {a : α} {n : ℕ}, (Array.replicate n a).back? = if n = 0 then none else some a
-- Mathlib.Order.Monotone.Basic
/-- **Alias** of the reverse direction of `strictAntiOn_toDual_comp_iff`. -/
StrictMonoOn.dual_right : ∀ {α : Type u} {β : Type v} [inst : Preorder α] [inst_1 : Preorder β] {f : α → β} {s : Set α},
  StrictMonoOn f s → StrictAntiOn (⇑OrderDual.toDual ∘ f) s
-- Mathlib.Computability.TuringMachine.PostTuringMachine
Turing.TM0.Cfg.mk.sizeOf_spec : ∀ {Γ : Type u_1} {Λ : Type u_2} [inst : Inhabited Γ] [inst_1 : SizeOf Γ] [inst_2 : SizeOf Λ] (q : Λ)
  (Tape : Turing.Tape Γ), sizeOf { q := q, Tape := Tape } = 1 + sizeOf q + sizeOf Tape
-- Mathlib.GroupTheory.Commutator.Basic
addCommutatorElement_add_left_eq_addConj_add : ∀ {G : Type u_1} [inst : AddGroup G] (a b c : G), ⁅a + b, c⁆ = a + ⁅b, c⁆ + -a + ⁅a, c⁆
-- Mathlib.Order.RelClasses
/-- Set notation form of `ne_of_lt` -/
ne_of_ssubset : ∀ {α : Type u_1} [UsesSetNotationForOrder α] [inst : Preorder α] {a b : α}, a ⊂ b → a ≠ b
-- Mathlib.GroupTheory.Coxeter.Inversion
CoxeterSystem.IsReflection.conj : ∀ {B : Type u_1} {W : Type u_2} [inst : Group W] {M : CoxeterMatrix B} {cs : CoxeterSystem M W} {t : W},
  cs.IsReflection t → ∀ (w : W), cs.IsReflection (w * t * w⁻¹)
-- Mathlib.MeasureTheory.Function.UniformIntegrable
/-- This lemma is less general than `MeasureTheory.unifIntegrable_finite` which applies to
all sequences indexed by a finite type.  -/
MeasureTheory.unifIntegrable_fin : ∀ {α : Type u_1} {β : Type u_2} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} [inst : NormedAddCommGroup β]
  {p : ENNReal},
  1 ≤ p →
    p ≠ ⊤ →
      ∀ {n : ℕ} {f : Fin n → α → β}, (∀ (i : Fin n), MeasureTheory.MemLp (f i) p μ) → MeasureTheory.UnifIntegrable f p μ
-- Mathlib.LinearAlgebra.RootSystem.RootPairingCat
/-- The coweight space of a root pairing.  -/
RootPairingCat.coweight : {R : Type u} → [inst : CommRing R] → RootPairingCat R → Type v
-- Mathlib.Logic.Equiv.Defs
Equiv.piUnique_apply : ∀ {α : Sort u} [inst : Unique α] (β : α → Sort u_1), ⇑(Equiv.piUnique β) = fun f => f default
-- Lean.Linter.UnusedVariables
Lean.Linter.UnusedVariables.FVarDefinition.mk.injEq : ∀ (userName : Lean.Name) (stx : Lean.Syntax) (opts : Lean.Options) (aliases : Array Lean.FVarId)
  (userName_1 : Lean.Name) (stx_1 : Lean.Syntax) (opts_1 : Lean.Options) (aliases_1 : Array Lean.FVarId),
  ({ userName := userName, stx := stx, opts := opts, aliases := aliases } =
      { userName := userName_1, stx := stx_1, opts := opts_1, aliases := aliases_1 }) =
    (userName = userName_1 ∧ stx = stx_1 ∧ opts = opts_1 ∧ aliases = aliases_1)
-- Lean.Meta.NatInstTesters
Lean.Meta.Structural.isInstHPowNat : Lean.Expr → Lean.MetaM Bool
-- Batteries.Data.List.Basic
/-- Two nil lists are `Forall₂`-related  -/
List.Forall₂.nil : ∀ {α : Type u_1} {β : Type u_2} {R : α → β → Prop}, List.Forall₂ R [] []
-- Aesop.RuleSet.Filter
Aesop.RuleSetNameFilter : Type
-- Mathlib.Analysis.Normed.Module.Bases
/-- A classical Schauder basis indexed by `ℕ` with conditional convergence.  -/
SchauderBasis : (𝕜 : Type u_4) →
  (X : Type u_5) →
    [inst : NontriviallyNormedField 𝕜] →
      [inst_1 : NormedAddCommGroup X] → [NormedSpace 𝕜 X] → Type (max (max 0 u_4) u_5)
-- Mathlib.CategoryTheory.Preadditive.Opposite
CategoryTheory.moduleEndLeft : (C : Type u_1) →
  [inst : CategoryTheory.Category.{v_1, u_1} C] →
    [inst_1 : CategoryTheory.Preadditive C] → {X Y : C} → Module (CategoryTheory.End X)ᵐᵒᵖ (X ⟶ Y)
-- Init.Data.List.Lemmas
List.getLast_of_mem_getLast? : ∀ {α : Type u_1} {x : α} {l : List α} (hx : x ∈ l.getLast?), l.getLast ⋯ = x
-- Mathlib.Data.Real.Sign
Real.sign_neg : ∀ {r : ℝ}, (-r).sign = -r.sign
-- Mathlib.Topology.ContinuousMap.ZeroAtInfty
ZeroAtInftyContinuousMap.instNonUnitalNonAssocSemiring : {α : Type u} →
  {β : Type v} →
    [inst : TopologicalSpace α] →
      [inst_1 : TopologicalSpace β] →
        [inst_2 : NonUnitalNonAssocSemiring β] →
          [IsTopologicalSemiring β] → NonUnitalNonAssocSemiring (ZeroAtInftyContinuousMap α β)
-- Init.Tactics
/-- If true (default: false), abstract the universe parameters of the surrounding
declaration as level metavariables in the goal handed to the inner tactic, so it
can specialize them by exhibiting witnesses at specific universes. By default
these parameters are kept fixed.  -/
Lean.Parser.Tactic.ImpossibleConfig.levels : Lean.Parser.Tactic.ImpossibleConfig → Bool
-- Std.Do.SPred.DerivedLaws
Std.Do.SPred.pure_elim_r : ∀ {σs : List (Type u)} {Q R : Std.Do.SPred σs} {φ : Prop}, (φ → Q ⊢ₛ R) → Q ∧ ⌜φ⌝ ⊢ₛ R
-- Lean.Meta.LazyDiscrTree
/-- Maps keys to index in tries array.  -/
Lean.Meta.LazyDiscrTree.PreDiscrTree.roots : {α : Type} → Lean.Meta.LazyDiscrTree.PreDiscrTree α → Std.HashMap Lean.Meta.LazyDiscrTree.Key ℕ
-- Mathlib.RingTheory.Localization.AtPrime.Extension
IsLocalization.AtPrime.liesOver_comap_of_liesOver : ∀ {R : Type u_1} {S : Type u_2} [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : Algebra R S] (p : Ideal R)
  [inst_3 : p.IsPrime] (Rₚ : Type u_3) [inst_4 : CommRing Rₚ] [inst_5 : Algebra R Rₚ] [IsLocalization.AtPrime Rₚ p]
  [inst_7 : IsLocalRing Rₚ] {T : Type u_5} [inst_8 : CommRing T] [inst_9 : Algebra R T] [inst_10 : Algebra Rₚ T]
  [inst_11 : Algebra S T] [IsScalarTower R S T] [IsScalarTower R Rₚ T] (Q : Ideal T)
  [Q.LiesOver (IsLocalRing.maximalIdeal Rₚ)], (Ideal.comap (algebraMap S T) Q).LiesOver p
-- Init.Data.Range.Polymorphic.Lemmas
Std.Roo.eq_succMany?_of_toList_eq_append_cons : ∀ {α : Type u} {r : Std.Roo α} [inst : LT α] [inst_1 : DecidableLT α] [inst_2 : Std.PRange.UpwardEnumerable α]
  [inst_3 : Std.PRange.LawfulUpwardEnumerable α] [inst_4 : Std.PRange.LawfulUpwardEnumerableLT α]
  [inst_5 : Std.Rxo.IsAlwaysFinite α] {pref suff : List α} {cur : α} (h : r.toList = pref ++ cur :: suff),
  cur = (Std.PRange.succMany? (pref.length + 1) r.lower).get ⋯
-- Std.Data.DTreeMap.Internal.Model
Std.DTreeMap.Internal.Impl.Const.some_maxEntry_eq_maxEntry? : ∀ {α : Type u} {β : Type v} [Ord α] {l : Std.DTreeMap.Internal.Impl α fun x => β} {he : l.isEmpty = false},
  some (Std.DTreeMap.Internal.Impl.Const.maxEntry l he) = Std.DTreeMap.Internal.Impl.Const.maxEntry? l
-- Init.Data.UInt.Lemmas
instLawfulCommIdentityUInt8HMulOfNat : Std.LawfulCommIdentity (fun x1 x2 => x1 * x2) 1
-- Lean.Parser.Extension
/-- Resolve the given parser name and return a list of candidates.  -/
Lean.Parser.ParserContext.resolveParserName : Lean.Parser.ParserContext → Lean.Ident → optParam Bool false → List Lean.Parser.ParserResolution
-- Mathlib.CategoryTheory.Monoidal.Bimon_
/-- Auxiliary definition for `equivMonComonUnitIsoApp`.  -/
CategoryTheory.Bimon.equivMonComonUnitIsoAppXAux : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    [inst_1 : CategoryTheory.MonoidalCategory C] →
      [inst_2 : CategoryTheory.BraidedCategory C] →
        (M : CategoryTheory.Bimon C) →
          M.X.X ≅ (((CategoryTheory.Bimon.toMonComon C).comp (CategoryTheory.Bimon.ofMonComon C)).obj M).X.X
-- Lean.Elab.AutoBound
Lean.Elab.autoImplicit : Lean.Option Bool
-- Mathlib.Algebra.Group.Defs
/-- An additive monoid in which addition is left-cancellative.
Main examples are `ℕ` and groups. This is the right typeclass for many sum lemmas, as having a zero
is useful to define the sum over the empty set, so `AddLeftCancelSemigroup` is not enough.  -/
AddLeftCancelMonoid : Type u → Type u
-- Mathlib.RingTheory.HahnSeries.Lex
HahnSeries.finiteArchimedeanClassOrderIso.eq_1 : ∀ (Γ : Type u_1) (R : Type u_2) [inst : LinearOrder Γ] [inst_1 : LinearOrder R] [inst_2 : AddCommGroup R]
  [inst_3 : IsOrderedAddMonoid R] [inst_4 : Archimedean R] [inst_5 : Nontrivial R],
  HahnSeries.finiteArchimedeanClassOrderIso Γ R =
    (HahnSeries.finiteArchimedeanClassOrderIsoLex Γ R).trans (Prod.Lex.prodUnique Γ (FiniteArchimedeanClass R))
-- Mathlib.MeasureTheory.Measure.Typeclasses.NullSingletonClass
MeasureTheory.Ioo_ae_eq_Icc : ∀ {α : Type u_1} {m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} [MeasureTheory.NullSingletonClass μ]
  [inst : PartialOrder α] {a b : α}, Set.Ioo a b =ᵐ[μ] Set.Icc a b
-- Mathlib.Combinatorics.SimpleGraph.Matching
SimpleGraph.Subgraph.IsMatching.not_adj_left_of_ne : ∀ {V : Type u_1} {G : SimpleGraph V} {M : G.Subgraph} {u v w : V}, M.IsMatching → v ≠ w → M.Adj u v → ¬M.Adj u w
-- Init.Data.BitVec.Bitblast
/-- Carry function for bitwise addition.  -/
BitVec.adcb : Bool → Bool → Bool → Bool × Bool
-- Mathlib.Algebra.Algebra.Operations
Submodule.smul_bot : ∀ {R : Type u} [inst : Semiring R] {A : Type v} [inst_1 : Semiring A] [inst_2 : Module R A] {M : Type u_1}
  [inst_3 : AddCommMonoid M] [inst_4 : Module R M] [inst_5 : Module A M] [inst_6 : IsScalarTower R A M]
  (I : Submodule R A), I • ⊥ = ⊥