mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Topology.Algebra.ConstMulAction
ProperlyDiscontinuousSMul.mk : ∀ {Γ : Type u_4} {T : Type u_5} [inst : TopologicalSpace T] [inst_1 : SMul Γ T],
  (∀ {K L : Set T}, IsCompact K → IsCompact L → {γ | ((fun x => γ • x) '' K ∩ L).Nonempty}.Finite) →
    ProperlyDiscontinuousSMul Γ T
-- Mathlib.Order.Monotone.Defs
Function.const_strictMono : ∀ {α : Type u} {β : Type v} [inst : Preorder α] [Nonempty β], StrictMono (Function.const β)
-- Mathlib.Algebra.Category.GrpWithZero
GrpWithZero.instLargeCategory : CategoryTheory.LargeCategory GrpWithZero
-- Mathlib.NumberTheory.ModularForms.EisensteinSeries.Defs
/-- The map from `Fin 2 → ℤ` sending `![a,b]` to `a.gcd b`.  -/
EisensteinSeries.finGcdMap : (Fin 2 → ℤ) → ℕ
-- Lean.Meta.Tactic.Grind.Proof
_private.Lean.Meta.Tactic.Grind.Proof.0.Lean.Meta.Grind.flipProof : Lean.Expr → Bool → Bool → Lean.MetaM Lean.Expr
-- Mathlib.Tactic.Linter.TextBased
_private.Mathlib.Tactic.Linter.TextBased.0.Mathlib.Linter.TextBased.StyleError.unicodeVariant.inj : ∀ {s : String} {selector : Option Char} {s_1 : String} {selector_1 : Option Char},
  Mathlib.Linter.TextBased.StyleError.unicodeVariant✝ s selector =
      Mathlib.Linter.TextBased.StyleError.unicodeVariant✝ s_1 selector_1 →
    s = s_1 ∧ selector = selector_1
-- Init.System.FilePath
/-- The character that separates file extensions from file names.
 -/
System.FilePath.extSeparator : Char
-- Mathlib.RingTheory.Extension.Presentation.Submersive
Algebra.PreSubmersivePresentation.comp.congr_simp : ∀ {R : Type u} {S : Type v} {ι : Type w} {σ : Type t} [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : Algebra R S]
  {ι' : Type u_1} {σ' : Type u_2} {T : Type u_3} [inst_3 : CommRing T] [inst_4 : Algebra R T] [inst_5 : Algebra S T]
  [inst_6 : IsScalarTower R S T] (Q Q_1 : Algebra.PreSubmersivePresentation S T ι' σ'),
  Q = Q_1 → ∀ (P P_1 : Algebra.PreSubmersivePresentation R S ι σ), P = P_1 → Q.comp P = Q_1.comp P_1
-- Mathlib.LinearAlgebra.Basis.MulOpposite
Module.Basis.mulOpposite_repr_op : ∀ {R : Type u_1} {H : Type u_2} {ι : Type u_3} [inst : Semiring R] [inst_1 : AddCommMonoid H] [inst_2 : Module R H]
  (b : Module.Basis ι R H) (x : H), b.mulOpposite.repr (MulOpposite.op x) = b.repr x
-- Mathlib.Data.Finsupp.ToDFinsupp
DFinsupp.toFinsupp_neg : ∀ {ι : Type u_1} {M : Type u_3} [inst : DecidableEq ι] [inst_1 : AddGroup M] [inst_2 : (m : M) → Decidable (m ≠ 0)]
  (f : Π₀ (x : ι), M), (-f).toFinsupp = -f.toFinsupp
-- Mathlib.MeasureTheory.Integral.Marginal
MeasureTheory.lmarginal_mono : ∀ {δ : Type u_1} {X : δ → Type u_3} [inst : (i : δ) → MeasurableSpace (X i)] {μ : (i : δ) → MeasureTheory.Measure (X i)}
  [inst_1 : DecidableEq δ] {s : Finset δ} {f g : ((i : δ) → X i) → ENNReal}, f ≤ g → ∫⋯∫⁻_s, f ∂μ ≤ ∫⋯∫⁻_s, g ∂μ
-- Mathlib.MeasureTheory.Function.LpSeminorm.Indicator
/-- A single function that is `MemLp f p μ` is tight with respect to `μ`.  -/
MeasureTheory.MemLp.exists_eLpNorm_indicator_compl_lt : ∀ {α : Type u_1} {m0 : MeasurableSpace α} {p : ENNReal} {μ : MeasureTheory.Measure α} {β : Type u_7}
  [inst : NormedAddCommGroup β],
  p ≠ ⊤ →
    ∀ {f : α → β},
      MeasureTheory.MemLp f p μ →
        ∀ {ε : ENNReal}, ε ≠ 0 → ∃ s, MeasurableSet s ∧ μ s < ⊤ ∧ MeasureTheory.eLpNorm (sᶜ.indicator f) p μ < ε
