mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Algebra.Order.AbsoluteValue.Basic
AbsoluteValue.trivial_apply : ∀ {R : Type u_5} [inst : Semiring R] [inst_1 : DecidablePred fun x => x = 0] [inst_2 : NoZeroDivisors R] {S : Type u_6}
  [inst_3 : Semiring S] [inst_4 : PartialOrder S] [inst_5 : IsOrderedRing S] [inst_6 : Nontrivial S] {x : R},
  x ≠ 0 → AbsoluteValue.trivial x = 1
-- Mathlib.Algebra.Group.Semiconj.Defs
/-- The relation “there exists an element that semiconjugates `a` to `b`” on an
additive monoid (or, more generally, on an `AddZeroClass` type) is reflexive.  -/
AddSemiconjBy.refl : ∀ {M : Type u_2} [inst : AddZeroClass M], Std.Refl fun a b => ∃ c, AddSemiconjBy c a b
-- Mathlib.FieldTheory.Minpoly.ConjRootClass
ConjRootClass.minpoly_ne_zero : ∀ {K : Type u_1} {L : Type u_2} [inst : Field K] [inst_1 : Field L] [inst_2 : Algebra K L] [Algebra.IsAlgebraic K L]
  (c : ConjRootClass K L), c.minpoly ≠ 0
-- Mathlib.CategoryTheory.Skeletal
CategoryTheory.Skeleton.comp_hom_assoc : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {X Y Z : CategoryTheory.Skeleton C} (f : X ⟶ Y) (g : Y ⟶ Z)
  {Z_1 : C} (h : Quotient.out Z ⟶ Z_1),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.CategoryStruct.comp f g).hom h =
    CategoryTheory.CategoryStruct.comp f.hom (CategoryTheory.CategoryStruct.comp g.hom h)
-- Std.Data.TreeSet.Basic
/-- Transforms an array into a tree set.  -/
Std.TreeSet.ofArray : {α : Type u} → Array α → (cmp : autoParam (α → α → Ordering) Std.TreeSet.ofArray._auto_1) → Std.TreeSet α cmp
-- Lean.Meta.Basic
/-- Reduces an expression to its *weak head normal form*.
This is when the "head" of the top-level expression has been fully reduced.
The result may contain subexpressions that have not been reduced.

See `Lean.Meta.whnfImp` for the implementation.
 -/
