mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Analysis.Normed.Module.Alternating.Uncurry.Fin
ContinuousLinearMap.postcomp.congr_simp : ∀ {𝕜₁ : Type u_1} {𝕜₂ : Type u_2} {𝕜₃ : Type u_3} [inst : NormedField 𝕜₁] [inst_1 : NormedField 𝕜₂]
  [inst_2 : NormedField 𝕜₃] {σ : 𝕜₁ →+* 𝕜₂} {τ : 𝕜₂ →+* 𝕜₃} {ρ : 𝕜₁ →+* 𝕜₃} [inst_3 : RingHomCompTriple σ τ ρ]
  (E : Type u_4) {F : Type u_5} {G : Type u_6} [inst_4 : AddCommGroup E] [inst_5 : Module 𝕜₁ E]
  [inst_6 : AddCommGroup F] [inst_7 : Module 𝕜₂ F] [inst_8 : AddCommGroup G] [inst_9 : Module 𝕜₃ G]
  [inst_10 : TopologicalSpace E] [inst_11 : TopologicalSpace F] [inst_12 : TopologicalSpace G]
  [inst_13 : IsTopologicalAddGroup F] [inst_14 : IsTopologicalAddGroup G] [inst_15 : ContinuousConstSMul 𝕜₃ G]
  [inst_16 : ContinuousConstSMul 𝕜₂ F] (L L_1 : F →SL[τ] G),
  L = L_1 → ContinuousLinearMap.postcomp E L = ContinuousLinearMap.postcomp E L_1
-- Mathlib.GroupTheory.PushoutI
Monoid.PushoutI.NormalWord.of_smul_eq_smul : ∀ {ι : Type u_1} {G : ι → Type u_2} {H : Type u_3} [inst : (i : ι) → Group (G i)] [inst_1 : Group H]
  {φ : (i : ι) → H →* G i} {d : Monoid.PushoutI.NormalWord.Transversal φ} [inst_2 : DecidableEq ι]
  [inst_3 : (i : ι) → DecidableEq (G i)] {i : ι} (g : G i) (w : Monoid.PushoutI.NormalWord d),
  (Monoid.PushoutI.of i) g • w = g • w
-- Mathlib.Order.Interval.Finset.Defs
Finset.Ioi_toDual : ∀ {α : Type u_1} [inst : Preorder α] [inst_1 : LocallyFiniteOrderBot α] (a : α),
  Finset.Ioi (OrderDual.toDual a) = Finset.map OrderDual.toDual.toEmbedding (Finset.Iio a)
-- Mathlib.Order.Basic
Ne.lt_or_gt : ∀ {α : Type u_2} [inst : LinearOrder α] {a b : α}, a ≠ b → a < b ∨ b < a
-- Init.Data.Order.Classes
Std.IsPreorder.le_refl : ∀ {α : Type u} {inst : LE α} [self : Std.IsPreorder α] (a : α), a ≤ a
-- Mathlib.Tactic.ComputeAsymptotics.Lemmas
Tactic.ComputeAsymptotics.tendsto_nhdsLT_of_tendsto_atTop : ∀ {α : Type u_1} {𝕜 : Type u_2} [inst : Field 𝕜] [inst_1 : LinearOrder 𝕜] [IsStrictOrderedRing 𝕜]
  [inst_3 : TopologicalSpace 𝕜] [OrderTopology 𝕜] {l : Filter α} (f : 𝕜 → α) (c : 𝕜),
  Filter.Tendsto (fun x => f (c - x⁻¹)) Filter.atTop l → Filter.Tendsto f (nhdsWithin c (Set.Iio c)) l
-- Mathlib.Algebra.Order.ToIntervalMod
toIcoMod_sub : ∀ {α : Type u_1} [inst : AddCommGroup α] [inst_1 : LinearOrder α] [inst_2 : IsOrderedAddMonoid α] [hα : Archimedean α]
  {p : α} (hp : 0 < p) (a b : α), toIcoMod hp a (b - p) = toIcoMod hp a b
-- Mathlib.Order.UpperLower.CompleteLattice
LowerSet.mem_top : ∀ {α : Type u_1} [inst : LE α] {a : α}, a ∈ ⊤
-- Mathlib.RingTheory.Unramified.Finite
/-- If `S` is an unramified `R`-algebra, then `R`-projective implies `S`-projective.  -/
Algebra.FormallyUnramified.projective_of_restrictScalars : ∀ (R : Type u_1) (S : Type u_2) [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : Algebra R S] (M : Type u_3)
  [inst_3 : AddCommGroup M] [inst_4 : Module R M] [inst_5 : Module S M] [IsScalarTower R S M]
  [Algebra.FormallyUnramified R S] [Algebra.EssFiniteType R S] [Module.Projective R M], Module.Projective S M