-- Init.Data.Dyadic.Basic
/-- Add two dyadic numbers.  -/
Dyadic.add : Dyadic → Dyadic → Dyadic
-- Mathlib.LinearAlgebra.Matrix.ToLin
LinearMap.toMatrixAlgEquiv'_id : ∀ {R : Type u_1} [inst : CommSemiring R] {n : Type u_5} [inst_1 : DecidableEq n] [inst_2 : Fintype n],
  LinearMap.toMatrixAlgEquiv' LinearMap.id = 1
-- Lean.Elab.App
_private.Lean.Elab.App.0.Lean.Elab.Term.elabAppFn : Lean.Syntax →
  List Lean.Elab.Term.LVal →
    Array Lean.Elab.Term.NamedArg →
      Array Lean.Elab.Term.Arg →
        Option Lean.Expr →
          Bool →
            Bool →
              Bool →
                Array (Lean.Elab.Term.TermElabResult Lean.Expr) →
                  Lean.Elab.TermElabM (Array (Lean.Elab.Term.TermElabResult Lean.Expr))
-- Mathlib.CategoryTheory.EssentiallySmall
/-- Implementation of `ShrinkHoms.equivalence`.  -/
CategoryTheory.ShrinkHoms.inverse : (C : Type u) →
  [inst : CategoryTheory.Category.{v, u} C] →
    [inst_1 : CategoryTheory.LocallySmall.{w, v, u} C] → CategoryTheory.Functor (CategoryTheory.ShrinkHoms.{u} C) C
-- Mathlib.Data.Real.ConjExponents
/-- For `r`, instead of `p`  -/
Real.HolderTriple.ne_zero' : ∀ {p q r : ℝ}, p.HolderTriple q r → r ≠ 0
-- Mathlib.Algebra.Torsor.Defs
Equiv.pointReflection_apply : ∀ {G : Type u_3} {P : Type u_4} [inst : AddGroup G] [inst_1 : AddTorsor G P] (x y : P),
  (Equiv.pointReflection x) y = (x -ᵥ y) +ᵥ x
-- Mathlib.RingTheory.HahnSeries.Summable
HahnSeries.SummableFamily.isPWO_iUnion_support' : ∀ {Γ : Type u_8} {R : Type u_9} [inst : PartialOrder Γ] [inst_1 : AddCommMonoid R] {α : Type u_7}
  (self : HahnSeries.SummableFamily Γ R α), (⋃ a, (self.toFun a).support).IsPWO
-- Mathlib.RingTheory.Spectrum.Prime.FreeLocus
Module.rankAtStalk_self : ∀ {R : Type uR} [inst : CommRing R] [Nontrivial R], Module.rankAtStalk R = 1
-- Mathlib.Order.Category.LinOrd
LinOrd.ext_iff : ∀ {X Y : LinOrd} {f g : X ⟶ Y},
  f = g ↔ ∀ (x : ↑X), (CategoryTheory.ConcreteCategory.hom f) x = (CategoryTheory.ConcreteCategory.hom g) x
-- Mathlib.CategoryTheory.Monoidal.Preadditive
CategoryTheory.instPreservesFiniteBiproductsTensorLeft : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Preadditive C]
  [inst_2 : CategoryTheory.MonoidalCategory C] [inst_3 : CategoryTheory.MonoidalPreadditive C] (X : C),
  CategoryTheory.Limits.PreservesFiniteBiproducts (CategoryTheory.MonoidalCategory.tensorLeft X)
-- Mathlib.Algebra.MonoidAlgebra.Defs
AddMonoidAlgebra.of'_eq_of : ∀ {R : Type u_1} {M : Type u_4} [inst : Semiring R] [inst_1 : AddZeroClass M] (a : M),
  AddMonoidAlgebra.of' R M a = (AddMonoidAlgebra.of R M) (Multiplicative.ofAdd a)
