mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Algebra.Order.Ring.Unbundled.Basic
/-- Variant of `lt_mul_of_one_lt_left` for `b` negative instead of positive.  -/
mul_lt_of_one_lt_left : ∀ {R : Type u} [inst : Semiring R] [inst_1 : PartialOrder R] {a b : R} [ExistsAddOfLE R] [MulPosStrictMono R]
  [AddRightStrictMono R] [AddRightReflectLT R], b < 0 → 1 < a → a * b < b
-- Mathlib.Data.ENNReal.Inv
/-- See `ENNReal.inv_mul_cancel_right'` for a stronger version.  -/
ENNReal.inv_mul_cancel_right : ∀ {a b : ENNReal}, b ≠ 0 → b ≠ ⊤ → a * b⁻¹ * b = a
-- Mathlib.Algebra.Group.Hom.Defs
map_comp_div : ∀ {ι : Type u_1} {G : Type u_7} {H : Type u_8} {F : Type u_9} [inst : FunLike F G H] [inst_1 : Group G]
  [inst_2 : DivisionMonoid H] [MonoidHomClass F G H] (f : F) (g h : ι → G), ⇑f ∘ (g / h) = ⇑f ∘ g / ⇑f ∘ h
-- Mathlib.Analysis.SpecialFunctions.Complex.Log
Complex.log_mul_eq_add_log_iff : ∀ {x y : ℂ},
  x ≠ 0 → y ≠ 0 → (Complex.log (x * y) = Complex.log x + Complex.log y ↔ x.arg + y.arg ∈ Set.Ioc (-Real.pi) Real.pi)
-- Mathlib.Algebra.Homology.HomotopyCategory.HomComplex
CochainComplex.HomComplex.Cochain.ofHoms_zero : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Preadditive C]
  {F G : CochainComplex C ℤ}, (CochainComplex.HomComplex.Cochain.ofHoms fun p => 0) = 0
-- Mathlib.Data.Nat.Nth
Nat.exists_lt_card_finite_nth_eq : ∀ {p : ℕ → Prop} (hf : (Set.ofPred p).Finite) {x : ℕ}, p x → ∃ n < hf.toFinset.card, Nat.nth p n = x
-- Mathlib.Topology.Algebra.OpenSubgroup
OpenAddSubgroup.hasCoeAddSubgroup.eq_1 : ∀ {G : Type u_1} [inst : AddGroup G] [inst_1 : TopologicalSpace G],
  OpenAddSubgroup.hasCoeAddSubgroup = { coe := OpenAddSubgroup.toAddSubgroup }
-- Mathlib.FieldTheory.IsAlgClosed.Basic
IsAlgClosed.instIsAlgClosure : ∀ (F : Type u_1) [inst : Field F] [IsAlgClosed F], IsAlgClosure F F
-- Lean.Server.Requests
Lean.Server.RequestError.invalidParams : String → Lean.Server.RequestError
-- Mathlib.Tactic.Ring.Compare
/-- `PartialOrder` implies `LT`.  -/
Mathlib.Tactic.Ring.ltOfPartialOrder : (α : Type u_1) → [PartialOrder α] → LT α
-- Std.Data.DTreeMap.Internal.Balancing
_private.Std.Data.DTreeMap.Internal.Balancing.0.Std.DTreeMap.Internal.Impl.balanceLErase.match_5.eq_1 : ∀ {α : Type u_1} {β : α → Type u_2} (rs : ℕ) (k : α) (v : β k) (l r : Std.DTreeMap.Internal.Impl α β)
  (motive :
    (l_1 : Std.DTreeMap.Internal.Impl α β) →
      l_1.Balanced →
        Std.DTreeMap.Internal.Impl.BalanceLErasePrecond l_1.size (Std.DTreeMap.Internal.Impl.inner rs k v l r).size →
          Sort u_3)
  (hlb : Std.DTreeMap.Internal.Impl.leaf.Balanced)
  (hlr :
    Std.DTreeMap.Internal.Impl.BalanceLErasePrecond Std.DTreeMap.Internal.Impl.leaf.size
      (Std.DTreeMap.Internal.Impl.inner rs k v l r).size)
  (h_1 :
    (hlb : Std.DTreeMap.Internal.Impl.leaf.Balanced) →
      (hlr :
          Std.DTreeMap.Internal.Impl.BalanceLErasePrecond Std.DTreeMap.Internal.Impl.leaf.size
            (Std.DTreeMap.Internal.Impl.inner rs k v l r).size) →
        motive Std.DTreeMap.Internal.Impl.leaf hlb hlr)
  (h_2 :
    (ls : ℕ) →
      (lk : α) →
        (lv : β lk) →
          (ll lr : Std.DTreeMap.Internal.Impl α β) →
            (hlb : (Std.DTreeMap.Internal.Impl.inner ls lk lv ll lr).Balanced) →
              (hlr :
                  Std.DTreeMap.Internal.Impl.BalanceLErasePrecond (Std.DTreeMap.Internal.Impl.inner ls lk lv ll lr).size
                    (Std.DTreeMap.Internal.Impl.inner rs k v l r).size) →
                motive (Std.DTreeMap.Internal.Impl.inner ls lk lv ll lr) hlb hlr),
  (match Std.DTreeMap.Internal.Impl.leaf, hlb, hlr with
    | Std.DTreeMap.Internal.Impl.leaf, hlb, hlr => h_1 hlb hlr
    | Std.DTreeMap.Internal.Impl.inner ls lk lv ll lr, hlb, hlr => h_2 ls lk lv ll lr hlb hlr) =
    h_1 hlb hlr