-- Lean.Meta.Tactic.Backtrack
/-- A wrapper around `run`, which works on "independent" goals separately first,
to reduce backtracking.
 -/
_private.Lean.Meta.Tactic.Backtrack.0.Lean.Meta.Tactic.Backtrack.Backtrack.processIndependentGoals : Lean.Meta.Tactic.Backtrack.BacktrackConfig →
  optParam Lean.Name Lean.Name.anonymous →
    (Lean.MVarId → (List Lean.MVarId → Lean.MetaM (Option (List Lean.MVarId))) → Lean.MetaM (List Lean.MVarId)) →
      List Lean.MVarId → List Lean.MVarId → List Lean.MVarId → Lean.MetaM (List Lean.MVarId)
-- Std.Data.DHashMap.RawLemmas
Std.DHashMap.Raw.Const.all_eq_true_iff_forall_mem_get : ∀ {α : Type u} [inst : BEq α] [inst_1 : Hashable α] {β : Type v} {m : Std.DHashMap.Raw α fun x => β} [LawfulBEq α]
  {p : α → β → Bool}, m.WF → (m.all p = true ↔ ∀ (a : α) (h : a ∈ m), p a (Std.DHashMap.Raw.Const.get m a h) = true)
-- Mathlib.Data.List.Map2
List.zipLeft_nil_right : ∀ {α : Type u} {β : Type v} (as : List α), as.zipLeft [] = List.map (fun a => (a, none)) as
-- Mathlib.RingTheory.Nilpotent.Exp
IsNilpotent.isUnit_exp : ∀ {A : Type u_1} [inst : Ring A] [inst_1 : Module ℚ A] {a : A}, IsNilpotent a → IsUnit (IsNilpotent.exp a)
-- Lean.Server.FileWorker.SemanticHighlighting
/-- Handles a new token. First, `untilToken` is called, which takes care of all transitions that are due
to token boundaries prior to the start of `t`. After that `t`'s priority is compared to the current
token (if any), and then the highest-priority of the two is made current with the other relegated to
the surrounding tokens list. If `t` and the current token have the same priority, then the one that
starts later or ends earlier is made into the new current token.
 -/
_private.Lean.Server.FileWorker.SemanticHighlighting.0.Lean.Server.FileWorker.HandleOverlapState.token : Lean.Server.FileWorker.HandleOverlapState✝ →
  Lean.Server.FileWorker.AbsoluteLspSemanticToken → Lean.Server.FileWorker.HandleOverlapState✝
-- Mathlib.Algebra.Lie.Subalgebra
LieSubalgebra.top_toSubmodule : ∀ {R : Type u} {L : Type v} [inst : CommRing R] [inst_1 : LieRing L] [inst_2 : LieAlgebra R L], ⊤.toSubmodule = ⊤
-- Mathlib.Algebra.Group.Pi.Basic
Sum.elim_zero_zero : ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} [inst : Zero γ], Sum.elim 0 0 = 0
-- Mathlib.Logic.Encodable.Basic
_private.Mathlib.Logic.Encodable.Basic.0.Encodable.encodeSum.match_1.eq_2 : ∀ {α : Type u_1} {β : Type u_2} (motive : α ⊕ β → Sort u_3) (b : β) (h_1 : (a : α) → motive (Sum.inl a))
  (h_2 : (b : β) → motive (Sum.inr b)),
  (match Sum.inr b with
    | Sum.inl a => h_1 a
    | Sum.inr b => h_2 b) =
    h_2 b
-- Aesop.Forward.SlotIndex
Aesop.SlotIndex.mk.injEq : ∀ (toNat toNat_1 : ℕ), ({ toNat := toNat } = { toNat := toNat_1 }) = (toNat = toNat_1)
-- Mathlib.Computability.Primrec.List
Nat.Primrec'.pred : Nat.Primrec' fun v => v.head.pred
-- Mathlib.AlgebraicGeometry.EllipticCurve.Reduction
WeierstrassCurve.IsIntegral.integral : ∀ {R : Type u_1} {inst : CommRing R} {K : Type u_2} {inst_1 : Field K} {inst_2 : Algebra R K} {W : WeierstrassCurve K}
  [self : WeierstrassCurve.IsIntegral R W], ∃ W_int, W = W_int.baseChange K