-- Mathlib.CategoryTheory.Functor.KanExtension.Pointwise
/-- A left extension `E : LeftExtension L F` is a pointwise left Kan extension when
it is a pointwise left Kan extension at any object.  -/
CategoryTheory.Functor.LeftExtension.IsPointwiseLeftKanExtension : {C : Type u_1} →
  {D : Type u_2} →
    {H : Type u_4} →
      [inst : CategoryTheory.Category.{v_1, u_1} C] →
        [inst_1 : CategoryTheory.Category.{v_2, u_2} D] →
          [inst_2 : CategoryTheory.Category.{v_4, u_4} H] →
            {L : CategoryTheory.Functor C D} →
              {F : CategoryTheory.Functor C H} → L.LeftExtension F → Type (max (max (max (max u_2 u_4) v_4) v_2) u_1)
-- Init.Data.Int.Linear
Int.Internal.Linear.eq_eq_subst' : ∀ (ctx : Int.Internal.Linear.Context) (a b : ℤ) (p₁ p₂ p₃ : Int.Internal.Linear.Poly),
  Int.Internal.Linear.eq_eq_subst'_cert a b p₁ p₂ p₃ = true →
    Int.Internal.Linear.Poly.denote' ctx p₁ = 0 →
      Int.Internal.Linear.Poly.denote' ctx p₂ = 0 → Int.Internal.Linear.Poly.denote' ctx p₃ = 0
-- Mathlib.Analysis.InnerProductSpace.Reproducing
RKHS.norm_kernel_eq_norm_kerFun_sq : ∀ {𝕜 : Type u_1} [inst : RCLike 𝕜] {X : Type u_2} {V : Type u_3} [inst_1 : NormedAddCommGroup V]
  [inst_2 : InnerProductSpace 𝕜 V] (H : Type u_4) [inst_3 : NormedAddCommGroup H] [inst_4 : InnerProductSpace 𝕜 H]
  [inst_5 : RKHS 𝕜 H X V] [inst_6 : CompleteSpace H] [inst_7 : CompleteSpace V] (x : X),
  ‖RKHS.kernel H x x‖ = ‖RKHS.kerFun H x‖ ^ 2
-- Mathlib.RingTheory.IntegralClosure.IsIntegral.Basic
RingHom.IsIntegralElem.of_map : ∀ {R : Type u_1} {S : Type u_2} {T : Type u_4} [inst : CommRing R] [inst_1 : Ring S] [inst_2 : Ring T] {f : R →+* S}
  {g : S →+* T}, Function.Injective ⇑g → ∀ {x : S}, (g.comp f).IsIntegralElem (g x) → f.IsIntegralElem x
-- Mathlib.RingTheory.Bialgebra.Hom
BialgHomClass.toAlgHomClass : ∀ {R : Type u_1} {A : Type u_2} {B : Type u_3} {F : Type u_4} [inst : CommSemiring R] [inst_1 : Semiring A]
  [inst_2 : Algebra R A] [inst_3 : Semiring B] [inst_4 : Algebra R B] [inst_5 : CoalgebraStruct R A]
  [inst_6 : CoalgebraStruct R B] [inst_7 : FunLike F A B] [BialgHomClass F R A B], AlgHomClass F R A B