-- Mathlib.Data.Finset.Card
Finset.map_eq_of_subset : ∀ {α : Type u_1} {s : Finset α} {f : α ↪ α}, Finset.map f s ⊆ s → Finset.map f s = s
-- Mathlib.Analysis.Calculus.Deriv.Add
deriv.neg : ∀ {𝕜 : Type u} [inst : NontriviallyNormedField 𝕜] {F : Type v} [inst_1 : NormedAddCommGroup F]
  [inst_2 : NormedSpace 𝕜 F] {f : 𝕜 → F} {x : 𝕜}, deriv (-f) x = -deriv f x
-- Mathlib.Tactic.Widget.LibraryRewrite
/-- Render the matching side of the rewrite lemma.
This is shown at the header of each section of rewrite results.  -/
Mathlib.Tactic.LibraryRewrite.pattern : {α : Type} → Lean.Expr → Bool → (Lean.Expr → Lean.MetaM α) → Lean.MetaM α
-- Mathlib.Data.Matrix.Mul
Matrix.mul_eq_one_comm_of_card_eq : ∀ (m : Type u_10) (n : Type u_11) (R : Type u_12) [inst : Fintype m] [inst_1 : DecidableEq m] [inst_2 : Fintype n]
  [inst_3 : DecidableEq n] [inst_4 : MulOne R] [inst_5 : AddCommMonoid R] [IsStablyFiniteRing R] {A : Matrix m n R}
  {B : Matrix n m R}, Fintype.card m = Fintype.card n → (A * B = 1 ↔ B * A = 1)
-- Mathlib.Tactic.Linarith.Oracle.FourierMotzkin
/-- Returns the current max variable.  -/
Mathlib.Tactic.Linarith.getMaxVar : Mathlib.Tactic.Linarith.LinarithM ℕ
-- Batteries.Data.UnionFind.Lemmas
Batteries.UnionFind.equiv_union : ∀ {a b : ℕ} {self : Batteries.UnionFind} {x y : Fin self.size},
  (self.union x y).Equiv a b ↔
    self.Equiv a b ∨ self.Equiv a ↑x ∧ self.Equiv (↑y) b ∨ self.Equiv a ↑y ∧ self.Equiv (↑x) b
-- Std.Data.HashSet.Lemmas
Std.HashSet.isSome_get?_eq_contains : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} {m : Std.HashSet α} [EquivBEq α] [LawfulHashable α] {a : α},
  (m.get? a).isSome = m.contains a
-- Mathlib.Algebra.Module.Submodule.Defs
Submodule.copy_eq : ∀ {R : Type u} {M : Type v} [inst : Semiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M] (S : Submodule R M)
  (s : Set M) (hs : s = ↑S), S.copy s hs = S
-- Mathlib.Data.Stream.Defs
/-- Given a function `f : α → β × α`, `corec' f` creates a stream by repeatedly:
1. Starting with an initial value `a : α`
2. Applying `f` to get both the next stream element (β) and next state value (α)

This is a more convenient form when the next element and state are computed together.  -/
Stream'.corec' : {α : Type u} → {β : Type v} → (α → β × α) → α → Stream' β
-- Mathlib.Topology.Category.CompHausLike.Basic
CompHausLike.isoOfHomeo_inv_hom_hom_apply : ∀ {P : TopCat → Prop} {X Y : CompHausLike P} (f : ↑X.toTop ≃ₜ ↑Y.toTop)
  (a : ↑((CompHausLike.compHausLikeToTop P).obj Y)), (TopCat.Hom.hom (CompHausLike.isoOfHomeo f).inv.hom) a = f.symm a