-- Mathlib.CategoryTheory.Limits.Shapes.Equalizers
/-- Satisfying the inhabited linter  -/
CategoryTheory.Limits.instInhabitedWalkingParallelPairHomZeroOne : Inhabited
  (CategoryTheory.Limits.WalkingParallelPairHom CategoryTheory.Limits.WalkingParallelPair.zero
    CategoryTheory.Limits.WalkingParallelPair.one)
-- Mathlib.Analysis.Calculus.FDeriv.Defs
hasFDerivAtFilter_iff_isLittleO : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : SeminormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {F : Type u_3} [inst_3 : SeminormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F] {f : E → F}
  {f' : E →L[𝕜] F} {L : Filter (E × E)},
  HasFDerivAtFilter f f' L ↔ (fun p => f p.1 - f p.2 - f' (p.1 - p.2)) =o[L] fun p => p.1 - p.2
-- Mathlib.AlgebraicGeometry.Pullbacks
AlgebraicGeometry.Scheme.Pullback.gluedLift.eq_1 : ∀ {X Y Z : AlgebraicGeometry.Scheme} (𝒰 : X.OpenCover) (f : X ⟶ Z) (g : Y ⟶ Z)
  [inst : ∀ (i : 𝒰.I₀), CategoryTheory.Limits.HasPullback (CategoryTheory.CategoryStruct.comp (𝒰.f i) f) g]
  (s : CategoryTheory.Limits.PullbackCone f g),
  AlgebraicGeometry.Scheme.Pullback.gluedLift 𝒰 f g s =
    AlgebraicGeometry.Scheme.Cover.glueMorphisms (CategoryTheory.Precoverage.ZeroHypercover.pullback₁ s.fst 𝒰)
      (fun i =>
        CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pullbackSymmetry s.fst (𝒰.f i)).hom
          (CategoryTheory.CategoryStruct.comp
            (CategoryTheory.Limits.pullback.map (𝒰.f i) s.fst (CategoryTheory.CategoryStruct.comp (𝒰.f i) f) g
              (CategoryTheory.CategoryStruct.id (𝒰.X i)) s.snd f ⋯ ⋯)
            ((AlgebraicGeometry.Scheme.Pullback.gluing 𝒰 f g).ι i)))
      ⋯
-- Mathlib.NumberTheory.NumberField.Completion.FinitePlace
/-- **Alias** of `NumberField.HeightOneSpectrum.adicAbv`.

---

The `v`-adic absolute value on `K` defined as the norm of `v` raised to negative `v`-adic
valuation  -/
NumberField.RingOfIntegers.HeightOneSpectrum.adicAbv : (K : Type u_1) →
  [inst : Field K] →
    {R : Type u_2} →
      [inst_1 : CommRing R] →
        [inst_2 : Algebra R K] →
          [IsDedekindDomain R] →
            [IsFractionRing R K] →
              IsDedekindDomain.HeightOneSpectrum R → [Module.Finite ℤ R] → [Module.Free ℤ R] → AbsoluteValue K ℝ
-- Std.Data.ExtTreeMap.Lemmas
Std.ExtTreeMap.filter_eq_self_iff : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Std.ExtTreeMap α β cmp} [inst : Std.TransCmp cmp]
  {f : α → β → Bool}, Std.ExtTreeMap.filter f t = t ↔ ∀ (k : α) (h : k ∈ t), f (t.getKey k h) t[k] = true
-- Mathlib.Data.Multiset.Defs
/-- `a ∈ s` means that `a` has nonzero multiplicity in `s`.  -/
Multiset.Mem : {α : Type u_1} → Multiset α → α → Prop
-- Mathlib.Algebra.Homology.ShortComplex.LeftHomology
CategoryTheory.ShortComplex.isIso_cyclesMap_of_isIso_of_mono' : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  {S₁ S₂ : CategoryTheory.ShortComplex C} (φ : S₁ ⟶ S₂),
  CategoryTheory.IsIso φ.τ₂ →
    CategoryTheory.Mono φ.τ₃ →
      ∀ [inst_2 : S₁.HasLeftHomology] [inst_3 : S₂.HasLeftHomology],
        CategoryTheory.IsIso (CategoryTheory.ShortComplex.cyclesMap φ)