-- Mathlib.MeasureTheory.Function.SimpleFunc
MeasureTheory.SimpleFunc.lintegral.eq_1 : ∀ {α : Type u_1} {_m : MeasurableSpace α} (f : MeasureTheory.SimpleFunc α ENNReal) (μ : MeasureTheory.Measure α),
  f.lintegral μ = ∑ x ∈ f.range, x * μ (⇑f ⁻¹' {x})
-- Mathlib.Order.Partition.Finpartition
Finpartition.card_bot : ∀ {α : Type u_1} [inst : DecidableEq α] (s : Finset α), ⊥.parts.card = s.card
-- Lean.Parser.Types
Lean.Parser.ParserState.allErrors : Lean.Parser.ParserState → Array (String.Pos.Raw × Lean.Parser.SyntaxStack × Lean.Parser.Error)
-- Mathlib.NumberTheory.ModularForms.CongruenceSubgroups
CongruenceSubgroup.Gamma1_in_Gamma0 : ∀ (N : ℕ), CongruenceSubgroup.Gamma1 N ≤ CongruenceSubgroup.Gamma0 N
-- Mathlib.Topology.ContinuousOn
ContinuousWithinAt.matrixVecCons : ∀ {α : Type u_1} {β : Type u_2} [inst : TopologicalSpace α] [inst_1 : TopologicalSpace β] {n : ℕ} {f : α → β}
  {g : α → Fin n → β} {a : α} {s : Set α},
  ContinuousWithinAt f s a → ContinuousWithinAt g s a → ContinuousWithinAt (fun a => Matrix.vecCons (f a) (g a)) s a
-- Mathlib.Data.Nat.ModEq
Nat.add_modEq_left_iff : ∀ {n a b : ℕ}, a + b ≡ a [MOD n] ↔ n ∣ b
-- Mathlib.Tactic.Linter.TextBased
/-- Lint a collection of input strings if one of them contains trailing whitespace.  -/
_private.Mathlib.Tactic.Linter.TextBased.0.Mathlib.Linter.TextBased.trailingWhitespaceLinter : Mathlib.Linter.TextBased.TextbasedLinter✝
-- Mathlib.CategoryTheory.Skeletal
CategoryTheory.instInhabitedSkeleton : (C : Type u_1) → [inst : CategoryTheory.Category.{u_2, u_1} C] → [Inhabited C] → Inhabited (CategoryTheory.Skeleton C)
-- Init.SizeOf
Lean.ParserDescr.const.sizeOf_spec : ∀ (name : Lean.Name), sizeOf (Lean.ParserDescr.const name) = 1 + sizeOf name
-- Mathlib.Order.Filter.Map
/-- The monad structure on filters.  -/
Filter.monad : Monad Filter
-- Mathlib.Algebra.Group.Basic
neg_add_eq_of_eq_add : ∀ {G : Type u_3} [inst : AddGroup G] {a b c : G}, b = a + c → -a + b = c
-- Mathlib.Algebra.Group.Subgroup.ZPowers.Basic
Subgroup.mem_zpowers : ∀ {G : Type u_1} [inst : Group G] (g : G), g ∈ Subgroup.zpowers g
-- Mathlib.CategoryTheory.ComposableArrows.Basic
/-- The obvious map `obj X₀ X₁ i ⟶ obj X₀ X₁ j` whenever `i j : Fin 2` satisfy `i ≤ j`.  -/
CategoryTheory.ComposableArrows.Mk₁.map : {C : Type u_1} →
  [inst : CategoryTheory.Category.{v_1, u_1} C] →
    {X₀ X₁ : C} →
      (X₀ ⟶ X₁) →
        (i j : Fin 2) →
          i ≤ j → (CategoryTheory.ComposableArrows.Mk₁.obj X₀ X₁ i ⟶ CategoryTheory.ComposableArrows.Mk₁.obj X₀ X₁ j)
-- Mathlib.Data.Real.ConjExponents
Real.HolderTriple.inv_lt_inv : ∀ {p q r : ℝ}, p.HolderTriple q r → p⁻¹ < r⁻¹
-- Mathlib.Data.Nat.GCD.Basic
Nat.coprime_add_mul_right_left : ∀ (m n k : ℕ), (m + k * n).Coprime n ↔ m.Coprime n
-- Mathlib.Algebra.Group.Submonoid.Defs
Submonoid.mk : {M : Type u_3} → [inst : MulOneClass M] → (toSubsemigroup : Subsemigroup M) → 1 ∈ toSubsemigroup.carrier → Submonoid M
-- Mathlib.RingTheory.HahnSeries.Summable
HahnSeries.SummableFamily.hsum_equiv : ∀ {Γ : Type u_1} {R : Type u_3} {α : Type u_5} {β : Type u_6} [inst : PartialOrder Γ] [inst_1 : AddCommMonoid R]
  (e : α ≃ β) (s : HahnSeries.SummableFamily Γ R α), (HahnSeries.SummableFamily.Equiv e s).hsum = s.hsum
-- Mathlib.CategoryTheory.ObjectProperty.FunctorCategory.PreservesLimits
CategoryTheory.ObjectProperty.congr_preservesLimit : ∀ {J : Type u_1} {C : Type u_3} (K : Type u_5) [inst : CategoryTheory.Category.{v_1, u_5} K]
  [inst_1 : CategoryTheory.Category.{v_3, u_1} J] [inst_2 : CategoryTheory.Category.{v_5, u_3} C]
  {F F' : CategoryTheory.Functor K J} (e : F ≅ F'),
  CategoryTheory.ObjectProperty.preservesLimit F = CategoryTheory.ObjectProperty.preservesLimit F'
-- Mathlib.FieldTheory.IsAlgClosed.Basic
/-- Used in the definition of `equivOfEquiv`  -/
IsAlgClosure.equivOfEquivAux : {R : Type u} →
  {S : Type u_3} →
    (L : Type v) →
      (M : Type w) →
        [inst : CommRing R] →
          [inst_1 : CommRing S] →
            [inst_2 : Field L] →
              [inst_3 : Field M] →
                [inst_4 : Algebra R M] →
                  [inst_5 : Module.IsTorsionFree R M] →
                    [IsAlgClosure R M] →
                      [inst_7 : Algebra S L] →
                        [inst_8 : Module.IsTorsionFree S L] →
                          [IsAlgClosure S L] →
                            [IsDomain R] →
                              [IsDomain S] →
                                (hSR : S ≃+* R) →
                                  { e // e.toRingHom.comp (algebraMap S L) = (algebraMap R M).comp hSR.toRingHom }
-- Mathlib.Data.Set.Inclusion
Set.inclusion_self : ∀ {α : Type u_1} {s : Set α} (x : ↑s), Set.inclusion ⋯ x = x
-- Mathlib.Data.Num.Lemmas
PosNum.bit_to_nat : ∀ (b : Bool) (n : PosNum), ↑(PosNum.bit b n) = Nat.bit b ↑n
-- Mathlib.CategoryTheory.Limits.IsLimit
CategoryTheory.Limits.IsColimit.ofExtendIso.eq_1 : ∀ {J : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} J] {C : Type u₃} [inst_1 : CategoryTheory.Category.{v₃, u₃} C]
  {F : CategoryTheory.Functor J C} {s : CategoryTheory.Limits.Cocone F} {X : C} (i : s.pt ⟶ X)
  [inst_2 : CategoryTheory.IsIso i] (hs : CategoryTheory.Limits.IsColimit (s.extend i)),
  CategoryTheory.Limits.IsColimit.ofExtendIso i hs = hs.ofIsoColimit (s.extendIso (CategoryTheory.asIso i)).symm
-- Std.Sat.AIG.Basic
/-- Lookup a `Decl` in a `Cache`.
 -/
Std.Sat.AIG.Cache.get? : {α : Type} →
  [inst : Hashable α] →
    [inst_1 : DecidableEq α] →
      {decls : Array (Std.Sat.AIG.Decl α)} →
        Std.Sat.AIG.Cache α decls → (decl : Std.Sat.AIG.Decl α) → Option (Std.Sat.AIG.CacheHit decls decl)
-- Mathlib.Data.Finsupp.Multiset
Finsupp.mem_toMultiset : ∀ {α : Type u_1} (f : α →₀ ℕ) (i : α), i ∈ Finsupp.toMultiset f ↔ i ∈ f.support
-- Init.Data.String.Slice
String.Slice.instInhabitedSplitIterator.default : {σ : String.Slice → Type} →
  {ρ : Type} →
    {pat : ρ} →
      {s : String.Slice} → {inst : String.Slice.Pattern.ToForwardSearcher pat σ} → String.Slice.SplitIterator pat s
-- Mathlib.Tactic.TacticAnalysis
/-- The condition is returned from the `.trigger` function to indicate which sublists of a
tactic sequence to test.

The `context` field can be used to accumulate data between different invocations of `.trigger`.
 -/
Mathlib.TacticAnalysis.TriggerCondition : Type u_1 → Type u_1
-- Mathlib.Tactic.CategoryTheory.Coherence.Datatypes
Mathlib.Tactic.BicategoryLike.Mor₂Iso.of.injEq : ∀ (η η_1 : Mathlib.Tactic.BicategoryLike.AtomIso),
  (Mathlib.Tactic.BicategoryLike.Mor₂Iso.of η = Mathlib.Tactic.BicategoryLike.Mor₂Iso.of η_1) = (η = η_1)
-- Mathlib.RingTheory.DividedPowerAlgebra.Init
DividedPowerAlgebra.dp_mul : ∀ {R : Type u_2} {M : Type u_3} [inst : CommSemiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M] {n p : ℕ}
  {m : M},
  DividedPowerAlgebra.dp R n m * DividedPowerAlgebra.dp R p m = (n + p).choose n • DividedPowerAlgebra.dp R (n + p) m
-- Init.Data.Range.Polymorphic.UInt
UInt8.instHasSize_2 : Std.Rxi.HasSize UInt8
-- Mathlib.Algebra.Group.Prod
Prod.semiconjBy_iff : ∀ {M : Type u_3} {N : Type u_4} [inst : Mul M] [inst_1 : Mul N] {x y z : M × N},
  SemiconjBy x y z ↔ SemiconjBy x.1 y.1 z.1 ∧ SemiconjBy x.2 y.2 z.2
-- Mathlib.Algebra.Category.ModuleCat.Monoidal.Basic
/-- Construct for morphisms from the tensor product of two objects in `ModuleCat`.  -/
ModuleCat.MonoidalCategory.tensorLift : {R : Type u} →
  [inst : CommRing R] →
    {M₁ M₂ M₃ : ModuleCat R} →
      (f : ↑M₁ → ↑M₂ → ↑M₃) →
        (∀ (m₁ m₂ : ↑M₁) (n : ↑M₂), f (m₁ + m₂) n = f m₁ n + f m₂ n) →
          (∀ (a : R) (m : ↑M₁) (n : ↑M₂), f (a • m) n = a • f m n) →
            (∀ (m : ↑M₁) (n₁ n₂ : ↑M₂), f m (n₁ + n₂) = f m n₁ + f m n₂) →
              (∀ (a : R) (m : ↑M₁) (n : ↑M₂), f m (a • n) = a • f m n) →
                (CategoryTheory.MonoidalCategoryStruct.tensorObj M₁ M₂ ⟶ M₃)
-- Mathlib.Algebra.Pointwise.Stabilizer
AddAction.stabilizer_union_eq_left : ∀ {G : Type u_1} {α : Type u_3} [inst : AddGroup G] [inst_1 : AddAction G α] {s t : Set α},
  Disjoint s t →
    AddAction.stabilizer G s ≤ AddAction.stabilizer G t →
      AddAction.stabilizer G (s ∪ t) ≤ AddAction.stabilizer G t →
        AddAction.stabilizer G (s ∪ t) = AddAction.stabilizer G s
-- Std.Data.DHashMap.Lemmas
Std.DHashMap.getKey?_eq_some_getKeyD_of_contains : ∀ {α : Type u} {β : α → Type v} {x : BEq α} {x_1 : Hashable α} {m : Std.DHashMap α β} [EquivBEq α] [LawfulHashable α]
  {a fallback : α}, m.contains a = true → m.getKey? a = some (m.getKeyD a fallback)
-- Mathlib.CategoryTheory.Limits.Sifted
/-- If the `colim` functor `(C ⥤ Type) ⥤ Type` preserves binary products, then `C` is sifted or
empty.  -/
CategoryTheory.IsSifted.isSiftedOrEmpty_of_colim_preservesBinaryProducts : ∀ (C : Type u) [inst : CategoryTheory.SmallCategory C]
  [CategoryTheory.Limits.PreservesLimitsOfShape (CategoryTheory.Discrete CategoryTheory.Limits.WalkingPair)
      CategoryTheory.Limits.colim],
  CategoryTheory.IsSiftedOrEmpty C
-- Mathlib.Analysis.Meromorphic.Divisor
/-- The divisor of the inverse is the negative of the divisor.  -/
MeromorphicOn.divisor_inv : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {U : Set 𝕜} {f : 𝕜 → 𝕜},
  MeromorphicOn.divisor f⁻¹ U = -MeromorphicOn.divisor f U
-- Mathlib.RingTheory.Ideal.Quotient.Basic
Ideal.Quotient.smulCommClass : ∀ {R : Type u_3} [inst : Ring R] {I : Ideal R} [inst_1 : I.IsTwoSided] {α : Type u_5} [inst_2 : SMul α R]
  [inst_3 : IsScalarTower α R R] [SMulCommClass α R R], SMulCommClass α (R ⧸ I) (R ⧸ I)
-- Mathlib.Data.Finset.Sum
Finset.disjSum_strictMono_right : ∀ {α : Type u_1} {β : Type u_2} (s : Finset α), StrictMono s.disjSum
-- Lean.Elab.Tactic.Induction
/-- View of `Lean.Parser.Tactic.elimTarget`.  -/
Lean.Elab.Tactic.ElimTargetView : Type
-- Mathlib.Topology.MetricSpace.Gluing
/-- Premetric space structure on `Σ n, X n`.  -/
Metric.inductivePremetric : {X : ℕ → Type u} →
  [inst : (n : ℕ) → MetricSpace (X n)] →
    {f : (n : ℕ) → X n → X (n + 1)} → (∀ (n : ℕ), Isometry (f n)) → PseudoMetricSpace ((n : ℕ) × X n)
-- Lean.Data.Lsp.Extra
Lean.Lsp.PlainGoalParams.mk.sizeOf_spec : ∀ (toTextDocumentPositionParams : Lean.Lsp.TextDocumentPositionParams),
  sizeOf { toTextDocumentPositionParams := toTextDocumentPositionParams } = 1 + sizeOf toTextDocumentPositionParams
-- Mathlib.Algebra.Ring.SumsOfSquares
IsSumSq.below : {R : Type u_1} →
  [inst : Mul R] →
    [inst_1 : Add R] → [inst_2 : Zero R] → {motive : (a : R) → IsSumSq a → Prop} → {a : R} → IsSumSq a → Prop
-- Mathlib.Topology.Order.Basic
/-- The set of points which are isolated on the right is countable when the space is
second-countable.  -/
countable_setOfPred_covBy_right : ∀ {α : Type u} [inst : TopologicalSpace α] [inst_1 : LinearOrder α] [OrderTopology α] [SecondCountableTopology α],
  {x | ∃ y, x ⋖ y}.Countable
-- Lean.Util.Path
/-- Like `findWithExt`, but ensures the returned path exists.  -/
Lean.SearchPath.findModuleWithExt : Lean.SearchPath → String → Lean.Name → IO (Option System.FilePath)
-- Init.Data.SInt.Lemmas
ISize.ofIntLE_le_iff_le : ∀ {a b : ℤ} (ha₁ : ISize.minValue.toInt ≤ a) (ha₂ : a ≤ ISize.maxValue.toInt) (hb₁ : ISize.minValue.toInt ≤ b)
  (hb₂ : b ≤ ISize.maxValue.toInt), ISize.ofIntLE a ha₁ ha₂ ≤ ISize.ofIntLE b hb₁ hb₂ ↔ a ≤ b
-- Std.Data.Iterators.Producers.Monadic.Empty
Std.Iterators.Types.Empty.mk : {m : Type w → Type w'} → {β : Type w} → Std.Iterators.Types.Empty m β
-- Mathlib.Analysis.Analytic.Constructions
/-- `x⁻¹` is analytic away from zero  -/
analyticOnNhd_inv : ∀ {𝕜 : Type u_2} [inst : NontriviallyNormedField 𝕜] {𝕝 : Type u_8} [inst_1 : NormedDivisionRing 𝕝]
  [inst_2 : NormedAlgebra 𝕜 𝕝], AnalyticOnNhd 𝕜 (fun z => z⁻¹) {z | z ≠ 0}
-- Mathlib.CategoryTheory.Limits.Shapes.Pullback.Categorical.Basic
CategoryTheory.Limits.CategoricalPullback.CatCommSqOver.precomposeObjComp_inv_app_snd_app : ∀ {A : Type u₁} {B : Type u₂} {C : Type u₃} [inst : CategoryTheory.Category.{v₁, u₁} A]
  [inst_1 : CategoryTheory.Category.{v₂, u₂} B] [inst_2 : CategoryTheory.Category.{v₃, u₃} C]
  (F : CategoryTheory.Functor A B) (G : CategoryTheory.Functor C B) {X : Type u₄} {Y : Type u₅} {Z : Type u₆}
  [inst_3 : CategoryTheory.Category.{v₄, u₄} X] [inst_4 : CategoryTheory.Category.{v₅, u₅} Y]
  [inst_5 : CategoryTheory.Category.{v₆, u₆} Z] (U : CategoryTheory.Functor X Y) (V : CategoryTheory.Functor Y Z)
  (X_1 : CategoryTheory.Limits.CategoricalPullback.CatCommSqOver F G Z) (x : X),
  ((CategoryTheory.Limits.CategoricalPullback.CatCommSqOver.precomposeObjComp F G U V).inv.app X_1).snd.app x =
    CategoryTheory.CategoryStruct.id (X_1.snd.obj (V.obj (U.obj x)))
-- Init.Data.SInt.Lemmas
Int16.minValue_le_toInt : ∀ (x : Int16), Int16.minValue.toInt ≤ x.toInt
-- Std.Data.DHashMap.Internal.Model
_private.Std.Data.DHashMap.Internal.Model.0.Std.DHashMap.Internal.Raw₀.insertListₘ.match_1.eq_2 : ∀ {α : Type u_2} {β : α → Type u_1} (motive : List ((a : α) × β a) → Sort u_3) (hd : (a : α) × β a)
  (tl : List ((a : α) × β a)) (h_1 : Unit → motive [])
  (h_2 : (hd : (a : α) × β a) → (tl : List ((a : α) × β a)) → motive (hd :: tl)),
  (match hd :: tl with
    | [] => h_1 ()
    | hd :: tl => h_2 hd tl) =
    h_2 hd tl
-- Mathlib.Algebra.Group.Pointwise.Finset.Basic
Finset.preimage_mul_right_one : ∀ {α : Type u_2} [inst : Group α] {b : α}, Finset.preimage 1 (fun x => x * b) ⋯ = {b⁻¹}
-- Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic
Real.cos_sub_int_mul_two_pi : ∀ (x : ℝ) (n : ℤ), Real.cos (x - ↑n * (2 * Real.pi)) = Real.cos x
-- Mathlib.Analysis.SpecialFunctions.Trigonometric.Chebyshev.Extremal
_private.Mathlib.Analysis.SpecialFunctions.Trigonometric.Chebyshev.Extremal.0.Polynomial.Chebyshev.negOnePow_mul_iterateDerivativeC_pos : ∀ {n k i : ℕ},
  0 < k → k ≤ n → i ≤ n → ∀ {x : ℝ}, 1 ≤ x → 0 < (-1) ^ i * Polynomial.Chebyshev.iterateDerivativeC✝ n k x i
-- Lean.Meta.Eqns
/-- Equation theorems are generated on demand, check whether they were generated in an imported file.
 -/
_private.Lean.Meta.Eqns.0.Lean.Meta.alreadyGenerated? : Lean.Name → Lean.MetaM (Option (Array Lean.Name))
-- Mathlib.RingTheory.TensorProduct.IsBaseChangeFree
IsBaseChange.of_fintype_basis_eq : ∀ {R : Type u_1} [inst : CommSemiring R] {V : Type u_2} [inst_1 : AddCommMonoid V] [inst_2 : Module R V] {A : Type u_3}
  [inst_3 : CommSemiring A] [inst_4 : Algebra A R] [inst_5 : Module A V] [IsScalarTower A R V] {ι : Type u_4}
  {b : Module.Basis ι R V} [inst_7 : Fintype ι] {a : ι → A} {v : V},
  (Fintype.linearCombination A ⇑b) a = v ↔ ⇑(algebraMap A R) ∘ a = b.equivFun v
-- Mathlib.Data.ENNReal.Inv
ENNReal.inv_lt_one : ∀ {a : ENNReal}, a⁻¹ < 1 ↔ 1 < a
-- Mathlib.Probability.Kernel.IonescuTulcea.Traj
/-- When computing `∫ x, f x ∂traj κ n x₀`, because the trajectory up to time `n` is
determined by `x₀` we can replace `x` by `updateFinset x (Iic a) x₀`.  -/
ProbabilityTheory.Kernel.integral_traj : ∀ {X : ℕ → Type u_1} [inst : (n : ℕ) → MeasurableSpace (X n)]
  {κ : (n : ℕ) → ProbabilityTheory.Kernel ((i : ↥(Finset.Iic n)) → X ↑i) (X (n + 1))}
  [inst_1 : ∀ (n : ℕ), ProbabilityTheory.IsMarkovKernel (κ n)] {E : Type u_2} [inst_2 : NormedAddCommGroup E]
  [inst_3 : NormedSpace ℝ E] {a : ℕ} (x₀ : (i : ↥(Finset.Iic a)) → X ↑i) {f : ((n : ℕ) → X n) → E},
  MeasureTheory.AEStronglyMeasurable f ((ProbabilityTheory.Kernel.traj κ a) x₀) →
    ∫ (x : (n : ℕ) → X n), f x ∂(ProbabilityTheory.Kernel.traj κ a) x₀ =
      ∫ (x : (n : ℕ) → X n), f (Function.updateFinset x (Finset.Iic a) x₀) ∂(ProbabilityTheory.Kernel.traj κ a) x₀
-- Mathlib.Data.Matrix.Basic
Matrix.piRingEquiv_apply : ∀ {n : Type u_3} {ι : Type u_14} {β : ι → Type u_15} [inst : (i : ι) → AddCommMonoid (β i)]
  [inst_1 : (i : ι) → Mul (β i)] [inst_2 : Fintype n] (f : Matrix n n ((i : ι) → β i)) (i : ι),
  Matrix.piRingEquiv f i = f.map fun x => x i
-- Mathlib.Topology.Neighborhoods
isOpen_singleton_iff_punctured_nhds : ∀ {X : Type u} [inst : TopologicalSpace X] (x : X), IsOpen {x} ↔ nhdsWithin x {x}ᶜ = ⊥
-- Mathlib.AlgebraicGeometry.Birational.RationalMap
AlgebraicGeometry.Scheme.PartialMap.toPartialMap_toRationalMap_restrict : ∀ {X Y : AlgebraicGeometry.Scheme} [inst : AlgebraicGeometry.IsReduced X] [inst_1 : Y.IsSeparated] (f : X.PartialMap Y),
  (f.toRationalMap.toPartialMap.restrict f.domain ⋯ ⋯).hom = f.hom
-- Mathlib.Algebra.Order.Group.PosPart
leOnePart_min : ∀ {α : Type u_1} [inst : Lattice α] [inst_1 : Group α] [MulLeftMono α] [MulRightMono α] (a b : α), (a ⊓ b)⁻ᵐ = a⁻ᵐ ⊔ b⁻ᵐ