-- Mathlib.Data.Finsupp.SMul
Finsupp.comapSMul_single : ∀ {α : Type u_1} {M : Type u_3} {G : Type u_5} [inst : Monoid G] [inst_1 : MulAction G α] [inst_2 : AddCommMonoid M]
  (g : G) (a : α) (b : M), (g • fun₀ | a => b) = fun₀ | g • a => b
-- Init.Data.UInt.IntToBitVec
USize.toBitVec32_xor : ∀ (a b : USize) (h : System.Platform.numBits = 32), (a ^^^ b).toBitVec32 h = a.toBitVec32 h ^^^ b.toBitVec32 h
-- Mathlib.Algebra.Group.Submonoid.Basic
AddSubmonoid.coe_iInf : ∀ {M : Type u_1} [inst : AddZeroClass M] {ι : Sort u_4} {S : ι → AddSubmonoid M}, ↑(⨅ i, S i) = ⋂ i, ↑(S i)
-- Mathlib.Logic.Embedding.Basic
Function.exists_surjective_iff : ∀ {α : Sort u_1} {β : Sort u_2}, (∃ f, Function.Surjective f) ↔ Nonempty (α → β) ∧ Nonempty (β ↪ α)
-- Std.Data.HashMap.Lemmas
Std.HashMap.Equiv.of_forall_contains_unit_eq : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} [LawfulBEq α] {m₁ m₂ : Std.HashMap α Unit},
  (∀ (k : α), m₁.contains k = m₂.contains k) → m₁.Equiv m₂
-- Mathlib.Algebra.Homology.Bifunctor
HomologicalComplex.mapBifunctor.d₂_eq' : ∀ {C₁ : Type u_1} {C₂ : Type u_2} {D : Type u_3} [inst : CategoryTheory.Category.{v_1, u_1} C₁]
  [inst_1 : CategoryTheory.Category.{v_2, u_2} C₂] [inst_2 : CategoryTheory.Category.{v_3, u_3} D] {I₁ : Type u_4}
  {I₂ : Type u_5} {J : Type u_6} {c₁ : ComplexShape I₁} {c₂ : ComplexShape I₂}
  [inst_3 : CategoryTheory.Limits.HasZeroMorphisms C₁] [inst_4 : CategoryTheory.Limits.HasZeroMorphisms C₂]
  [inst_5 : CategoryTheory.Preadditive D] (K₁ : HomologicalComplex C₁ c₁) (K₂ : HomologicalComplex C₂ c₂)
  (F : CategoryTheory.Functor C₁ (CategoryTheory.Functor C₂ D)) [inst_6 : F.PreservesZeroMorphisms]
  [inst_7 : ∀ (X₁ : C₁), (F.obj X₁).PreservesZeroMorphisms] (c : ComplexShape J) [inst_8 : TotalComplexShape c₁ c₂ c]
  [inst_9 : K₁.HasMapBifunctor K₂ F c] [inst_10 : DecidableEq J] (i₁ : I₁) {i₂ i₂' : I₂},
  c₂.Rel i₂ i₂' →
    ∀ (j : J),
      HomologicalComplex.mapBifunctor.d₂ K₁ K₂ F c i₁ i₂ j =
        c₁.ε₂ c₂ c (i₁, i₂) •
          CategoryTheory.CategoryStruct.comp ((F.obj (K₁.X i₁)).map (K₂.d i₂ i₂'))
            (K₁.ιMapBifunctorOrZero K₂ F c i₁ i₂' j)
-- Mathlib.Algebra.Module.Submodule.Map
Submodule.map_inf : ∀ {R : Type u_1} {R₂ : Type u_3} {M : Type u_5} {M₂ : Type u_7} [inst : Semiring R] [inst_1 : Semiring R₂]
  [inst_2 : AddCommMonoid M] [inst_3 : AddCommMonoid M₂] [inst_4 : Module R M] [inst_5 : Module R₂ M₂] {σ₁₂ : R →+* R₂}
  [inst_6 : RingHomSurjective σ₁₂] (f : M →ₛₗ[σ₁₂] M₂) {p q : Submodule R M},
  Function.Injective ⇑f → Submodule.map f (p ⊓ q) = Submodule.map f p ⊓ Submodule.map f q
-- Mathlib.AlgebraicGeometry.Group.Affine
AlgebraicGeometry.instIsOverMapOfHomSpecOf : ∀ {R S T : Type u} [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : CommRing T] [inst_3 : Algebra R S]
  [inst_4 : Algebra R T] (f : S →ₐ[R] T),
  AlgebraicGeometry.Scheme.Hom.IsOver (AlgebraicGeometry.Spec.map (CommRingCat.ofHom f.toRingHom))
    (AlgebraicGeometry.Spec (CommRingCat.of R))
-- Mathlib.CategoryTheory.Subobject.NoetherianObject
/-- An object `X` in a category `C` is Noetherian if `Subobject X`
satisfies the ascending chain condition. This definition is a
term in `ObjectProperty C` which allows to study the stability
properties of Noetherian objects. For statements regarding
specific objects, it is advisable to use the type class
`IsNoetherianObject` instead.  -/
CategoryTheory.isNoetherianObject : {C : Type u} → [inst : CategoryTheory.Category.{v, u} C] → CategoryTheory.ObjectProperty C
-- Mathlib.CategoryTheory.Monoidal.Rigid.Basic
CategoryTheory.rightAdjointMate.eq_1 : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.MonoidalCategory C] {X Y : C}
  [inst_2 : CategoryTheory.HasRightDual X] [inst_3 : CategoryTheory.HasRightDual Y] (f : X ⟶ Y),
  fᘁ =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.rightUnitor Yᘁ).inv
      (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerLeft Yᘁ (η_ X Xᘁ))
        (CategoryTheory.CategoryStruct.comp
          (CategoryTheory.MonoidalCategoryStruct.whiskerLeft Yᘁ
            (CategoryTheory.MonoidalCategoryStruct.whiskerRight f Xᘁ))
          (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.associator Yᘁ Y Xᘁ).inv
            (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerRight (ε_ Y Yᘁ) Xᘁ)
              (CategoryTheory.MonoidalCategoryStruct.leftUnitor Xᘁ).hom))))