-- Mathlib.AlgebraicGeometry.Scheme
AlgebraicGeometry.Scheme.Hom.appLE_map_assoc : ∀ {X Y : AlgebraicGeometry.Scheme} (f : X ⟶ Y) {U : Y.Opens} {V V' : X.Opens}
  (e : V ≤ (TopologicalSpace.Opens.map f.base).obj U) (i : Opposite.op V ⟶ Opposite.op V') {Z : CommRingCat}
  (h : X.presheaf.obj (Opposite.op V') ⟶ Z),
  CategoryTheory.CategoryStruct.comp (AlgebraicGeometry.Scheme.Hom.appLE f U V e)
      (CategoryTheory.CategoryStruct.comp (X.presheaf.map i) h) =
    CategoryTheory.CategoryStruct.comp (AlgebraicGeometry.Scheme.Hom.appLE f U V' ⋯) h
-- Lean.Compiler.InitAttr
_private.Lean.Compiler.InitAttr.0.Lean.isIOUnit : Lean.Expr → Bool
-- Std.Data.DTreeMap.Basic
/-- Checks if a mapping for the given key exists and returns the key if it does, otherwise `fallback`.
If a mapping exists the result is guaranteed to be pointer equal to the key in the map.
 -/
Std.DTreeMap.getKeyD : {α : Type u} → {β : α → Type v} → {cmp : α → α → Ordering} → Std.DTreeMap α β cmp → α → α → α
-- Mathlib.Analysis.SpecialFunctions.Trigonometric.Complex
/-- `tan (x / 2)` takes the junk value `0` when `sin x = 0` so this always holds.  -/
Complex.sin_eq_two_mul_tan_half_div_one_add_tan_half_sq : ∀ (x : ℂ), Complex.sin x = 2 * Complex.tan (x / 2) / (1 + Complex.tan (x / 2) ^ 2)
-- Mathlib.Tactic.TacticAnalysis
/-- The tactic analysis framework hooks into the linter to run analysis rounds on sequences
of tactics.
This can be used for linting, or in a more batch-like mode to report potential refactors.
 -/
linter.tacticAnalysis : Lean.Option Bool
-- Mathlib.CategoryTheory.Limits.Types.PreservesLimit
CategoryTheory.Presheaf.coconePtToShrinkYoneda_comp : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {J : Type u'} [inst_1 : CategoryTheory.Category.{v', u'} J]
  [inst_2 : CategoryTheory.LocallySmall.{w, v, u} C] {F : CategoryTheory.Functor J Cᵒᵖ}
  (c : CategoryTheory.Limits.Cone F)
  {c' : CategoryTheory.Limits.Cocone (F.leftOp.comp CategoryTheory.shrinkYoneda.{w, v, u})}
  (hc' : CategoryTheory.Limits.IsColimit c') {P : CategoryTheory.Functor Cᵒᵖ (Type w)} (x : P.obj c.pt),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.Presheaf.coconePtToShrinkYoneda c hc')
      (CategoryTheory.shrinkYonedaEquiv.symm x) =
    (CategoryTheory.Presheaf.coconeCompShrinkYonedaHomEquiv hc').symm
      (CategoryTheory.Limits.Types.sectionOfCone (P.mapCone c) x)
-- Mathlib.CategoryTheory.Limits.Shapes.Multiequalizer
/-- For `I : MulticospanIndex J C`, we say that it has a multiequalizer if the associated
multicospan has a limit.  -/
CategoryTheory.Limits.HasMultiequalizer : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    {J : CategoryTheory.Limits.MulticospanShape} → CategoryTheory.Limits.MulticospanIndex J C → Prop
-- Mathlib.Control.Basic
guard_true : ∀ {F : Type → Type v} [inst : Alternative F] {h : Decidable True}, guard True = pure ()
-- Mathlib.FieldTheory.Finite.Basic
FiniteField.sum_subgroup_pow_eq_zero : ∀ {K : Type u_1} [inst : CommRing K] [NoZeroDivisors K] {G : Subgroup Kˣ} [inst_2 : Fintype ↥G] {k : ℕ},
  k ≠ 0 → k < Fintype.card ↥G → ∑ x, ↑↑x ^ k = 0
-- Mathlib.AlgebraicGeometry.EllipticCurve.Projective.Basic
WeierstrassCurve.Projective.X_eq_iff : ∀ {F : Type u} [inst : Field F] {P Q : Fin 3 → F}, P 2 ≠ 0 → Q 2 ≠ 0 → (P 0 * Q 2 = Q 0 * P 2 ↔ P 0 / P 2 = Q 0 / Q 2)
-- Mathlib.Probability.Process.Filtration
MeasureTheory.measurableSet_filtrationOfSet' : ∀ {Ω : Type u_1} {ι : Type u_2} {m : MeasurableSpace Ω} [inst : Preorder ι] {s : ι → Set Ω}
  (hsm : ∀ (n : ι), MeasurableSet (s n)) (i : ι), MeasurableSet (s i)
-- Mathlib.RingTheory.DividedPowers.SubDPIdeal
DividedPowers.SubDPIdeal.sSup_carrier_def : ∀ {A : Type u_1} [inst : CommSemiring A] {I : Ideal A} {hI : DividedPowers I} (S : Set hI.SubDPIdeal),
  (sSup S).carrier = sSup (DividedPowers.SubDPIdeal.toIdeal '' S)
-- Mathlib.Topology.Algebra.Category.ProfiniteGrp.Basic
/-- A closed additive subgroup of a profinite additive group is profinite.  -/
ProfiniteAddGrp.ofClosedAddSubgroup : {G : ProfiniteAddGrp.{u_1}} → ClosedAddSubgroup ↑G.toProfinite.toTop → ProfiniteAddGrp.{u_1}
-- Std.Data.Internal.List.Associative
Std.Internal.List.foldlM_eq_foldlM_keys : ∀ {α : Type u} {β : α → Type v} {δ : Type w} {m' : Type w → Type w'} [inst : Monad m'] [LawfulMonad m']
  {l : List ((a : α) × β a)} {f : δ → α → m' δ} {init : δ},
  List.foldlM (fun a b => f a b.fst) init l = List.foldlM f init (Std.Internal.List.keys l)
-- Mathlib.AlgebraicTopology.SimplicialSet.Dimension
SSet.instHasDimensionLTToSSetBotSubcomplex : ∀ {X : SSet} (n : ℕ), ⊥.toSSet.HasDimensionLT n
-- Mathlib.Algebra.Order.Floor.Ring
Int.self_sub_floor : ∀ {R : Type u_2} [inst : Ring R] [inst_1 : LinearOrder R] [inst_2 : FloorRing R] (a : R), a - ↑⌊a⌋ = Int.fract a
-- Lean.Meta.Tactic.Grind.AC.Seq
Lean.Grind.AC.Seq.isSorted : Lean.Grind.AC.Seq → Bool
-- Mathlib.CategoryTheory.Bicategory.Modification.Pseudo
CategoryTheory.Pseudofunctor.StrongTrans.Modification.mk : {B : Type u₁} →
  [inst : CategoryTheory.Bicategory B] →
    {C : Type u₂} →
      [inst_1 : CategoryTheory.Bicategory C] →
        {F G : CategoryTheory.Pseudofunctor B C} →
          {η θ : F ⟶ G} →
            (app : (a : B) → η.app a ⟶ θ.app a) →
              autoParam
                  (∀ {a b : B} (f : a ⟶ b),
                    CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.whiskerLeft (F.map f) (app b))
                        (θ.naturality f).hom =
                      CategoryTheory.CategoryStruct.comp (η.naturality f).hom
                        (CategoryTheory.Bicategory.whiskerRight (app a) (G.map f)))
                  CategoryTheory.Pseudofunctor.StrongTrans.Modification.naturality._autoParam →
                CategoryTheory.Pseudofunctor.StrongTrans.Modification η θ
-- Mathlib.Algebra.Order.Field.Basic
le_one_div : ∀ {α : Type u_2} [inst : Semifield α] [inst_1 : PartialOrder α] [PosMulReflectLT α] {a b : α},
  0 < a → 0 < b → (a ≤ 1 / b ↔ b ≤ 1 / a)
-- Std.Tactic.BVDecide.LRAT.Internal.Assignment
/-- Updates the old assignment of `l` to reflect the fact that `(l, true)` is now part of the formula.
 -/
Std.Tactic.BVDecide.LRAT.Internal.Assignment.addPosAssignment : Std.Tactic.BVDecide.LRAT.Internal.Assignment → Std.Tactic.BVDecide.LRAT.Internal.Assignment
-- Init.Data.Int.DivMod.Lemmas
Int.bmod_natAbs_add_one : ∀ (x : ℤ), x ≠ -1 → x.bmod (x.natAbs + 1) = -x.sign
-- Mathlib.NumberTheory.MulChar.Basic
/-- The sum over all values of a nontrivial multiplicative character on a finite ring is zero
(when the target is a domain).  -/
MulChar.sum_eq_zero_of_ne_one : ∀ {R : Type u_1} [inst : CommMonoid R] [inst_1 : Fintype R] {R' : Type u_2} [inst_2 : CommRing R'] [IsDomain R']
  {χ : MulChar R R'}, χ ≠ 1 → ∑ a, χ a = 0
-- Mathlib.Algebra.Homology.SpectralObject.Page
CategoryTheory.Abelian.SpectralObject.homologyDataIdId_iso_inv : ∀ {C : Type u_1} {ι : Type u_2} [inst : CategoryTheory.Category.{v_1, u_1} C]
  [inst_1 : CategoryTheory.Category.{v_2, u_2} ι] [inst_2 : CategoryTheory.Abelian C]
  (X : CategoryTheory.Abelian.SpectralObject C ι) {i j : ι} (f : i ⟶ j) (n₀ n₁ n₂ : ℤ)
  (hn₁ : autoParam (n₀ + 1 = n₁) CategoryTheory.Abelian.SpectralObject.homologyDataIdId._auto_1)
  (hn₂ : autoParam (n₁ + 1 = n₂) CategoryTheory.Abelian.SpectralObject.homologyDataIdId._auto_3),
  (X.homologyDataIdId f n₀ n₁ n₂ hn₁ hn₂).iso.inv =
    CategoryTheory.CategoryStruct.id ((X.H n₁).obj (CategoryTheory.ComposableArrows.mk₁ f))
-- Mathlib.Algebra.Homology.Additive
CategoryTheory.instFaithfulHomologicalComplexMapHomologicalComplex : ∀ {ι : Type u_1} {V : Type u} [inst : CategoryTheory.Category.{v, u} V] [inst_1 : CategoryTheory.Preadditive V]
  {W : Type u_2} [inst_2 : CategoryTheory.Category.{v_1, u_2} W] [inst_3 : CategoryTheory.Preadditive W]
  (F : CategoryTheory.Functor V W) [inst_4 : F.Additive] (c : ComplexShape ι) [F.Faithful],
  (F.mapHomologicalComplex c).Faithful
-- Init.Data.Fin.Basic
Fin.val_lt_of_le : ∀ {n b : ℕ} (i : Fin b), b ≤ n → ↑i < n
-- Mathlib.Order.RelClasses
instIrreflLt : ∀ {α : Type u} [inst : Preorder α], Std.Irrefl fun x1 x2 => x1 < x2
-- Mathlib.CategoryTheory.Adjunction.Basic
CategoryTheory.Adjunction.equivHomsetRightOfNatIso_apply : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  {F F' : CategoryTheory.Functor C D} (iso : F ≅ F') {X : C} {Y : D} (f : Y ⟶ F.obj X),
  (CategoryTheory.Adjunction.equivHomsetRightOfNatIso iso) f = CategoryTheory.CategoryStruct.comp f (iso.hom.app X)
-- Mathlib.Topology.DiscreteQuotient
/-- The map induced by a refinement of a discrete quotient.  -/
DiscreteQuotient.ofLE : {X : Type u_2} →
  [inst : TopologicalSpace X] → {A B : DiscreteQuotient X} → A ≤ B → Quotient A.toSetoid → Quotient B.toSetoid
-- Std.Sync.Channel
_private.Std.Sync.Channel.0.Std.CloseableChannel.Bounded.Consumer.mk.sizeOf_spec : ∀ {α : Type} [inst : SizeOf α] (promise : IO.Promise Bool) (waiter : Option (Std.Async.Waiter (Option α))),
  sizeOf { promise := promise, waiter := waiter } = 1 + sizeOf promise + sizeOf waiter
-- Mathlib.GroupTheory.MonoidLocalization.Order
AddLocalization.lt.eq_1 : ∀ {α : Type u_1} [inst : AddCommMonoid α] [inst_1 : PartialOrder α] [inst_2 : IsOrderedCancelAddMonoid α]
  {s : AddSubmonoid α}, AddLocalization.lt = { lt := fun a b => a.liftOn₂ b (fun a₁ a₂ b₁ b₂ => ↑b₂ + a₁ < ↑a₂ + b₁) ⋯ }
-- Lean.Meta.Tactic.Simp.Rewrite
/-- Wrapper for invoking `discharge?` method. It checks for maximum discharge depth, create trace nodes, and ensure
the generated proof was successfully assigned to `x`.
 -/
Lean.Meta.Simp.discharge?' : Lean.Meta.Origin → Lean.Expr → Lean.Expr → Lean.Meta.SimpM Bool
-- Mathlib.Algebra.Module.LinearMap.Defs
DistribMulActionHom.toLinearMap_injective : ∀ {R : Type u_1} {S : Type u_5} {M : Type u_8} {M₂ : Type u_10} [inst : AddCommMonoid M] [inst_1 : AddCommMonoid M₂]
  [inst_2 : Semiring R] [inst_3 : Module R M] [inst_4 : Semiring S] [inst_5 : Module S M₂] {σ : R →+* S}
  {f g : M →ₑ+[↑σ] M₂}, ↑f = ↑g → f = g
-- Init.Data.Stream
Std.instForInOfMonadOfStream : {m : Type u_1 → Type u_2} → {ρ : Type u_3} → {α : Type u_4} → [Monad m] → [Std.Stream ρ α] → ForIn m ρ α
-- Init.Prelude
instHSub : {α : Type u_1} → [Sub α] → HSub α α α
-- Mathlib.CategoryTheory.Equivalence.Symmetry
/-- Taking the symmetric of an equivalence induces an equivalence of categories
`(C ≌ D) ≌ (D ≌ C)ᵒᵖ`.  -/
CategoryTheory.Equivalence.symmEquiv : (C : Type u_1) →
  [inst : CategoryTheory.Category.{v_1, u_1} C] →
    (D : Type u_2) → [inst_1 : CategoryTheory.Category.{v_2, u_2} D] → (C ≌ D) ≌ (D ≌ C)ᵒᵖ
-- Std.Sync.CancellationToken
Std.instReprCancellationReason : Repr Std.CancellationReason
-- Mathlib.LinearAlgebra.AffineSpace.Basis
/-- TODO: generalize to include `SMul (P ≃ᵃ[k] P) (AffineBasis ι k P)`, which acts on `P` with a
`VAdd` version of a `DistribMulAction`.  -/
AffineBasis.instIsScalarTower : ∀ {ι : Type u_1} {G : Type u_3} {G' : Type u_4} {k : Type u_5} {V : Type u_6} [inst : AddCommGroup V] [inst_1 : Ring k]
  [inst_2 : Module k V] [inst_3 : Group G] [inst_4 : Group G'] [inst_5 : DistribMulAction G V]
  [inst_6 : DistribMulAction G' V] [inst_7 : SMulCommClass G k V] [inst_8 : SMulCommClass G' k V] [inst_9 : SMul G G']
  [IsScalarTower G G' V], IsScalarTower G G' (AffineBasis ι k V)
-- Mathlib.Geometry.Manifold.VectorBundle.Riemannian
Bundle.ContMDiffRiemannianMetric.mk.inj : ∀ {EB : Type u_1} {inst : NormedAddCommGroup EB} {inst_1 : NormedSpace ℝ EB} {HB : Type u_2}
  {inst_2 : TopologicalSpace HB} {IB : ModelWithCorners ℝ EB HB} {n : WithTop ℕ∞} {B : Type u_3}
  {inst_3 : TopologicalSpace B} {inst_4 : ChartedSpace HB B} {F : Type u_4} {inst_5 : NormedAddCommGroup F}
  {inst_6 : NormedSpace ℝ F} {E : B → Type u_5} {inst_7 : TopologicalSpace (Bundle.TotalSpace F E)}
  {inst_8 : (b : B) → TopologicalSpace (E b)} {inst_9 : (b : B) → AddCommGroup (E b)}
  {inst_10 : (b : B) → Module ℝ (E b)} {inst_11 : FiberBundle F E} {inst_12 : VectorBundle ℝ F E}
  {inner : (b : B) → E b →L[ℝ] E b →L[ℝ] ℝ} {symm : ∀ (b : B) (v w : E b), ((inner b) v) w = ((inner b) w) v}
  {pos : ∀ (b : B) (v : E b), v ≠ 0 → 0 < ((inner b) v) v}
  {isVonNBounded : ∀ (b : B), Bornology.IsVonNBounded ℝ {v | ((inner b) v) v < 1}}
  {contMDiff : ContMDiff IB (IB.prod (modelWithCornersSelf ℝ (F →L[ℝ] F →L[ℝ] ℝ))) n fun b => ⟨b, inner b⟩}
  {inner_1 : (b : B) → E b →L[ℝ] E b →L[ℝ] ℝ} {symm_1 : ∀ (b : B) (v w : E b), ((inner_1 b) v) w = ((inner_1 b) w) v}
  {pos_1 : ∀ (b : B) (v : E b), v ≠ 0 → 0 < ((inner_1 b) v) v}
  {isVonNBounded_1 : ∀ (b : B), Bornology.IsVonNBounded ℝ {v | ((inner_1 b) v) v < 1}}
  {contMDiff_1 : ContMDiff IB (IB.prod (modelWithCornersSelf ℝ (F →L[ℝ] F →L[ℝ] ℝ))) n fun b => ⟨b, inner_1 b⟩},
  { inner := inner, symm := symm, pos := pos, isVonNBounded := isVonNBounded, contMDiff := contMDiff } =
      { inner := inner_1, symm := symm_1, pos := pos_1, isVonNBounded := isVonNBounded_1, contMDiff := contMDiff_1 } →
    inner = inner_1
-- Mathlib.Algebra.Category.MonCat.Basic
MonCat.id_apply : ∀ (M : MonCat) (x : ↑M), (CategoryTheory.ConcreteCategory.hom (CategoryTheory.CategoryStruct.id M)) x = x
-- Mathlib.Analysis.Meromorphic.TrailingCoefficient
/-- The trailing coefficient of `fun z ↦ z - constant` at `z₀` equals one if `z₀ = constant`, or else
`z₀ - constant`.
 -/
meromorphicTrailingCoeffAt_id_sub_const : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] [inst_1 : DecidableEq 𝕜] {x y : 𝕜},
  meromorphicTrailingCoeffAt (fun x => x - y) x = if x = y then 1 else x - y
-- Lean.Meta.Tactic.Intro
Lean.Meta.tactic.hygienic : Lean.Option Bool
-- Mathlib.RingTheory.Jacobson.Radical
Module.map_jacobson_of_ker_le : ∀ {R : Type u_1} {R₂ : Type u_2} {M : Type u_3} {M₂ : Type u_4} [inst : Ring R] [inst_1 : Ring R₂]
  [inst_2 : AddCommGroup M] [inst_3 : Module R M] [inst_4 : AddCommGroup M₂] [inst_5 : Module R₂ M₂] {τ₁₂ : R →+* R₂}
  [inst_6 : RingHomSurjective τ₁₂] {f : M →ₛₗ[τ₁₂] M₂},
  Function.Surjective ⇑f → f.ker ≤ Module.jacobson R M → Submodule.map f (Module.jacobson R M) = Module.jacobson R₂ M₂
-- Mathlib.Analysis.Convex.GaugeRescale
gauge_gaugeRescale' : ∀ {E : Type u_1} [inst : AddCommGroup E] [inst_1 : Module ℝ E] (s : Set E) {t : Set E} {x : E},
  gauge t x ≠ 0 → gauge t (gaugeRescale s t x) = gauge s x
-- Mathlib.Data.Nat.Pairing
Nat.pair_eq_pair : ∀ {a b c d : ℕ}, Nat.pair a b = Nat.pair c d ↔ a = c ∧ b = d
-- Mathlib.Analysis.Calculus.Rademacher
/-- Integration by parts formula for the line derivative of Lipschitz functions, assuming one of
them is compactly supported.  -/
LipschitzWith.integral_lineDeriv_mul_eq : ∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] [inst_2 : MeasurableSpace E] [BorelSpace E]
  {C D : NNReal} {f g : E → ℝ} {μ : MeasureTheory.Measure E} [FiniteDimensional ℝ E] [μ.IsAddHaarMeasure],
  LipschitzWith C f →
    LipschitzWith D g →
      HasCompactSupport g → ∀ (v : E), ∫ (x : E), lineDeriv ℝ f x v * g x ∂μ = ∫ (x : E), lineDeriv ℝ g x (-v) * f x ∂μ
-- Mathlib.Order.Hom.Basic
/-- The order isomorphism `α ≃o β` when `α` and `β` are preordered types
containing unique elements.  -/
OrderIso.ofUnique : (α : Type u_6) → (β : Type u_7) → [Unique α] → [Unique β] → [inst : Preorder α] → [inst_1 : Preorder β] → α ≃o β