Lean.Meta.whnf : Lean.Expr → Lean.MetaM Lean.Expr
-- Batteries.Data.List.Basic
List.sigmaTR.eq_1 : ∀ {α : Type u_1} {σ : α → Type u_2} (l₁ : List α) (l₂ : (a : α) → List (σ a)),
  l₁.sigmaTR l₂ = (List.foldl (fun acc a => List.foldl (fun acc b => acc.push ⟨a, b⟩) acc (l₂ a)) #[] l₁).toList
-- Mathlib.RingTheory.Ideal.IsPrincipal
Ideal.associatesEquivIsPrincipal_map_zero : ∀ {R : Type u_1} [inst : CommRing R] [inst_1 : IsDomain R], ↑((Ideal.associatesEquivIsPrincipal R) 0) = 0
-- Mathlib.Algebra.Group.Subgroup.Even
AddSubsemigroup.mem_even : ∀ {S : Type u_1} [inst : AddCommSemigroup S] {a : S}, a ∈ AddSubsemigroup.even S ↔ Even a
-- Init.Data.List.MinMaxIdx
List.minIdxOn_nil_eq_iff_true : ∀ {β : Type u_1} {α : Type u_2} [inst : LE β] [inst_1 : DecidableLE β] {f : α → β} {x : ℕ} (h : [] ≠ []),
  List.minIdxOn f [] h = x ↔ True
-- Std.Data.DTreeMap.Internal.Lemmas
Std.DTreeMap.Internal.Impl.Const.toList_toArray : ∀ {α : Type u} {β : Type v} {t : Std.DTreeMap.Internal.Impl α fun x => β},
  (Std.DTreeMap.Internal.Impl.Const.toArray t).toList = Std.DTreeMap.Internal.Impl.Const.toList t
-- Mathlib.Computability.TuringMachine.PostTuringMachine
Turing.TM1.Stmt.load.sizeOf_spec : ∀ {Γ : Type u_1} {Λ : Type u_2} {σ : Type u_3} [inst : SizeOf Γ] [inst_1 : SizeOf Λ] [inst_2 : SizeOf σ] (a : Γ → σ → σ)
  (a_1 : Turing.TM1.Stmt Γ Λ σ), sizeOf (Turing.TM1.Stmt.load a a_1) = 1 + sizeOf a_1
-- Std.Data.Iterators.Lemmas.Equivalence.HetT
Std.Internal.instSmall : ∀ {α : Type v}, Std.Internal.Small α
-- Std.Sat.AIG.Basic
Std.Sat.AIG.ArbitraryShiftTarget.mk.injEq : ∀ {α : Type} [inst : Hashable α] [inst_1 : DecidableEq α] {aig : Std.Sat.AIG α} {m : ℕ} (n : ℕ) (target : aig.RefVec m)
  (distance : aig.RefVec n) (n_1 : ℕ) (target_1 : aig.RefVec m) (distance_1 : aig.RefVec n_1),
  ({ n := n, target := target, distance := distance } = { n := n_1, target := target_1, distance := distance_1 }) =
    (n = n_1 ∧ target = target_1 ∧ distance ≍ distance_1)
-- Mathlib.CategoryTheory.Limits.Types.Equalizers
CategoryTheory.Limits.Types.equalizerIso_inv_comp_ι_apply : ∀ {Y Z : Type u} (g h : Y ⟶ Z)
  (x : { x // (CategoryTheory.ConcreteCategory.hom g) x = (CategoryTheory.ConcreteCategory.hom h) x }),
  (CategoryTheory.ConcreteCategory.hom (CategoryTheory.Limits.equalizer.ι g h))
      ((CategoryTheory.ConcreteCategory.hom (CategoryTheory.Limits.Types.equalizerIso g h).inv) x) =
    ↑x
-- Mathlib.AlgebraicGeometry.PullbackCarrier
AlgebraicGeometry.Scheme.Pullback.Triplet.instNontrivialCarrierTensor : ∀ {X Y S : AlgebraicGeometry.Scheme} {f : X ⟶ S} {g : Y ⟶ S} (T : AlgebraicGeometry.Scheme.Pullback.Triplet f g),
  Nontrivial ↑T.tensor
-- Mathlib.Algebra.Category.CommHopfAlgCat
CommHopfAlgCat.ofIso_apply : ∀ {R : Type u} [inst : CommRing R] {A B : CommHopfAlgCat R} (i : A ≅ B) (a : ↑A),
  (CommHopfAlgCat.ofIso i) a = (CategoryTheory.ConcreteCategory.hom i.hom) a
-- Mathlib.MeasureTheory.Function.ConditionalExpectation.AEMeasurable
MeasureTheory.lpMeas.aestronglyMeasurable : ∀ {α : Type u_1} {F : Type u_2} {𝕜 : Type u_3} {p : ENNReal} [inst : RCLike 𝕜] [inst_1 : NormedAddCommGroup F]
  [inst_2 : NormedSpace 𝕜 F] {m x : MeasurableSpace α} {μ : MeasureTheory.Measure α}
  (f : ↥(MeasureTheory.lpMeas F 𝕜 m p μ)), MeasureTheory.AEStronglyMeasurable (↑↑↑f) μ
-- Init.Data.Int.DivMod.Lemmas
Int.dvd_antisymm : ∀ {a b : ℤ}, 0 ≤ a → 0 ≤ b → a ∣ b → b ∣ a → a = b
-- Std.Data.DTreeMap.Raw.Lemmas
Std.DTreeMap.Raw.Const.get!_eq_default_of_contains_eq_false : ∀ {α : Type u} {cmp : α → α → Ordering} {β : Type v} {t : Std.DTreeMap.Raw α (fun x => β) cmp} [Std.TransCmp cmp]
  [inst : Inhabited β], t.WF → ∀ {a : α}, t.contains a = false → Std.DTreeMap.Raw.Const.get! t a = default
-- Mathlib.Topology.Algebra.Group.ClosedSubgroup
ClosedSubgroup.ext : ∀ {G : Type u} {inst : Group G} {inst_1 : TopologicalSpace G} {x y : ClosedSubgroup G},
  (↑x).carrier = (↑y).carrier → x = y
-- Mathlib.NumberTheory.NumberField.CanonicalEmbedding.NormLeOne
NumberField.mixedEmbedding.fundamentalCone.completeFamily.congr_simp : ∀ (K : Type u_1) [inst : Field K] [inst_1 : NumberField K] (a a_1 : NumberField.InfinitePlace K),
  a = a_1 →
    ∀ (a_2 a_3 : NumberField.InfinitePlace K),
      a_2 = a_3 →
        NumberField.mixedEmbedding.fundamentalCone.completeFamily K a a_2 =
          NumberField.mixedEmbedding.fundamentalCone.completeFamily K a_1 a_3
-- Mathlib.Data.Part
Part.Dom.bind : ∀ {α : Type u_1} {β : Type u_2} {o : Part α} (h : o.Dom) (f : α → Part β), o.bind f = f (o.get h)
-- Mathlib.NumberTheory.PellMatiyasevic
/-- The Pell sequences, i.e. the sequence of integer solutions to `x ^ 2 - d * y ^ 2 = 1`, where
`d = a ^ 2 - 1`, defined together in mutual recursion.  -/
Pell.pell : {a : ℕ} → 1 < a → ℕ → ℕ × ℕ
-- Mathlib.Data.List.Sort
/-- **Alias** of the reverse direction of `List.sortedLE_iff_isChain`. -/
List.IsChain.sortedLE : ∀ {α : Type u_1} {l : List α} [inst : Preorder α], List.IsChain (fun x1 x2 => x1 ≤ x2) l → l.SortedLE
-- Std.Internal.UV.System
Std.Internal.UV.System.CPUTimes.mk : UInt64 → UInt64 → UInt64 → UInt64 → UInt64 → Std.Internal.UV.System.CPUTimes
-- Mathlib.CategoryTheory.Comma.Final
/-- Let the following diagram commute up to isomorphism:

```
      L       R
  A  ---→ T  ←--- B
  |       |       |
  | F     | H     | G
  ↓       ↓       ↓
  A' ---→ T' ←--- B'
      L'      R'
```

Let `F`, `G`, `R` and `R'` be final and `B` be filtered. Then, the induced functor between the comma
categories of the first and second row of the diagram is final.  -/
CategoryTheory.Comma.map_final : ∀ {A : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} A] {B : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} B]
  {T : Type u₃} [inst_2 : CategoryTheory.Category.{v₃, u₃} T] {L : CategoryTheory.Functor A T}
  {R : CategoryTheory.Functor B T} {A' : Type u₄} [inst_3 : CategoryTheory.Category.{v₄, u₄} A'] {B' : Type u₅}
  [inst_4 : CategoryTheory.Category.{v₅, u₅} B'] {T' : Type u₆} [inst_5 : CategoryTheory.Category.{v₆, u₆} T']
  {L' : CategoryTheory.Functor A' T'} {R' : CategoryTheory.Functor B' T'} {F : CategoryTheory.Functor A A'}
  {G : CategoryTheory.Functor B B'} {H : CategoryTheory.Functor T T'} (iL : F.comp L' ≅ L.comp H)
  (iR : G.comp R' ≅ R.comp H) [CategoryTheory.IsFiltered B] [R.Final] [R'.Final] [F.Final] [G.Final],
  (CategoryTheory.Comma.map iL.hom iR.inv).Final
-- Mathlib.Topology.Algebra.Module.ContinuousLinearMap.Basic
ContinuousLinearMap.neg_comp : ∀ {R : Type u_1} [inst : Ring R] {R₂ : Type u_2} [inst_1 : Ring R₂] {R₃ : Type u_3} [inst_2 : Ring R₃] {M : Type u_4}
  [inst_3 : TopologicalSpace M] [inst_4 : AddCommGroup M] {M₂ : Type u_5} [inst_5 : TopologicalSpace M₂]
  [inst_6 : AddCommGroup M₂] {M₃ : Type u_6} [inst_7 : TopologicalSpace M₃] [inst_8 : AddCommGroup M₃]
  [inst_9 : Module R M] [inst_10 : Module R₂ M₂] [inst_11 : Module R₃ M₃] {σ₁₂ : R →+* R₂} {σ₂₃ : R₂ →+* R₃}
  {σ₁₃ : R →+* R₃} [inst_12 : RingHomCompTriple σ₁₂ σ₂₃ σ₁₃] [inst_13 : IsTopologicalAddGroup M₃] (g : M₂ →SL[σ₂₃] M₃)
  (f : M →SL[σ₁₂] M₂), (-g) ∘SL f = -g ∘SL f
-- Init.Data.Iterators.Lemmas.Combinators.Monadic.Append
Std.IterM.toList_appendSnd : ∀ {α₁ α₂ β : Type w} {m : Type w → Type w'} [inst : Monad m] [LawfulMonad m] [inst_2 : Std.Iterator α₁ m β]
  [inst_3 : Std.Iterator α₂ m β] [Std.Iterators.Finite α₁ m] [Std.Iterators.Finite α₂ m] {it₂ : Std.IterM m β},
  (Std.IterM.Intermediate.appendSnd α₁ it₂).toList = it₂.toList
-- Mathlib.LinearAlgebra.PerfectPairing.Basic
LinearEquiv.symm_flip : ∀ {R : Type u_1} {M : Type u_2} {N : Type u_3} [inst : CommRing R] [inst_1 : AddCommGroup M] [inst_2 : Module R M]
  [inst_3 : AddCommGroup N] [inst_4 : Module R N] [inst_5 : Module.IsReflexive R M] (e : N ≃ₗ[R] Module.Dual R M),
  e.flip.symm = e.symm.dualMap ≪≫ₗ (Module.evalEquiv R M).symm
-- Mathlib.RingTheory.TensorProduct.Basic
Algebra.TensorProduct.sMulCommClass_right : ∀ {R : Type uR} {S : Type uS} {A : Type uA} {B : Type uB} [inst : CommSemiring R] [inst_1 : NonUnitalNonAssocSemiring A]
  [inst_2 : Module R A] [inst_3 : SMulCommClass R A A] [inst_4 : IsScalarTower R A A]
  [inst_5 : NonUnitalNonAssocSemiring B] [inst_6 : Module R B] [inst_7 : SMulCommClass R B B]
  [inst_8 : IsScalarTower R B B] [inst_9 : Monoid S] [inst_10 : DistribMulAction S A] [SMulCommClass S A A]
  [inst_12 : SMulCommClass R S A], SMulCommClass S (TensorProduct R A B) (TensorProduct R A B)
-- Std.Data.DTreeMap.Internal.Lemmas
Std.DTreeMap.Internal.Impl.self_le_maxKey?_insert! : ∀ {α : Type u} {β : α → Type v} {instOrd : Ord α} {t : Std.DTreeMap.Internal.Impl α β} [inst : Std.TransOrd α]
  (h : t.WF) {k : α} {v : β k} {kmi : α},
  (Std.DTreeMap.Internal.Impl.insert! k v t).maxKey?.get ⋯ = kmi → (compare k kmi).isLE = true
-- Mathlib.MeasureTheory.Function.ConditionalExpectation.CondJensen
Set.codRestrict.eq_1 : ∀ {α : Type u_1} {ι : Sort u_5} (f : ι → α) (s : Set α) (h : ∀ (x : ι), f x ∈ s) (x : ι),
  Set.codRestrict f s h x = ⟨f x, ⋯⟩
-- Mathlib.Tactic.DeriveTraversable
/-- derive the `map` definition and declare `Functor` using this.  -/
Mathlib.Deriving.Traversable.deriveFunctor : Lean.MVarId → Lean.Elab.TermElabM Unit
-- Mathlib.NumberTheory.NumberField.House
_private.Mathlib.NumberTheory.NumberField.House.0.NumberField.house.c₁.eq_1 : ∀ (K : Type u_1) [inst : Field K] [inst_1 : NumberField K] [inst_2 : DecidableEq (K →+* ℂ)],
  NumberField.house.c₁✝ K = ↑(Module.finrank ℚ K) * NumberField.house.c₂✝ K
-- Mathlib.Data.Multiset.Fintype
Multiset.instFintypeElemProdNatOfPredLtSndCountFst : {α : Type u_1} → [inst : DecidableEq α] → {m : Multiset α} → Fintype ↑{p | p.2 < Multiset.count p.1 m}
-- Mathlib.CategoryTheory.Monoidal.Opposite.Mon
MonObj.mopEquivCompForgetIso_inv_app_unmop : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.MonoidalCategory C]
  (X : CategoryTheory.Mon C), (MonObj.mopEquivCompForgetIso.inv.app X).unmop = CategoryTheory.CategoryStruct.id X.X
-- Mathlib.RingTheory.Spectrum.Prime.Topology
PrimeSpectrum.instQuasiSeparatedSpace : ∀ {R : Type u} [inst : CommSemiring R], QuasiSeparatedSpace (PrimeSpectrum R)
-- Mathlib.RingTheory.AdicCompletion.Topology
Ideal.ringFilterBasis.eq_1 : ∀ {R : Type u_1} [inst : CommRing R] (I : Ideal R), I.ringFilterBasis = ⋯.toRingFilterBasis
-- Std.Internal.Do.PredTrans
/-- Unfolding `<*>` through `apply`.  -/
Std.Internal.Do.PredTrans.apply_seq : ∀ {α β : Type u_1} {Pred : Type u} {EPred : Type v} (f : Std.Internal.Do.PredTrans Pred EPred (α → β))
  (x : Std.Internal.Do.PredTrans Pred EPred α) (post : β → Pred) (epost : EPred),
  (f <*> x).apply post epost = f.apply (fun g => x.apply (fun a => post (g a)) epost) epost
-- Mathlib.LinearAlgebra.DFinsupp
DFinsupp.mapRange.linearEquiv_refl : ∀ {ι : Type u_1} {R : Type u_3} [inst : Semiring R] {β₁ : ι → Type u_8} [inst_1 : (i : ι) → AddCommMonoid (β₁ i)]
  [inst_2 : (i : ι) → Module R (β₁ i)],
  (DFinsupp.mapRange.linearEquiv fun i => LinearEquiv.refl R (β₁ i)) = LinearEquiv.refl R (Π₀ (i : ι), β₁ i)
-- Mathlib.Topology.Sets.Closeds
TopologicalSpace.IrreducibleCloseds.isClosed : ∀ {α : Type u_2} [inst : TopologicalSpace α] (s : TopologicalSpace.IrreducibleCloseds α), IsClosed ↑s
-- Mathlib.GroupTheory.Torsion
/-- **Alias** of `IsMulTorsion.extension_closed`.

---

Torsion groups are closed under extensions.  -/
IsTorsion.extension_closed : ∀ {G : Type u_1} {H : Type u_2} [inst : Group G] {N : Subgroup G} [inst_1 : Group H] {f : G →* H},
  N = f.ker → IsMulTorsion H → IsMulTorsion ↥N → IsMulTorsion G
-- Mathlib.Probability.Moments.ComplexMGF
/-- If two random variables have the same moment-generating function then they have
the same `integrableExpSet`.  -/
ProbabilityTheory.integrableExpSet_eq_of_mgf' : ∀ {Ω : Type u_1} {m : MeasurableSpace Ω} {X : Ω → ℝ} {μ : MeasureTheory.Measure Ω} {Ω' : Type u_3}
  {mΩ' : MeasurableSpace Ω'} {Y : Ω' → ℝ} {μ' : MeasureTheory.Measure Ω'},
  ProbabilityTheory.mgf X μ = ProbabilityTheory.mgf Y μ' →
    (μ = 0 ↔ μ' = 0) → ProbabilityTheory.integrableExpSet X μ = ProbabilityTheory.integrableExpSet Y μ'
-- Mathlib.Geometry.Manifold.Algebra.SMul
Diffeomorph.smul_apply : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {H : Type u_2} [inst_1 : TopologicalSpace H] {E : Type u_3}
  [inst_2 : NormedAddCommGroup E] [inst_3 : NormedSpace 𝕜 E] {I : ModelWithCorners 𝕜 E H} {H' : Type u_4}
  [inst_4 : TopologicalSpace H'] {E' : Type u_5} [inst_5 : NormedAddCommGroup E'] [inst_6 : NormedSpace 𝕜 E']
  {I' : ModelWithCorners 𝕜 E' H'} {G : Type u_8} [inst_7 : TopologicalSpace G] [inst_8 : ChartedSpace H G]
  {M : Type u_9} [inst_9 : TopologicalSpace M] [inst_10 : ChartedSpace H' M] [inst_11 : Group G]
  [inst_12 : MulAction G M] {n : WithTop ℕ∞} [inst_13 : ContMDiffSMul I I' n G M] (g : G) (x : M),
  (Diffeomorph.smul I I' n g) x = g • x
-- Mathlib.CategoryTheory.SmallObject.Iteration.Basic
CategoryTheory.SmallObject.SuccStruct.Iteration.prop_map_succ : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {J : Type w} {Φ : CategoryTheory.SmallObject.SuccStruct C}
  [inst_1 : LinearOrder J] [inst_2 : SuccOrder J] [inst_3 : OrderBot J]
  [inst_4 : CategoryTheory.Limits.HasIterationOfShape J C] [inst_5 : WellFoundedLT J] {j : J} (iter : Φ.Iteration j)
  (i : J) (hi : i < j), Φ.prop (iter.F.map (CategoryTheory.homOfLE ⋯))
-- Mathlib.Topology.ApproximateUnit
/-- In a topological unital magma, `𝓝 1` is an approximate unit.  -/
Filter.IsApproximateUnit.nhds_one : ∀ (α : Type u_1) [inst : TopologicalSpace α] [inst_1 : MulOneClass α] [SeparatelyContinuousMul α],
  (nhds 1).IsApproximateUnit
-- Init.Data.Option.Array
Option.toList_toArray : ∀ {α : Type u_1} {o : Option α}, o.toArray.toList = o.toList
-- Lean.Data.NameTrie
Lean.NamePart.str.sizeOf_spec : ∀ (s : String), sizeOf (Lean.NamePart.str s) = 1 + sizeOf s
-- Mathlib.Algebra.Group.Submonoid.Units
Submonoid.units.eq_1 : ∀ {M : Type u_1} [inst : Monoid M] (S : Submonoid M),
  S.units =
    { toSubmonoid := Submonoid.comap (Units.coeHom M) S ⊓ (Submonoid.comap (Units.coeHom M) S)⁻¹, inv_mem' := ⋯ }
-- Mathlib.AlgebraicGeometry.ProjectiveSpectrum.Scheme
AlgebraicGeometry.ProjIsoSpecTopComponent.FromSpec.carrier.add_mem : ∀ {A : Type u_1} {σ : Type u_2} [inst : CommRing A] [inst_1 : SetLike σ A] [inst_2 : AddSubgroupClass σ A] {𝒜 : ℕ → σ}
  [inst_3 : GradedRing 𝒜] {f : A} {m : ℕ} (f_deg : f ∈ 𝒜 m)
  (q :
    ↑↑(AlgebraicGeometry.Spec.locallyRingedSpaceObj
            (CommRingCat.of (HomogeneousLocalization.Away 𝒜 f))).toPresheafedSpace)
  {a b : A},
  a ∈ AlgebraicGeometry.ProjIsoSpecTopComponent.FromSpec.carrier f_deg q →
    b ∈ AlgebraicGeometry.ProjIsoSpecTopComponent.FromSpec.carrier f_deg q →
      a + b ∈ AlgebraicGeometry.ProjIsoSpecTopComponent.FromSpec.carrier f_deg q
-- Mathlib.FieldTheory.IntermediateField.Basic
IntermediateField.extendScalars_injective : ∀ {K : Type u_1} {L : Type u_2} [inst : Field K] [inst_1 : Field L] [inst_2 : Algebra K L] (F : IntermediateField K L),
  Function.Injective fun E => IntermediateField.extendScalars ⋯
-- Mathlib.Data.PEquiv
PEquiv.bot_apply : ∀ {α : Type u} {β : Type v} (a : α), ⊥ a = none
-- Mathlib.CategoryTheory.Comma.Over.Basic
CategoryTheory.CostructuredArrow.ofDiagEquivalence.functor_obj_left_left : ∀ {T : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} T] (X : T × T)
  (Y : CategoryTheory.CostructuredArrow (CategoryTheory.Functor.diag T) X),
  ((CategoryTheory.CostructuredArrow.ofDiagEquivalence.functor X).obj Y).left.left = Y.left
-- Std.Time.Internal.Bounded
/-- A `Bounded` integer where the relation used is the less-equal relation, so it includes all
integers that `lo ≤ val ≤ hi`.
 -/
Std.Time.Internal.Bounded.LE : ℤ → ℤ → Type
-- Mathlib.CategoryTheory.MorphismProperty.LiftingProperty
CategoryTheory.MorphismProperty.gc_llp_rlp : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C],
  GaloisConnection (⇑OrderDual.toDual ∘ CategoryTheory.MorphismProperty.llp)
    (CategoryTheory.MorphismProperty.rlp ∘ ⇑OrderDual.ofDual)
-- Mathlib.Analysis.SpecialFunctions.Complex.Circle
/-- The canonical map `fun x => exp (2 π i x / T)` from `ℝ / ℤ • T` to the unit circle in `ℂ`.
If `T = 0` we understand this as the constant function 1.  -/
AddCircle.toCircle : {T : ℝ} → AddCircle T → Circle
-- Mathlib.Topology.Basic
isClosed_univ : ∀ {X : Type u} [inst : TopologicalSpace X], IsClosed Set.univ
-- Mathlib.LinearAlgebra.SpecialLinearGroup
/-- The special linear group of a module is a group.  -/
SpecialLinearGroup.instGroup : {R : Type u_1} →
  {V : Type u_2} →
    [inst : CommRing R] → [inst_1 : AddCommGroup V] → [inst_2 : Module R V] → Group (SpecialLinearGroup R V)
-- Mathlib.Data.PFunctor.Univariate.Basic
/-- The destructor for W-types  -/
PFunctor.W.dest : {P : PFunctor.{uA, uB}} → P.W → ↑P P.W
-- Std.Data.DTreeMap.Lemmas
Std.DTreeMap.Equiv.constGet!_eq : ∀ {α : Type u} {cmp : α → α → Ordering} {β : Type v} {t₁ t₂ : Std.DTreeMap α (fun x => β) cmp} [Std.TransCmp cmp]
  [inst : Inhabited β] {k : α}, t₁.Equiv t₂ → Std.DTreeMap.Const.get! t₁ k = Std.DTreeMap.Const.get! t₂ k
-- Mathlib.RingTheory.Localization.AtPrime.Basic
Localization.localRingEquiv_apply : ∀ {R : Type u_1} [inst : CommSemiring R] {P : Type u_3} [inst_1 : CommSemiring P] (I : Ideal R) [hI : I.IsPrime]
  (J : Ideal P) [inst_2 : J.IsPrime] (f : R ≃+* P) (hIJ : I = Ideal.comap f J) (a : Localization.AtPrime I),
  (Localization.localRingEquiv I J f hIJ) a = (↑↑(Localization.localRingHom I J (↑f) hIJ)).toFun a
-- Mathlib.Data.Vector.MapLemmas
List.Vector.map_eq_mapAccumr : ∀ {α : Type u_1} {β : Type u_2} {n : ℕ} {xs : List.Vector α n} {f : α → β},
  List.Vector.map f xs = (List.Vector.mapAccumr (fun x x_1 => ((), f x)) xs ()).2
-- Lean.Meta.Tactic.Grind.Arith.Cutsat.Util
Lean.Meta.Grind.Arith.Cutsat.isIntTerm : Lean.Expr → Lean.Meta.Grind.GoalM Bool
-- Std.Data.TreeMap.Raw.Lemmas
Std.TreeMap.Raw.minKey?_bind_getKey? : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Std.TreeMap.Raw α β cmp} [Std.TransCmp cmp],
  t.WF → t.minKey?.bind t.getKey? = t.minKey?
-- Init.Data.UInt.Bitwise
instCommutativeUInt32HXor : Std.Commutative fun x1 x2 => x1 ^^^ x2
-- Batteries.Recycling.RBTree.Basic
/-- `O(1)`. Is the tree empty?  -/
RBTree.RBMap.isEmpty : {α : Type u} → {β : Type v} → {cmp : α → α → Ordering} → RBTree.RBMap α β cmp → Bool
-- Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.NonUnital
cfcₙ_smul : ∀ {R : Type u_1} {A : Type u_2} {p : A → Prop} [inst : CommSemiring R] [inst_1 : Nontrivial R] [inst_2 : StarRing R]
  [inst_3 : MetricSpace R] [inst_4 : IsTopologicalSemiring R] [inst_5 : ContinuousStar R] [inst_6 : NonUnitalRing A]
  [inst_7 : StarRing A] [inst_8 : TopologicalSpace A] [inst_9 : Module R A] [inst_10 : IsScalarTower R A A]
  [inst_11 : SMulCommClass R A A] [instCFCₙ : NonUnitalContinuousFunctionalCalculus R A p] {S : Type u_3}
  [inst_12 : SMulZeroClass S R] [ContinuousConstSMul S R] [inst_14 : SMulZeroClass S A] [IsScalarTower S R A]
  [IsScalarTower S R (R → R)] (s : S) (f : R → R) (a : A),
  autoParam (ContinuousOn f (quasispectrum R a)) cfcₙ_smul._auto_1 →
    autoParam (f 0 = 0) cfcₙ_smul._auto_3 → cfcₙ (fun x => s • f x) a = s • cfcₙ f a
-- Batteries.Recycling.RBTree.Lemmas
RBTree.RBMap.foldr_eq_foldr_toList : ∀ {α : Type u_1} {β : Type u_2} {cmp : α → α → Ordering} {α_1 : Type u_3} {f : α → β → α_1 → α_1} {init : α_1}
  {t : RBTree.RBMap α β cmp}, RBTree.RBMap.foldr f init t = List.foldr (fun p r => f p.1 p.2 r) init t.toList
-- Mathlib.Algebra.Star.NonUnitalSubalgebra
NonUnitalStarSubalgebra.coe_neg : ∀ {R : Type u} {A : Type v} [inst : CommRing R] [inst_1 : NonUnitalNonAssocRing A] [inst_2 : Module R A]
  [inst_3 : Star A] {S : NonUnitalStarSubalgebra R A} (x : ↥S), ↑(-x) = -↑x
-- Mathlib.Order.Filter.CountablyGenerated
Filter.HasAntitoneBasis.mem : ∀ {α : Type u_1} {ι : Type u_4} [inst : Preorder ι] {l : Filter α} {s : ι → Set α},
  l.HasAntitoneBasis s → ∀ (i : ι), s i ∈ l
-- Mathlib.Logic.Equiv.Prod
Equiv.pprodEquivProdPLift_symm_apply : ∀ {α : Sort u_1} {β : Sort u_4} (a : PLift α × PLift β), Equiv.pprodEquivProdPLift.symm a = ⟨a.1.down, a.2.down⟩
-- Mathlib.MeasureTheory.Function.AEEqOfIntegral
MeasureTheory.AEFinStronglyMeasurable.ae_eq_zero_of_forall_setIntegral_eq_zero : ∀ {α : Type u_1} {E : Type u_2} {m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} [inst : NormedAddCommGroup E]
  [inst_1 : NormedSpace ℝ E] [CompleteSpace E] {f : α → E},
  (∀ (s : Set α), MeasurableSet s → μ s < ⊤ → MeasureTheory.IntegrableOn f s μ) →
    (∀ (s : Set α), MeasurableSet s → μ s < ⊤ → ∫ (x : α) in s, f x ∂μ = 0) →
      MeasureTheory.AEFinStronglyMeasurable f μ → f =ᵐ[μ] 0
-- Mathlib.Algebra.Order.Module.HahnEmbedding
HahnEmbedding.Seed.mk.inj : ∀ {K : Type u_1} {inst : DivisionRing K} {inst_1 : LinearOrder K} {inst_2 : IsOrderedRing K} {inst_3 : Archimedean K}
  {M : Type u_2} {inst_4 : AddCommGroup M} {inst_5 : LinearOrder M} {inst_6 : IsOrderedAddMonoid M}
  {inst_7 : Module K M} {inst_8 : IsOrderedModule K M} {R : Type u_3} {inst_9 : AddCommGroup R}
  {inst_10 : LinearOrder R} {inst_11 : Module K R} {toArchimedeanStrata : HahnEmbedding.ArchimedeanStrata K M}
  {coeff : (c : FiniteArchimedeanClass M) → ↥(toArchimedeanStrata.stratum c) →ₗ[K] R}
  {strictMono_coeff : ∀ (c : FiniteArchimedeanClass M), StrictMono ⇑(coeff c)}
  {toArchimedeanStrata_1 : HahnEmbedding.ArchimedeanStrata K M}
  {coeff_1 : (c : FiniteArchimedeanClass M) → ↥(toArchimedeanStrata_1.stratum c) →ₗ[K] R}
  {strictMono_coeff_1 : ∀ (c : FiniteArchimedeanClass M), StrictMono ⇑(coeff_1 c)},
  { toArchimedeanStrata := toArchimedeanStrata, coeff := coeff, strictMono_coeff := strictMono_coeff } =
      { toArchimedeanStrata := toArchimedeanStrata_1, coeff := coeff_1, strictMono_coeff := strictMono_coeff_1 } →
    toArchimedeanStrata = toArchimedeanStrata_1 ∧ coeff ≍ coeff_1
-- Mathlib.CategoryTheory.Category.Quiv
CategoryTheory.Quiv.freeMap_pathsOf_pathComposition : ∀ (V : Type u) [inst : Quiver V],
  (CategoryTheory.Cat.freeMap (CategoryTheory.Paths.of V)).comp
      (CategoryTheory.pathComposition (CategoryTheory.Paths V)) =
    CategoryTheory.Functor.id (CategoryTheory.Paths V)
-- Lean.Data.Lsp.LanguageFeatures
Lean.Lsp.WorkspaceSymbolParams.mk.inj : ∀ {query query_1 : String}, { query := query } = { query := query_1 } → query = query_1