-- Mathlib.Analysis.Convex.Side
Wbtw.wOppSide₃₁ : ∀ {R : Type u_1} {V : Type u_2} {P : Type u_4} [inst : CommRing R] [inst_1 : PartialOrder R]
  [inst_2 : IsStrictOrderedRing R] [inst_3 : AddCommGroup V] [inst_4 : Module R V] [inst_5 : AddTorsor V P]
  {s : AffineSubspace R P} {x y z : P}, Wbtw R x y z → y ∈ s → s.WOppSide z x
-- Mathlib.CategoryTheory.MorphismProperty.TransfiniteComposition
CategoryTheory.MorphismProperty.instRespectsIsoTransfiniteCompositionsOfShape : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] (W : CategoryTheory.MorphismProperty C) (J : Type w)
  [inst_1 : LinearOrder J] [inst_2 : SuccOrder J] [inst_3 : OrderBot J] [inst_4 : WellFoundedLT J],
  (W.transfiniteCompositionsOfShape J).RespectsIso
-- Mathlib.Topology.Compactness.Lindelof
/-- The set difference of a Lindelöf set and an open set is a Lindelöf set.  -/
IsLindelof.diff : ∀ {X : Type u} [inst : TopologicalSpace X] {s t : Set X}, IsLindelof s → IsOpen t → IsLindelof (s \ t)
-- Mathlib.Probability.Kernel.Condexp
ProbabilityTheory.condExpKernel_ae_eq_condExp' : ∀ {Ω : Type u_1} {m : MeasurableSpace Ω} [mΩ : MeasurableSpace Ω] [inst : StandardBorelSpace Ω]
  {μ : MeasureTheory.Measure Ω} [inst_1 : MeasureTheory.IsFiniteMeasure μ] {s : Set Ω},
  MeasurableSet s → (fun ω => ((ProbabilityTheory.condExpKernel μ m) ω).real s) =ᵐ[μ] μ[s.indicator fun ω => 1 | m ⊓ mΩ]
-- Mathlib.RingTheory.PowerSeries.Basic
MvPolynomial.toMvPowerSeries_pUnitAlgEquiv : ∀ {R : Type u_1} [inst : CommSemiring R] {f : MvPolynomial PUnit.{1} R},
  ↑f = ↑((MvPolynomial.uniqueAlgEquiv R PUnit.{1}) f)
-- Init.Data.Int.Order
Int.lt_add_of_neg_add_lt_left : ∀ {a b c : ℤ}, -b + a < c → a < b + c
-- Mathlib.RingTheory.Algebraic.Integral
Algebra.IsIntegral.transcendental_iff : ∀ (R : Type u_1) (S : Type u_2) {A : Type u_3} [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : Ring A]
  [inst_3 : Algebra R S] [inst_4 : Algebra R A] [inst_5 : Algebra S A] [IsScalarTower R S A] [NoZeroDivisors S]
  [FaithfulSMul R S] {a : A} [Algebra.IsIntegral R S], Transcendental R a ↔ Transcendental S a
-- Mathlib.Analysis.Asymptotics.Defs
Asymptotics.IsBigO.congr' : ∀ {α : Type u_1} {E : Type u_3} {F : Type u_4} [inst : Norm E] [inst_1 : Norm F] {l : Filter α} {f₁ f₂ : α → E}
  {g₁ g₂ : α → F}, f₁ =O[l] g₁ → f₁ =ᶠ[l] f₂ → g₁ =ᶠ[l] g₂ → f₂ =O[l] g₂
-- Mathlib.CategoryTheory.Limits.Shapes.Biproducts
/-- A bicone over `F : J → C`, which is both a limit cone and a colimit cocone.  -/
CategoryTheory.Limits.LimitBicone.isBilimit : {J : Type w} →
  {C : Type uC} →
    [inst : CategoryTheory.Category.{uC', uC} C] →
      [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C] →
        {F : J → C} → (self : CategoryTheory.Limits.LimitBicone F) → self.bicone.IsBilimit
-- Mathlib.CategoryTheory.Limits.Cones
/-- Change a cocone on `F.unop : J ⥤ C` into a cone on `F : Jᵒᵖ ⥤ Cᵒᵖ`.  -/
CategoryTheory.Limits.coneOfCoconeUnop : {J : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} J] →
    {C : Type u₃} →
      [inst_1 : CategoryTheory.Category.{v₃, u₃} C] →
        {F : CategoryTheory.Functor Jᵒᵖ Cᵒᵖ} → CategoryTheory.Limits.Cocone F.unop → CategoryTheory.Limits.Cone F
-- Aesop.Frontend.Tactic
Aesop.Frontend.TacticConfig.mk.sizeOf_spec : ∀ (additionalRules erasedRules : Array Aesop.Frontend.RuleExpr) (enabledRuleSets : Std.HashSet Aesop.RuleSetName)
  (options : Aesop.Options) (simpConfig : Lean.Meta.Simp.Config) (simpConfigSyntax? : Option Lean.Term),
  sizeOf
      { additionalRules := additionalRules, erasedRules := erasedRules, enabledRuleSets := enabledRuleSets,
        options := options, simpConfig := simpConfig, simpConfigSyntax? := simpConfigSyntax? } =
    1 + sizeOf additionalRules + sizeOf erasedRules + sizeOf enabledRuleSets + sizeOf options + sizeOf simpConfig +
      sizeOf simpConfigSyntax?
-- Mathlib.Algebra.Ring.Ext
NonAssocRing.ext : ∀ {R : Type u} ⦃inst₁ inst₂ : NonAssocRing R⦄, HAdd.hAdd = HAdd.hAdd → HMul.hMul = HMul.hMul → inst₁ = inst₂
-- Mathlib.CategoryTheory.Abelian.GrothendieckCategory.ModuleEmbedding.Opposite
CategoryTheory.Abelian.IsGrothendieckAbelian.OppositeModuleEmbedding.instRingEmbeddingRing : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    {D : Type v} →
      [inst_1 : CategoryTheory.SmallCategory D] →
        (F : CategoryTheory.Functor D Cᵒᵖ) →
          [inst_2 : CategoryTheory.Abelian C] →
            [inst_3 : CategoryTheory.IsGrothendieckAbelian.{v, v, u} C] →
              Ring (CategoryTheory.Abelian.IsGrothendieckAbelian.OppositeModuleEmbedding.EmbeddingRing F)
-- Mathlib.AlgebraicTopology.ModelCategory.CategoryWithCofibrations
/-- the class of fibrations  -/
HomotopicalAlgebra.CategoryWithFibrations.fibrations : {C : Type u} →
  {inst : CategoryTheory.Category.{v, u} C} →
    [self : HomotopicalAlgebra.CategoryWithFibrations C] → CategoryTheory.MorphismProperty C
-- Mathlib.MeasureTheory.MeasurableSpace.Constructions
QuotientGroup.measurableSpace.eq_1 : ∀ {G : Type u_6} [inst : Group G] [inst_1 : MeasurableSpace G] (S : Subgroup G),
  QuotientGroup.measurableSpace S = Quotient.instMeasurableSpace
-- Mathlib.Topology.MetricSpace.Thickening
Metric.cthickening.eq_1 : ∀ {α : Type u} [inst : PseudoEMetricSpace α] (δ : ℝ) (E : Set α),
  Metric.cthickening δ E = {x | Metric.infEDist x E ≤ ENNReal.ofReal δ}
-- Mathlib.Order.Booleanisation
Booleanisation.instBooleanAlgebra : {α : Type u_1} → [GeneralizedBooleanAlgebra α] → BooleanAlgebra (Booleanisation α)
-- Mathlib.Topology.IsLocalHomeomorph
IsLocalHomeomorphOn.discreteTopology_image_iff : ∀ {X : Type u_1} {Y : Type u_2} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y] {f : X → Y} {s : Set X},
  IsLocalHomeomorphOn f s → IsOpen s → (DiscreteTopology ↑(f '' s) ↔ DiscreteTopology ↑s)
-- Mathlib.NumberTheory.Padics.RingHoms
PadicInt.lift_sub_val_mem_span : ∀ {R : Type u_1} [inst : NonAssocSemiring R] {p : ℕ} {f : (k : ℕ) → R →+* ZMod (p ^ k)} [hp_prime : Fact (Nat.Prime p)]
  (f_compat : ∀ (k1 k2 : ℕ) (hk : k1 ≤ k2), (ZMod.castHom ⋯ (ZMod (p ^ k1))).comp (f k2) = f k1) (r : R) (n : ℕ),
  (PadicInt.lift f_compat) r - ↑((f n) r).val ∈ Ideal.span {↑p ^ n}
-- Mathlib.CategoryTheory.Bicategory.Adjunction.Adj
/-- Given an isomorphism between two 1-morphisms in `Adj B`, this is the
underlying isomorphism between the right adjoints.  -/
CategoryTheory.Bicategory.Adj.rIso : {B : Type u} →
  [inst : CategoryTheory.Bicategory B] →
    {a b : CategoryTheory.Bicategory.Adj B} → {adj₁ adj₂ : a ⟶ b} → (adj₁ ≅ adj₂) → (adj₁.r ≅ adj₂.r)
-- Batteries.Recycling.RBTree.Basic
RBTree.RBNode.Path.left.sizeOf_spec : ∀ {α : Type u} [inst : SizeOf α] (c : RBTree.RBColor) (parent : RBTree.RBNode.Path α) (v : α) (r : RBTree.RBNode α),
  sizeOf (RBTree.RBNode.Path.left c parent v r) = 1 + sizeOf c + sizeOf parent + sizeOf v + sizeOf r
-- Mathlib.Algebra.Category.MonCat.Basic
MulEquiv.toMonCatIso_hom : ∀ {X Y : Type u} [inst : Monoid X] [inst_1 : Monoid Y] (e : X ≃* Y), e.toMonCatIso.hom = MonCat.ofHom e.toMonoidHom
-- Std.Data.ExtTreeMap.Basic
/-- Tries to retrieve the mapping for the given key, returning `none` if no such mapping is present.

Uses the `LawfulEqCmp` instance to cast the retrieved value to the correct type.
 -/
Std.ExtTreeMap.get? : {α : Type u} → {β : Type v} → {cmp : α → α → Ordering} → [Std.TransCmp cmp] → Std.ExtTreeMap α β cmp → α → Option β
-- Mathlib.Data.QPF.Multivariate.Constructions.Comp
MvQPF.Comp.get_mk : ∀ {n m : ℕ} {F : TypeVec.{u} n → Type u_1} {G : Fin2 n → TypeVec.{u} m → Type u} {α : TypeVec.{u} m}
  (x : F fun i => G i α), (MvQPF.Comp.mk x).get = x
-- Mathlib.LinearAlgebra.Alternating.Basic
AlternatingMap.coe_multilinearMap_injective : ∀ {R : Type u_1} [inst : Semiring R] {M : Type u_2} [inst_1 : AddCommMonoid M] [inst_2 : Module R M] {N : Type u_3}
  [inst_3 : AddCommMonoid N] [inst_4 : Module R N] {ι : Type u_7}, Function.Injective AlternatingMap.toMultilinearMap
-- Mathlib.Order.CompleteBooleanAlgebra
/-- Construct a complete distrib lattice instance using the minimal amount of work needed.

This sets `a ⇨ b := sSup {c | c ⊓ a ≤ b}`, `aᶜ := a ⇨ ⊥`, `a \ b := sInf {c | a ≤ b ⊔ c}` and
`￢a := ⊤ \ a`.  -/
CompleteDistribLattice.ofMinimalAxioms : {α : Type u} → [inst : CompleteLattice α] → CompleteDistribLattice.MinimalAxioms α → CompleteDistribLattice α
-- Mathlib.Algebra.Algebra.Spectrum.Quasispectrum
QuasispectrumRestricts.algebraMap_image : ∀ {R : Type u_3} {S : Type u_4} {A : Type u_5} [inst : Semifield R] [inst_1 : Field S] [inst_2 : NonUnitalRing A]
  [inst_3 : Module R A] [inst_4 : Module S A] [inst_5 : Algebra R S] {a : A} {f : S → R} [IsScalarTower S A A]
  [SMulCommClass S A A] [IsScalarTower R S A],
  QuasispectrumRestricts a f → ⇑(algebraMap R S) '' quasispectrum R a = quasispectrum S a
-- Lean.Meta.Tactic.Grind.Arith.Linear.LinearM
Lean.Meta.Grind.Arith.Linear.LinearM.Context : Type
-- Lean.Meta.Tactic.Grind.Arith.Linear.Types
Lean.Meta.Grind.Arith.Linear.EqCnstrProof.coeff.injEq : ∀ (k : ℕ) (c : Lean.Meta.Grind.Arith.Linear.EqCnstr) (k_1 : ℕ) (c_1 : Lean.Meta.Grind.Arith.Linear.EqCnstr),
  (Lean.Meta.Grind.Arith.Linear.EqCnstrProof.coeff k c = Lean.Meta.Grind.Arith.Linear.EqCnstrProof.coeff k_1 c_1) =
    (k = k_1 ∧ c = c_1)
-- Mathlib.Analysis.Normed.Group.Basic
indiscreteTopology_iff_forall_nnnorm_eq_zero' : ∀ {E : Type u_5} [inst : SeminormedGroup E], IndiscreteTopology E ↔ ∀ (x : E), ‖x‖₊ = 0
-- Lean.Elab.DeclModifiers
/-- Codegen-relevant modifiers.  -/
Lean.Elab.ComputeKind : Type
-- Mathlib.Data.Set.NAry
/-- Symmetric statement to `Set.image2_image_left_comm`.  -/
Set.image_image2_distrib_left : ∀ {α : Type u_1} {α' : Type u_2} {β : Type u_3} {γ : Type u_5} {δ : Type u_7} {f : α → β → γ} {s : Set α} {t : Set β}
  {g : γ → δ} {f' : α' → β → δ} {g' : α → α'},
  (∀ (a : α) (b : β), g (f a b) = f' (g' a) b) → g '' Set.image2 f s t = Set.image2 f' (g' '' s) t
-- Mathlib.Topology.NhdsWithin
nhdsWithin_pi_eq : ∀ {ι : Type u_5} {X : ι → Type u_6} [inst : (i : ι) → TopologicalSpace (X i)] {I : Set ι},
  I.Finite →
    ∀ (s : (i : ι) → Set (X i)) (x : (i : ι) → X i),
      nhdsWithin x (I.pi s) =
        (⨅ i ∈ I, Filter.comap (fun x => x i) (nhdsWithin (x i) (s i))) ⊓
          ⨅ i, ⨅ (_ : i ∉ I), Filter.comap (fun x => x i) (nhds (x i))
-- Lean.Util.ForEachExpr
Lean.Expr.forEach : {ω : Type} →
  {m : Type → Type} → [STWorld ω m] → [MonadLiftT (ST ω) m] → [Monad m] → Lean.Expr → (Lean.Expr → m Unit) → m Unit
-- Init.Grind.Ring.CommSolver
Lean.Grind.CommRing.Mon.denote_mul_nc : ∀ {α : Type u_1} [inst : Lean.Grind.Semiring α] (ctx : Lean.Grind.CommRing.Context α) (m₁ m₂ : Lean.Grind.CommRing.Mon),
  Lean.Grind.CommRing.Mon.denote ctx (m₁.mul_nc m₂) =
    Lean.Grind.CommRing.Mon.denote ctx m₁ * Lean.Grind.CommRing.Mon.denote ctx m₂
-- Mathlib.Algebra.Order.Monoid.Unbundled.WithTop
WithTop.addRightReflectLT : ∀ {α : Type u} [inst : Add α] [inst_1 : LT α] [AddRightReflectLT α], AddRightReflectLT (WithTop α)
-- Init.Data.Int.Linear
Int.Internal.Linear.Poly.isUnsatEq_k : Int.Internal.Linear.Poly → Bool
-- Mathlib.Algebra.Category.Ring.Limits
SemiRingCat.limitSemiring : {J : Type v} →
  [inst : CategoryTheory.Category.{w, v} J] →
    (F : CategoryTheory.Functor J SemiRingCat) →
      [inst_1 : Small.{u, max u v} ↑(F.comp (CategoryTheory.forget SemiRingCat)).sections] →
        Semiring (CategoryTheory.Limits.Types.Small.limitCone (F.comp (CategoryTheory.forget SemiRingCat))).pt
-- Mathlib.Algebra.Group.Subgroup.Basic
AddSubgroup.pi_empty : ∀ {η : Type u_7} {f : η → Type u_8} [inst : (i : η) → AddGroup (f i)] (H : (i : η) → AddSubgroup (f i)),
  AddSubgroup.pi ∅ H = ⊤
-- Mathlib.CategoryTheory.Limits.Elements
/-- An initial object in the category `F.Elements` of a covariant functor defines a
corepresentation for that functor.  -/
CategoryTheory.Functor.Elements.corepresentableByOfIsInitial : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    {F : CategoryTheory.Functor C (Type w)} →
      {E : F.Elements} → CategoryTheory.Limits.IsInitial E → F.CorepresentableBy E.fst
-- Std.Tactic.BVDecide.Bitblast.BVExpr.Circuit.Impl.Operations.Replicate
Std.Tactic.BVDecide.BVExpr.bitblast.ReplicateTarget.mk.injEq : ∀ {α : Type} [inst : Hashable α] [inst_1 : DecidableEq α] {aig : Std.Sat.AIG α} {combined w : ℕ} (n : ℕ)
  (inner : aig.RefVec w) (h : combined = w * n) (w_1 n_1 : ℕ) (inner_1 : aig.RefVec w_1) (h_1 : combined = w_1 * n_1),
  ({ w := w, n := n, inner := inner, h := h } = { w := w_1, n := n_1, inner := inner_1, h := h_1 }) =
    (w = w_1 ∧ n = n_1 ∧ inner ≍ inner_1)
-- Init.Data.Nat.Fold
_private.Init.Data.Nat.Fold.0.Nat.any.match_1.splitter : (motive : (x : ℕ) → ((i : ℕ) → i < x → Bool) → Sort u_1) →
  (x : ℕ) →
    (x_1 : (i : ℕ) → i < x → Bool) →
      ((f : (i : ℕ) → i < 0 → Bool) → motive 0 f) →
        ((n : ℕ) → (f : (i : ℕ) → i < n.succ → Bool) → motive n.succ f) → motive x x_1
-- Mathlib.MeasureTheory.Function.LpSpace.Indicator
/-- Constant function as an element of `MeasureTheory.Lp` for a finite measure.  -/
MeasureTheory.Lp.const : {α : Type u_1} →
  {E : Type u_2} →
    {m : MeasurableSpace α} →
      (p : ENNReal) →
        (μ : MeasureTheory.Measure α) →
          [inst : NormedAddCommGroup E] → [MeasureTheory.IsFiniteMeasure μ] → E →+ ↥(MeasureTheory.Lp E p μ)
-- Mathlib.Topology.Algebra.Module.Equiv
ContinuousLinearMap.IsInvertible.bijective : ∀ {R : Type u_1} {M : Type u_2} {M₂ : Type u_3} [inst : TopologicalSpace M] [inst_1 : TopologicalSpace M₂]
  [inst_2 : Semiring R] [inst_3 : AddCommMonoid M] [inst_4 : Module R M] [inst_5 : AddCommMonoid M₂]
  [inst_6 : Module R M₂] {f : M →L[R] M₂}, f.IsInvertible → Function.Bijective ⇑f
-- Mathlib.Analysis.Complex.UpperHalfPlane.Basic
/-- **Alias** of `UpperHalfPlane.ne_intCast`. -/
UpperHalfPlane.ne_int : ∀ (z : UpperHalfPlane) (n : ℤ), ↑z ≠ ↑n